import Mathlib.CategoryTheory.CopyDiscardCategory.Basic import FormalLab.CategoricalConstructions.Monads import FormalLab.LogicAndComputation.LinearLogicAndResourceSemantics /-! # 第77章：指数様相と線形・非線形意味論——複製可能性を追加構造として制御する 前章の対称モノイダル閉圏は線形含意を解釈しましたが、任意の対象を複製する射や破棄する射は与えません。それでは、 通常のプログラムのように何度でも使える値を、線形な資源と同じ体系の中でどう扱えばよいでしょうか。 本章では、破棄と複製を余モノイド構造として明示し、加法的結合子と古典線形論理が要求する圏構造を切り分けます。 中心となる**指数様相**（exponential modality） `!` には、余モナドだけでは不十分であることを型から確かめます。 最後に線形・非線形モデル（linear/non-linear model; LNLモデル）へ進み、デカルト閉な世界と線形な世界を随伴で 分離する理由を説明します。 ## 複製と破棄には追加の余モノイド構造が要る 対象 `A` を破棄する射 `A→I` と複製する射 `A→A⊗A` は、モノイダル閉性のフィールドではありません。 それらを単位律・結合律と両立させると、`A` 上の余モノイド対象になります。交換と両立する複製には可換性も 要求します。 -/ namespace FormalLab.LogicAndComputation.ExponentialsAndLinearNonlinearModels open _root_.CategoryTheory open _root_.CategoryTheory.MonoidalCategory open scoped MonoidalCategory universe uC vC variable {C : Type uC} [Category.{vC} C] [MonoidalCategory C] variable [SymmetricCategory C] variable {A B : C} 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であり、線形論理の型付け判断を 意味しません。 ## 要点 * 破棄 `A→I` と複製 `A→A⊗A` は余モノイド構造であり、モノイダル閉性の一部ではない。 * 加法的結合子には圏論的積・余積が、古典線形論理の対合的否定には *-自律構造が必要である。 * 指数様相 `!` には余モナド構造に加え、`!A` 上の可換余モノイド構造とモノイダルな整合性が必要である。 * 線形・非線形意味論は、デカルト閉な非線形世界と対称モノイダル閉な線形世界を随伴で結ぶ。 * 一般の余モナドと線形指数余モナド、LNL随伴から誘導される余モナドを同一視しない。 ## 研究史と文献案内 Girard [GIR87] は指数的結合子を含む線形論理を導入しました。Seely [SEE89] は *-自律圏と余自由余代数を通じて、 古典線形論理の圏論モデルを研究しました。Benton [BEN95] は直観主義的な線形世界と非線形世界を対称モノイダル 随伴で結ぶLNL体系を提示しました。本章のLeanコードは必要な構造を層ごとに検査しますが、完全な線形指数余モナドや LNLモデルのstructureまでは実装していません。現行Lean APIには [MATHLIB] を参照してください。 ## 問題 ### 乗法的結合子と加法的結合子を反例で分ける テンソル右規則と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.LogicAndComputation.ExponentialsAndLinearNonlinearModels