import FormalLab.DependentTypeTheory.DependentTypes
import FormalLab.TypedComputation.SimplyTypedLambdaCalculus

/-!
# 第33章：純粋型システム・ラムダ・キューブ・構成計算

単純型、依存型、パラメトリック多相、型演算子は、互いに無関係な機能なのでしょうか。
それとも「何が何に依存できるか」という少数の規則から統一的に分類できるのでしょうか。

この章は名称の暗記から始めません。まず単純型付きラムダ計算の判断
$\Gamma \vdash t : A$ に、型自身を分類する判断 $\Gamma \vdash A : s$ を加えます。次に、Π型の束縛変数と
本体がどの階層に属するかを三つの軸として読みます。八体系の名前は、その組合せに
後から付く座標名です。最後に全三軸を持つCoCを位置づけ、帰納型・宇宙・商などを備える
Lean 4やCICと同一視できない理由を明確にします。

## sort公理とΠ形成規則から型理論を指定する

PTSは三つ組 $(\mathcal S,\mathcal A,\mathcal R)$ で指定されます。$\mathcal S$ はsortの集合、
$\mathcal A \subseteq \mathcal S^2$ はsort公理、$\mathcal R \subseteq \mathcal S^3$ はΠ形成規則です。
項・型・kindは別々の文法カテゴリではなく、判断 $\Gamma \vdash M : A$ の中で担う役割によって区別されます。
下のLeanコードはこの考え方の構文と
ラムダ・キューブの座標をモデル化するもので、完全なPTS型検査器ではありません。
-/

namespace FormalLab.DependentTypeTheory.PureTypeSystems

/-!
## 項・型・kindを一つの構文で表す

**純粋型システム**（pure type system; PTS）では、項と型に別々の文法を用意しません。
変数・適用・ラムダ抽象・依存積・sortを、同じ式の文法で表します。ある式が項・型・
kindのどれとして働くかは、構文の形だけでなく型判断によって決まります。

次の `Expression` はその共通構文の骨格です。`lam domain body` は
`λ (x : domain). body`、`pi domain codomain` は `Π (x : domain), codomain` を表します。
de Bruijn添字 `0` は最も近い束縛子を参照します。
-/

/-- ラムダ・キューブを記述する二つのsort。 -/
inductive PTSSort where
  | star
  | box

/-- sort集合を型 `SortType` で表したPTS仕様。公理関係とΠ形成関係だけを保持する。 -/
structure PTSSpec (SortType : Type) where
  sortAxiom : SortType → SortType → Prop
  productRule : SortType → SortType → SortType → Prop

/-- PTSの共通構文の骨格。型もkindも同じ構文の式として表す。 -/
inductive Expression where
  | sort : PTSSort → Expression
  | var : Nat → Expression
  | app : Expression → Expression → Expression
  | lam : Expression → Expression → Expression
  | pi : Expression → Expression → Expression

/-- 注釈付き恒等関数 `λ (x : A). x` の構文。 -/
def annotatedIdentity (A : Expression) : Expression :=
  .lam A (.var 0)

/-!
`*`（star）は項を分類する型のsort、`□`（box）は型を分類するkindのsortとして読みます。
ラムダ・キューブの標準的なPTS表示では公理 $* : \Box$ を置き、$\Box$ 自身の型はこの二sort
体系の内部では与えません。ここでの `*` と `□` はLeanの `Type` と `Sort` の別名では
ありません。Leanの可算な宇宙階層を、二sortへ潰して理解してはいけません。

三つ組のうち集合 $\mathcal S$ はLeanの型引数 `SortType` に、公理関係 $\mathcal A$ は
`PTSSpec.sortAxiom` に、形成関係 $\mathcal R$ は `PTSSpec.productRule` に対応します。この構造体は規則の
許可範囲だけを記録します。
項の導出、文脈の整形式性、簡約関係はまだ含みません。

## Π形成規則を座標にする

PTSの積形成規則はsortの三つ組 $(s_1,s_2,s_3)$ で指定されます。$(s_1,s_2,s_3)\in\mathcal R$
であるとき、次の形成規則を使えます。

$$
\frac{\Gamma \vdash A:s_1 \qquad \Gamma,x:A \vdash B:s_2}
     {\Gamma \vdash \Pi x:A.\,B:s_3}
\;\textsc{(product)}
$$

ラムダ・キューブでは、単純関数に必要な `(*, *, *)` を全頂点が持ち、残る三規則を
加えるか否かで座標を作ります。
-/

/-- ラムダ・キューブで区別する四種類のΠ形成規則。 -/
inductive ProductRule where
  /-- `(*, *, *)`：項から項への通常の関数。 -/
  | termToTerm
  /-- `(□, *, *)`：型を束縛して項を作る多相。 -/
  | typeToTerm
  /-- `(*, □, □)`：項を束縛して型構成子を作る依存型。 -/
  | termToType
  /-- `(□, □, □)`：型を束縛して型構成子を作る型演算子。 -/
  | typeToType

/-- 規則名をPTSのsort三つ組へ戻す。 -/
def productRuleSorts : ProductRule → PTSSort × PTSSort × PTSSort
  | .termToTerm => (.star, .star, .star)
  | .typeToTerm => (.box, .star, .star)
  | .termToType => (.star, .box, .box)
  | .typeToType => (.box, .box, .box)

/-!
`(*, □, □)` が「型が項に依存する」軸なのは、型族そのものが
`λ (x : A). B` という型レベルの関数だからです。その型 `Π (x : A), *` はkindに属します。
一方、個々の依存積 `Π (x : A), B x` の形成だけを見て三軸を推測すると向きを取り違えます。

## 三つの独立な追加機能

`CubeFeatures` の三つの真偽値は次を表します。

* `dependentTypes`：型が項に依存できる。
* `polymorphism`：項が型に依存できる。
* `typeOperators`：型が型に依存できる。

項が項に依存する通常の関数は全頂点に共通なので、座標には含めません。
-/

/-- ラムダ・キューブの頂点を決める三つの独立な機能。 -/
structure CubeFeatures where
  dependentTypes : Bool
  polymorphism : Bool
  typeOperators : Bool

/-- ある頂点で積形成規則が許されるか。通常の関数規則は常に許す。 -/
def CubeFeatures.allows (features : CubeFeatures) : ProductRule → Bool
  | .termToTerm => true
  | .typeToTerm => features.polymorphism
  | .termToType => features.dependentTypes
  | .typeToType => features.typeOperators

/-- 三軸の指定から二sortのPTS仕様を作る。 -/
def lambdaCubeSpec (features : CubeFeatures) : PTSSpec PTSSort where
  sortAxiom s₁ s₂ := s₁ = .star ∧ s₂ = .box
  productRule s₁ s₂ s₃ :=
    ∃ rule, productRuleSorts rule = (s₁, s₂, s₃) ∧ features.allows rule = true

/-!
## 形成だけでは項を型付けできない

$\mathcal A$ の要素 $(s_1,s_2)$ は、空の文脈でsortを導入します。

$$
\frac{(s_1,s_2)\in\mathcal A}{\varnothing\vdash s_1:s_2}
\;\textsc{(axiom)}
$$

変数を文脈へ加えるには、その型自身がsortを持つことを先に確かめます。文脈 $\Gamma$ が整形式で、
$\Gamma\vdash A:s$ なら、$\Gamma,x:A\vdash x:A$ を導けます。弱化は、既存の判断を新しい未使用変数の下へ
持ち上げます。形成済みのΠ型に対するラムダ抽象と適用は次の形です。

$$
\frac{\Gamma,x:A\vdash b:B \qquad \Gamma\vdash \Pi x:A.\,B:s}
     {\Gamma\vdash \lambda x:A.\,b:\Pi x:A.\,B}
\;\textsc{(abstraction)}
$$

$$
\frac{\Gamma\vdash f:\Pi x:A.\,B \qquad \Gamma\vdash a:A}
     {\Gamma\vdash f\,a:B[x:=a]}
\;\textsc{(application)}
$$

右下の $B[x:=a]$ は、$B$ に現れる自由な $x$ を $a$ で捕獲を避けて置換した式です。値域 $B$ が $x$ を
含まなければ通常の関数型 $A\to B$ に戻ります。さらに型がβ変換で一致するときの変換規則が、計算と型付けを
結びます。したがって `PTSSpec` の二関係は体系の可変部分を指定しますが、型付け関係そのものではありません。

## 三軸を代表項から見分ける

三つの追加規則は、すべて「型を引数に取る」という一語では区別できません。外側の束縛子と本体のsortを調べます。

1. $(\Box,*,*)$ は、型 $A:*$ を束縛して項を作ります。多相恒等関数の型は
   $\Pi A:*.\,\Pi x:A.\,A$ です。
2. $(*,\Box,\Box)$ は、項 $x:A$ を束縛して型族を作ります。例えば
   $\lambda n:\mathsf{Nat}.\,\mathsf{Vec}\;A\;n$ は $\Pi n:\mathsf{Nat}.*$ というkindを持ちます。
3. $(\Box,\Box,\Box)$ は、型 $A:*$ を束縛して型演算子を作ります。例えば
   $\lambda A:*.\,A\to A$ のkindは $\Pi A:*.*$ です。

多相恒等関数と型演算子は、どちらも型変数 $A$ を束縛します。前者の本体は項でありsort $*$ に分類され、後者の
本体は型でありkindの側に分類されます。この値域のsortが、項の多相と高階の型演算を分けます。

## 八頂点

三つの独立な真偽値には $2^3=8$ 通りあります。文献では次の名称が標準的です。
$\lambda\underline{\omega}$ と $\lambda\omega$ は下線の有無が意味を持つため、プレーンテキストでは機能の列も
必ず併記します。

| 体系 | 型←項 | 項←型 | 型←型 | 通称・役割 |
|---|:---:|:---:|:---:|---|
| `λ→` | × | × | × | 単純型付きラムダ計算 |
| `λP` | ○ | × | × | 依存型 |
| `λ2` | × | ○ | × | System F、二階多相 |
| $\lambda\underline{\omega}$ | × | × | ○ | 型演算子だけを加えた体系 |
| `λP2` | ○ | ○ | × | 依存型＋多相 |
| `λPω` | ○ | × | ○ | 依存型＋型演算子 |
| $\lambda\omega$ | × | ○ | ○ | System Fω |
| `λC` | ○ | ○ | ○ | 構成計算（CoC） |

矢印 `型←項` は「左のものが右のものに依存する」と読みます。関数の入出力方向では
ありません。
-/

/-- `λ→`：三機能を追加しない基点。 -/
def lambdaArrow : CubeFeatures := ⟨false, false, false⟩

/-- `λP`：型が項に依存する。 -/
def lambdaP : CubeFeatures := ⟨true, false, false⟩

/-- `λ2`（System F）：項が型に依存する。 -/
def lambda2 : CubeFeatures := ⟨false, true, false⟩

/-- `λ\underline{ω}`：型が型に依存する。 -/
def lambdaOmegaUnderlined : CubeFeatures := ⟨false, false, true⟩

/-- `λP2`：依存型と多相を組み合わせる。 -/
def lambdaP2 : CubeFeatures := ⟨true, true, false⟩

/-- `λPω`：依存型と型演算子を組み合わせる。 -/
def lambdaPOmega : CubeFeatures := ⟨true, false, true⟩

/-- `λω`（System Fω）：多相と型演算子を組み合わせる。 -/
def lambdaOmega : CubeFeatures := ⟨false, true, true⟩

/-- `λC`（CoC）：三機能を全て組み合わせる。 -/
def lambdaC : CubeFeatures := ⟨true, true, true⟩

theorem lambdaArrow_has_only_term_functions :
    lambdaArrow.allows .termToTerm = true ∧
    lambdaArrow.allows .typeToTerm = false ∧
    lambdaArrow.allows .termToType = false ∧
    lambdaArrow.allows .typeToType = false :=
  ⟨rfl, rfl, rfl, rfl⟩

theorem lambdaC_has_all_product_rules (rule : ProductRule) :
    lambdaC.allows rule = true := by
  cases rule <;> rfl

theorem lambdaCube_has_star_box_axiom (features : CubeFeatures) :
    (lambdaCubeSpec features).sortAxiom .star .box :=
  ⟨rfl, rfl⟩

theorem lambdaC_spec_contains_every_cube_product (rule : ProductRule) :
    (lambdaCubeSpec lambdaC).productRule
      (productRuleSorts rule).1
      (productRuleSorts rule).2.1
      (productRuleSorts rule).2.2 := by
  exact ⟨rule, rfl, lambdaC_has_all_product_rules rule⟩

/-!
## 構成計算（CoC）

CoCはキューブの対角頂点 `λC` です。単純型付きラムダ計算を基点にすると、次を同時に
許します。

1. **依存型**：型族が項を引数に取る。
2. **パラメトリック多相**：項が型を引数に取る。
3. **高階の型演算子**：型構成子が型を引数に取る。

ただし規則一覧だけでは型理論は完成しません。PTSの型判断には、sort公理と変数規則が必要です。
さらに弱化、Π形成、ラムダ抽象、適用、β変換による変換規則を備えます。
文脈の整形式性と代入補題も必要です。型保存、合流性、強正規化などは、体系について証明する
メタ定理です。「表現力が高い」ことから無矛盾性や停止性は自動では出ません。

命題＝型対応の下では、型は命題、項は証明、β簡約は証明の正規化として読めます。
CoCが「構成」と「計算」を同じ言語で扱う要点はここにあります。

## キューブの分類表をLeanで検査する範囲

`ProductRule` と `CubePoint` はラムダ・キューブの三軸と八頂点を有限データとして検査するための
Lean上の表現です。これはPTSの構文・文脈・型判断・β変換・メタ理論を全て実装したものでは
ありません。`rfl` で閉じる各定理は表の定義展開を検査しており、CoCの正規化や無矛盾性を
証明しているわけではありません。

## CoC、CIC、Lean 4を同一視しない

古典的なラムダ・キューブのCoCは二sort `* : □` と四種類のΠ形成規則を持つ小さな核です。
Lean 4はこれに似た依存ラムダ計算を核としますが、実際には可算な非累積宇宙、
非可述的かつ証明無関係な `Prop`、帰納族、商などを備えます。したがってLeanを単に
「キューブの `λC`」と呼ぶだけでは、kernelの重要な規則を落とします。CoCは設計の座標軸、
Leanはその発展形の一つとして理解します [LEAN-DTT]。

また、**帰納構成計算**（Calculus of Inductive Constructions; CIC）は、CoCへ帰納的定義を
組み込む系統の名称です。LeanとRocq（旧Coq）はCIC系の発想を共有しますが、宇宙の累積性、
証明無関係性、商、再帰のkernel上の扱いなどに差があります [LEAN-FAQ]。

## 要点

* PTSは項・型・kindを同じ構文で書き、sort公理とΠ形成規則で役割を判定する。
* ラムダ・キューブの三軸は、項による型への依存、型による項への依存、型による型への依存である。
* 八頂点は三機能の有無による分類で、発明順や強弱だけを表す年代図ではない。
* CoCは三軸をすべて持つが、帰納型などを備えるCICやLean 4そのものではない。
* 形成規則、型判断、計算規則、メタ定理がそれぞれ何を定めるかを混同しない。

## 研究史と文献案内

CoquandとHuetは1988年の論文でCoCの基本理論を提示しました [CH88]。Barendregtは1991年、
型付きラムダ計算群を一般化型システムとして統一し、CoCを八体系の標準的な立方体として
細分しました [BAR91]。ラムダ・キューブはCoCの発明順をそのまま描く年代図ではなく、
許される依存規則による包含関係の分類です。

CoC原論文 [CH88] とBarendregtのPTSによる再編 [BAR91] は役割が異なります。CoC・System F・
正規化をproof theoryから読むには [GLT89] を参照してください。LeanとCIC系の差は
[LEAN-DTT; LEAN-FAQ; LEAN-REF] が扱います。

## 問題

### PTSの規則から依存の許可範囲を読む

純粋型システムのsort、公理、Π形成規則をそれぞれ定義せよ。形成規則に現れる三つのsortについて、
定義域、値域、形成されるΠ型の分類を順に説明する。同じ構文範疇に項・型・kindを置けても、型判断における
役割まで同じになるわけではないことを具体的な判断で示す。

[CH88] のCoCと [BAR91] のPTSによる整理を対照し、原体系の記法と後世の一般化を混同しない表を
作れ。表には原典が与える規則、一般化でパラメータ化された部分、本章のLean上のモデルを含める。

### ラムダ・キューブを暗記せず復元する

ラムダ・キューブの三軸を「何が何に依存するか」という文で表し、各軸を追加したときに初めて
書ける代表的な型を一つずつ挙げよ。その記述から `λP2`、`λPω`、`λω` の機能を表を見ずに復元し、
八頂点を包含関係に従って配置する。

ポリモーフィック恒等関数と、型構成子を引数に取る高階演算を別々の軸へ分類せよ。両者を単に
「ジェネリック」と呼ぶと失われる区別を、束縛変数のsortから説明すること。

### 体系の規則とメタ定理を切り分ける

型形成規則を列挙することと、その体系について保存、合流性、強正規化を証明することを区別せよ。
各メタ定理が何を量化し、どの簡約関係に依存するかを書き、ある規則集合から自動的に全てが従う
わけではない理由を述べる。

CoC、CIC、Lean 4の差を比較する。少なくとも帰納型、宇宙、計算・再帰の扱いを比較項目に含める。LeanがCoCの
系譜にあるという歴史的説明を、LeanのkernelがCoCそのものであるという同一視へ強めてはならない。
-/

end FormalLab.DependentTypeTheory.PureTypeSystems