import Mathlib.CategoryTheory.CopyDiscardCategory.Basic import FormalLab.Logic.ProofSystems import FormalLab.TypeTheory.SimplyTypedLambdaCalculus import FormalLab.CategoryTheory.Monads import FormalLab.Bridges.MonoidalClosedCategories /-! # 第76章：線形論理・線形型——仮定を資源として追跡する 通常の自然演繹では、文脈に仮定 `A` があれば、それを使わなくても、何度使っても構いません。第10章の `NaturalDeduction.hyp` は所属証明 `A∈Γ` を受け取るため、一つの仮定を複数の枝から参照できます。この自由は 弱化と縮約という構造規則に支えられています。 $$ \frac{\Gamma\vdash B}{\Gamma,A\vdash B}\;\mathsf{weakening}, \qquad \frac{\Gamma,A,A\vdash B}{\Gamma,A\vdash B}\;\mathsf{contraction}. $$ 線形論理（linear logic）は、これらの規則を全ての仮定へ無条件には許しません。推論規則は、結論だけでなく、 どの仮定をどの部分導出が消費したかを記録します。その結果、同じ「かつ」や「ならば」に見えた結合子が、資源の 分配方法によって複数の結合子へ分かれます。 本章では、まず乗法的直観主義線形論理の小さなシーケント計算をLeanで定義します。次に項の変数出現回数を計算し、 破棄と複製が構文上どこに現れるかを観察します。圏論側では、対称モノイダル閉圏においてテンソルを文脈結合、 内部homを線形含意として解釈します。最後に加法的結合子、古典線形論理の双対性、指数様相 `!`、線形世界と 非線形世界を結ぶ随伴を位置づけます。 ## 線形性は線形代数という意味ではない ここで「線形」とは、ベクトル空間上の一次写像だけを指す語ではありません。証明やプログラムの仮定使用を、 自由に複製・破棄できない資源として扱うことを指します。ベクトル空間と線形写像は重要なモデルを与えますが、 線形論理の定義そのものではありません。 また「全ての変数が文字通り一回現れる」は、乗法的な項計算への有用な入口ですが、線形論理全体の定義では ありません。加法的結合子では同じ文脈を代替的な枝が共有し、指数様相の内側では複製と破棄が制御された形で 復活します。正確な条件は各推論規則が文脈をどう受け渡すかにあります。 ## 乗法的結合子は文脈を分割する 原子命題、テンソル単位 `1`、テンソル積 `A⊗B`、線形含意 `A⊸B` から式を作ります。判断 `Γ⊢A` の文脈は 利用可能な仮定の有限列です。交換規則は順序だけを変えますが、弱化と縮約は基本規則に含めません。 -/ namespace FormalLab.Bridges.LinearLogicAndResourceSemantics inductive LinearFormula where | atom : Nat → LinearFormula | one : LinearFormula | tensor : LinearFormula → LinearFormula → LinearFormula | lollipop : LinearFormula → LinearFormula → LinearFormula deriving DecidableEq, Repr infixr:56 " ⊗ₗ " => LinearFormula.tensor infixr:55 " ⊸ " => LinearFormula.lollipop abbrev LinearContext := List LinearFormula inductive LinearDerivation : LinearContext → LinearFormula → Type where | ax (A) : LinearDerivation [A] A | exchange {Γ Δ A} : Γ.Perm Δ → LinearDerivation Γ A → LinearDerivation Δ A | cut {Γ Δ A B} : LinearDerivation Γ A → LinearDerivation (A :: Δ) B → LinearDerivation (Γ ++ Δ) B | oneRight : LinearDerivation [] .one | tensorRight {Γ Δ A B} : LinearDerivation Γ A → LinearDerivation Δ B → LinearDerivation (Γ ++ Δ) (A ⊗ₗ B) | tensorLeft {Γ A B D} : LinearDerivation (A :: B :: Γ) D → LinearDerivation ((A ⊗ₗ B) :: Γ) D | lollipopRight {Γ A B} : LinearDerivation (A :: Γ) B → LinearDerivation Γ (A ⊸ B) | lollipopLeft {Γ Δ A B D} : LinearDerivation Γ A → LinearDerivation (B :: Δ) D → LinearDerivation ((A ⊸ B) :: (Γ ++ Δ)) D /-! 公理規則の文脈は `[A]` ちょうど一つです。通常の `A∈Γ` ではないため、未使用の仮定を公理へ残せません。 テンソル右規則は文脈を `Γ` と `Δ` に分け、左の証明と右の証明へ別々に渡します。同じ仮定を両方へ渡す 規則はありません。 $$ \frac{A\vdash A\qquad B\vdash B}{A,B\vdash A\otimes B}\;\otimes R. $$ -/ def linearIdentity (A : LinearFormula) : LinearDerivation [] (A ⊸ A) := .lollipopRight (.ax A) def linearPair (A B : LinearFormula) : LinearDerivation [A, B] (A ⊗ₗ B) := .tensorRight (.ax A) (.ax B) def linearApplication (A B : LinearFormula) : LinearDerivation [A ⊸ B, A] B := .lollipopLeft (.ax A) (.ax B) def eliminateTensor (A B D : LinearFormula) (body : LinearDerivation [A, B] D) : LinearDerivation [A ⊗ₗ B] D := .tensorLeft body /-! `linearIdentity` では導入した仮定を公理が一度消費します。`linearPair` の二成分は異なる文脈を受け取ります。 `linearApplication` は関数資源と引数資源をそれぞれ一度使います。これらは実行時コストが常に一であるという 主張ではありません。型付け導出中の仮定の流れを述べています。 ## cutは資源の出力を次の導出へ渡す cut規則では `Γ⊢A` が作った資源を、`A,Δ⊢B` の先頭仮定へ渡します。残る文脈は `Γ++Δ` であり、`A` を 作るために使った仮定と、`B` の残りを作る仮定を重ねて使いません。 -/ def linearCut {Γ Δ : LinearContext} {A B : LinearFormula} (producer : LinearDerivation Γ A) (consumer : LinearDerivation (A :: Δ) B) : LinearDerivation (Γ ++ Δ) B := .cut producer consumer def evaluateClosedLinearFunction (A B : LinearFormula) (function : LinearDerivation [] (A ⊸ B)) (argument : LinearDerivation [] A) : LinearDerivation [] B := linearCut argument (linearCut function (linearApplication A B)) /-! この定義はまず閉じた関数を `linearApplication` の関数仮定へcutし、次に閉じた引数を残った引数仮定へcutします。 二つの入力がそれぞれ一度だけ接続され、終文脈は空になります。Lean自身の関数型は非線形ですが、ここで構成した 対象言語の導出は `LinearDerivation` の規則に従います。対象言語と実装に使うメタ言語の構造規則は別です。 cut除去は、このような中間式を含む導出を同じ終シーケントのcutなし導出へ変換する定理です。線形論理でも cutは資源を勝手に複製する規則ではなく、二導出の境界を接続します。本章のLean定義はcutを構成しますが、 全導出に対するcut除去や正規化までは証明していません。 ## 出現回数は複製と破棄を見える形にする 線形ラムダ項の表面構文には、de Bruijn添字を持つ変数、単位、テンソル対を置きます。さらに抽象と適用を 加えます。次の関数は 指定した変数の自由出現回数を数えます。ラムダの下では、同じ自由変数を指す添字が一つ増えます。 -/ inductive ResourceTerm where | var : Nat → ResourceTerm | unit : ResourceTerm | tensor : ResourceTerm → ResourceTerm → ResourceTerm | lam : ResourceTerm → ResourceTerm | app : ResourceTerm → ResourceTerm → ResourceTerm deriving DecidableEq, Repr def occurrences (index : Nat) : ResourceTerm → Nat | .var found => if found = index then 1 else 0 | .unit => 0 | .tensor left right => occurrences index left + occurrences index right | .lam body => occurrences (index + 1) body | .app function argument => occurrences index function + occurrences index argument def identityBody : ResourceTerm := .var 0 def discardingBody : ResourceTerm := .unit def duplicatingBody : ResourceTerm := .tensor (.var 0) (.var 0) example : occurrences 0 identityBody = 1 := rfl example : occurrences 0 discardingBody = 0 := rfl example : occurrences 0 duplicatingBody = 2 := rfl /-! `λx.x` の本体は仮定を一回使い、`λx.()` は破棄し、`λx.(x,x)` は複製します。後二項は `ResourceTerm` という生構文としては作れますが、先ほどの乗法的導出規則からは自動的に型付けされません。 出現回数検査と型付け導出を同一視してはいけません。束縛、加法的分岐、指数様相を含む完全な線形型検査は、 構文木全体に対する文脈分割を追跡します。 「高々一回」を許す体系はアフィン型、「少なくとも一回」を要求して複製を許す体系はrelevant型と呼ばれます。 ちょうど一回を基本とする線形型とは、どの構造規則を許すかが異なります。実装上の所有権型も線形論理から 着想を得ますが、借用、寿命、可変性を備えた個々の言語仕様を線形論理そのものと同一視はできません。 ## 対称モノイダル閉圏が乗法的意味論を与える 線形式を圏 `C` の対象へ、線形導出を射へ移します。 | 構文 | 圏論的意味 | |---|---| | 文脈の結合 | テンソル積 `⊗` | | 空文脈 | テンソル単位 `I` | | 線形含意 `A⊸B` | 内部hom `[A,B]` | | 恒等規則 | 恒等射 | | cut | 射の合成 | | 交換 | 対称性 | | 含意右規則 | カリー化 | | 含意左規則・適用 | 評価射 | 対称性は文脈の順序を交換できることに対応します。非対称なモノイダル閉圏は、交換も制限する非可換な変種の 意味論になり得ます。 -/ open _root_.CategoryTheory open _root_.CategoryTheory.MonoidalCategory open _root_.CategoryTheory.MonoidalClosed open FormalLab.Bridges.MonoidalClosedCategories open scoped MonoidalCategory universe uC vC variable {C : Type uC} [Category.{vC} C] [MonoidalCategory C] variable [SymmetricCategory C] [MonoidalClosed C] variable {Γ Δ A B X Y Z : C} def interpretLinearImplication (A B : C) : C := internalHom A B def interpretIdentity (A : C) : A ⟶ A := 𝟙 A def interpretCut (f : Γ ⟶ A) (g : A ⟶ B) : Γ ⟶ B := f ≫ g def interpretTensorIntroduction (f : Γ ⟶ A) (g : Δ ⟶ B) : Γ ⊗ Δ ⟶ A ⊗ B := f ⊗ₘ g def interpretExchange (A B : C) : A ⊗ B ⟶ B ⊗ A := (β_ A B).hom def interpretAbstraction (body : A ⊗ Γ ⟶ B) : Γ ⟶ interpretLinearImplication A B := curry body def interpretApplication (A B : C) : interpretLinearImplication A B ⊗ A ⟶ B := (β_ (internalHom A B) A).hom ≫ evaluation A B omit [SymmetricCategory C] in theorem interpret_beta (body : A ⊗ Γ ⟶ B) : A ◁ interpretAbstraction body ≫ evaluation A B = body := whiskerLeft_curry_ihom_ev_app A B body omit [SymmetricCategory C] in theorem interpret_eta (function : Γ ⟶ interpretLinearImplication A B) : interpretAbstraction (uncurry function) = function := curry_uncurry function /-! `interpretApplication` で組紐を使うのは、前章の評価射が `A⊗[A,B]→B` の順を採用する一方、項の関数と引数を `[A,B]⊗A` の順に並べたためです。これは資源を複製する操作ではなく、二資源の順序交換です。 恒等射と合成は、導出の恒等とcutを検証します。テンソルの関手性とモノイダル整合性は、文脈分割と変数交換を 支えます。カリー化のβη則は含意の計算法則になります。構文圏を構成し、その射の等式をcut除去で割れば、対称モノイダル閉圏の 構造を持つ自由なモデルとして完全性を述べられます。本章は任意のモデルへの解釈を構成する段階を扱い、自由性の 証明までは含めません。 ## 複製と破棄には追加の余モノイド構造が要る 対象 `A` を破棄する射 `A→I` と複製する射 `A→A⊗A` は、モノイダル閉性のフィールドではありません。 それらを単位律・結合律と両立させると、`A` 上の余モノイド対象になります。交換と両立する複製には可換性も 要求します。 -/ open scoped ComonObj section ExplicitStructuralMaps variable [ComonObj A] def explicitDiscard : A ⟶ 𝟙_ C := ComonObj.counit def explicitDuplicate : A ⟶ A ⊗ A := ComonObj.comul example : explicitDuplicate (A := A) ≫ explicitDiscard (A := A) ▷ A = (λ_ A).inv := ComonObj.counit_comul A example : explicitDuplicate (A := A) ≫ A ◁ explicitDiscard (A := A) = (ρ_ A).inv := ComonObj.comul_counit A end ExplicitStructuralMaps /-! Leanでも `[ComonObj A]` を追加するまで二射は定義できません。デカルトモノイダル圏では全対象に標準的な可換 余モノイド構造があり、その射が対角射と終対象への一意射です。全ての射についてこの構造が自然なら、テンソルは 本質的にデカルト積へ戻ります。線形モデルでは通常、任意の `A` ではなく、複製可能と明示された対象だけに この構造を与えます。 ## 加法的結合子は同じ文脈から選択肢を作る 乗法的連言 `A⊗B` の右規則は文脈を二分しました。加法的連言 `A & B` の右規則は、同じ文脈から `A` と `B` の 両方を導く二つの代替的な方法を要求します。 $$ \frac{\Gamma\vdash A\qquad\Delta\vdash B}{\Gamma,\Delta\vdash A\otimes B} \qquad \frac{\Gamma\vdash A\qquad\Gamma\vdash B}{\Gamma\vdash A\mathbin{\&}B}. $$ `&` の二枝は同時に実行して同じ資源を二重消費するのではなく、後でどちらの射影を要求されても応答できる選択を 表します。圏論的には、`⊗` はモノイダル積、`&` は圏論的積で解釈されます。同様に加法的選言 `A⊕B` は余積、 その単位 `0` は始対象、`&` の単位 `⊤` は終対象です。 従って、対称モノイダル閉圏だけで全ての加法的結合子が解釈できるわけではありません。有限積と有限余積の存在を 追加で要求します。さらにテンソルが余積を保存すると、分配に関する標準射を同型として扱える場合があります。 ## 古典線形論理は否定と双対を前面に出す 古典線形論理では、線形否定 `A⊥` が対合的な双対を与えます。テンソルのDe Morgan双対がパー（par）です。 $$ A\mathbin{\operatorname{par}}B:=(A^\bot\otimes B^\bot)^\bot, \qquad A\multimap B:=A^\bot\mathbin{\operatorname{par}}B. $$ 乗法単位 `1` の双対は `⊥`、加法的連言 `&` の双対は加法的選言 `⊕`、`⊤` の双対は `0` です。この意味で 線形論理の双対性は、単に推論規則の矢印を反転するだけでなく、結合子を対にして交換します。 古典乗法的線形論理の標準的な圏論モデルには *-自律圏を用います。これは適切な双対化対象を備えた対称 モノイダル閉圏として表せます。対称モノイダル閉圏だけでは、全対象に対合的な線形否定が自動的に存在するとは 限りません。本章のLeanコードは直観主義的な `⊗,1,⊸` 断片を直接検証し、*-自律構造を仮定していません。 ## 指数様相は非線形使用を局所化する 指数様相 `!A` は「複製・破棄してよい `A`」を表します。代表的な構造射は次の四つです。 $$ \mathsf{der}:!A\to A, \quad\mathsf{dig}:!A\to!!A, \quad\mathsf{weak}:!A\to I, \quad\mathsf{contr}:!A\to!A\otimes!A. $$ 最初の二射は `!` が余モナドであることに対応し、後二射は各 `!A` が可換余モノイド対象であることに対応します。 任意の余モナドを選ぶだけでは、weakeningとcontractionも、テンソルとの必要な整合性も得られません。 -/ section Exponential variable (Bang : Comonad C) def bangDereliction (A : C) : Bang.obj A ⟶ A := Bang.ε.app A def bangDigging (A : C) : Bang.obj A ⟶ Bang.obj (Bang.obj A) := Bang.δ.app A variable [ComonObj (Bang.obj A)] def bangWeakening : Bang.obj A ⟶ 𝟙_ C := ComonObj.counit def bangContraction : Bang.obj A ⟶ Bang.obj A ⊗ Bang.obj A := ComonObj.comul end Exponential /-! 線形指数余モナドを完全に定義するには、余モナド構造、対称モノイダル構造との両立、`!A` 上の可換余モノイド 構造、その自然性をまとめます。しばしば `!A` を `A` 上の余自由可換余モノイドとして特徴づけますが、その存在は 任意の対称モノイダル閉圏からは従いません。 `!` を単に「値を何度でも使える」という実行時タグとみなすと、余モナド法則と余モノイド法則が見えなくなります。 derelictionは線形世界で一度使える値を取り出し、diggingは再利用可能性自体を再利用可能にします。weakeningと contractionは、その構造を持つ対象に限って破棄と複製を許します。 ## 線形世界と非線形世界を随伴で分ける Bentonのlinear/non-linear意味論では、非線形世界をデカルト閉圏 `C`、線形世界を対称モノイダル閉圏 `L` とし、 対称モノイダル随伴 $$ F:\mathcal C\rightleftarrows\mathcal L:G. $$ で結びます。複合 `! = F∘G` は `L` 上の余モナドになります。非線形世界のデカルト対角射と終対象射を `F` で 線形世界へ運ぶことで、`!A` の複製と破棄を説明します。 この二世界表示は、全ての線形対象へコピーを追加してデカルト閉圏へ潰すことを避けます。非線形な仮定と線形な 仮定を別の文脈に置く型付け規則も自然に導けます。一方、余モナドだけから必ずそのような随伴表示が一意に決まる わけではありません。Kleisli型・Eilenberg–Moore型の標準随伴と、モデルに要求する対称モノイダルな構造を 区別します。 ## 現行mathlibが形式化する境界 現行mathlibには対称モノイダル圏、モノイダル閉圏、余モナド、余モノイド対象、copy-discard圏の一般APIが あります。本章はそれらを組み合わせ、乗法的線形論理の基本射と `!` に必要なデータの各層を検査します。 ただし、線形論理の式・証明網・cut除去を束ねた専用APIが全て用意されているわけではありません。*-自律圏、 線形指数余モナド、Benton型LNLモデルにも別の追加構造が必要です。`LinearDerivation` は本章で定義した教育用の小体系です。 mathlibの `CategoryTheory.Linear` はhom加群上のスカラー作用に関する別のAPIであり、線形論理の型付け判断を 意味しません。 ## 要点 * 線形論理は弱化と縮約を全仮定へ無条件に許さず、推論規則ごとに資源の流れを記録する。 * 乗法的テンソルの右規則は文脈を分割し、加法的連言の右規則は同じ文脈に対する代替的な二導出を要求する。 * 対称モノイダル閉圏では、文脈をテンソル、線形含意を内部hom、cutを合成、抽象をカリー化として解釈する。 * 対称性は交換を与えるが、複製 `A→A⊗A` と破棄 `A→I` は閉性からは得られない。 * 指数様相 `!` には余モナド構造だけでなく、`!A` 上の可換余モノイド構造とモノイダルな整合性が必要である。 * 古典線形論理の否定とparを解釈するには、対称モノイダル閉性より強い *-自律構造を用いる。 * LNL意味論はデカルト閉な非線形世界と対称モノイダル閉な線形世界を随伴で結ぶ。 ## 研究史と文献案内 Girard [GIR87] は線形論理を導入し、乗法的・加法的・指数的結合子、線形否定、証明論と意味論を一つの体系として 提示した一次論文です。資源解釈は現在もっとも有力な導入です。ただし原論文全体を、後世の「資源論理」という 標語だけへ還元はできません。coherent space、位相的双対、cut除去との関係も含めて読んでください。 Seely [SEE89] は *-自律圏と余自由余代数を通じて古典線形論理の圏論モデルを研究した一次資料です。Benton [BEN95] は直観主義的な線形世界と非線形世界を対称モノイダル随伴で結ぶLNL体系を提示しました。本章の `LinearDerivation` はこれらの完全な体系ではなく、乗法的直観主義断片の資源分割をLeanで観察するための核です。 モノイダル閉圏と豊穣圏論の一般理論には [EK66], [KEL82]、現行Lean APIには [MATHLIB] を参照してください。 ## 問題 ### 弱化と縮約が導出をどこで止めるか調べる 原子式 `P,Q` について `[P,Q]⊢P` と `[P]⊢P⊗P` を `LinearDerivation` で構成しようとしてください。各構成子を 終結論から逆向きに適用し、最初に文脈の型が一致しなくなる位置を記録します。次に弱化規則と縮約規則を新しい 構成子として追加し、二判断がそれぞれ導けることを示してください。規則追加前に「証明できない」と述べるだけでなく、 導出不可能性を帰納法で証明するために必要な不変量まで定式化できれば完了です。 ### β簡約が資源使用を保存する条件を示す `ResourceTerm` に捕獲回避代入を定義し、線形な本体で束縛変数が一回、引数中の各自由変数も一回現れると仮定します。 `(λx.t) u` を `t[u/x]` へ簡約した前後で、各自由変数の出現回数が等しいことを証明してください。本体が `x` を 零回または二回使う反例も計算し、単なるβ簡約ではなく線形型付けの仮定が保存則に必要な箇所を特定します。 ### シーケント規則を圏の射へ逐語的に翻訳する `ax`, `cut`, `tensorRight`, `lollipopRight`, `lollipopLeft`, `exchange` の各規則について、前提導出を表す射の型と 結論射を通常の数式で書いてください。結合子と単位子を省略せず、始域と終域が一致するまで合成を補います。その後 本章の `interpretCut`, `interpretTensorIntroduction`, `interpretAbstraction`, `interpretApplication` と照合し、 Leanコードでまだ構成していない左規則の整合射を完成できれば完了です。 ### 乗法的結合子と加法的結合子を反例で分ける テンソル右規則とwith右規則に同じ二つの部分導出を代入し、前者では文脈が分割され、後者では同じ文脈が二回 現れることを導出木で示してください。次にデカルト閉圏 `Type` で、テンソルと積の差が見えにくくなる理由を 説明します。一般の対称モノイダル閉圏では、`A⊗B` と圏論的積 `A&B` を比較する標準同型が存在しない例を調べます。 モデルの追加仮定と論理規則の対応を表にできれば完了です。 ### 余モナドと線形指数余モナドの差を列挙する 任意の余モナド `Bang` から `bangDereliction` と `bangDigging` を取り出し、三つの余モナド法則を書いてください。 次に `bangWeakening` と `bangContraction` の型を得るために追加した `ComonObj (Bang.obj A)` の三法則を展開します。 さらに自然性、可換性、テンソルとの整合性を調べます。余モナド構造との両立も含め、どの条件が両クラスだけでは 未保証かを分類してください。線形指数余モナドの定義案をLeanのstructureとして提示できれば完了です。 ### LNL随伴から指数様相を構成する デカルト閉圏 `C` と対称モノイダル閉圏 `L` の間に、対称モノイダル随伴 `F⊣G` を仮定します。`F⋙G` と `G⋙F` のどちらがどちらの圏上のモナド・余モナドになるかを、単位と余単位の型から判定してください。 線形世界 `L` 上で、`!=F⋙G` のderelictionとdiggingを書きます。次に `C` の対角射と終対象射から、`!A` の contractionとweakeningを運ぶ構成を図式化します。全ての射の始域と終域を照合できれば完了です。 -/ end FormalLab.Bridges.LinearLogicAndResourceSemantics