import FormalLab.Proofs.ProofSystems
import FormalLab.TypedComputation.SimplyTypedLambdaCalculus
import FormalLab.LogicAndComputation.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.LogicAndComputation.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.LogicAndComputation.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除去で割れば、対称
モノイダル閉圏の構造を持つ自由なモデルとして完全性を述べられます。本章は任意のモデルへの解釈を構成する段階を
扱い、自由性の証明までは含めません。

## 要点

* 線形論理は弱化と縮約を全仮定へ無条件に許さず、推論規則ごとに資源の流れを記録する。
* 乗法的テンソルの右規則は文脈を分割し、同じ仮定を二つの部分導出へ重ねて渡さない。
* 対称モノイダル閉圏では、文脈をテンソル、線形含意を内部hom、cutを合成、抽象をカリー化として解釈する。
* 対称性は交換を与えるが、複製 `A→A⊗A` と破棄 `A→I` はモノイダル閉性からは得られない。

## 研究史と文献案内

Girard [GIR87] は線形論理を導入し、乗法的・加法的・指数的結合子、線形否定、証明論と意味論を一つの体系として
提示した一次論文です。本章ではそのうち、乗法的直観主義断片の資源分割を小さな導出体系で検査します。
対称モノイダル閉圏の一般理論には [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コードでまだ構成していない左規則の整合射を完成できれば完了です。
-/

end FormalLab.LogicAndComputation.LinearLogicAndResourceSemantics