import FormalLab.Foundation.UntypedLambdaCalculus

/-!
# 第11章：単純型付きラムダ計算——型判断を規則として読む

ラムダ項に型を付けるとは、各項へ後からラベルを貼ることなのでしょうか。それとも、
文脈と規則から導出できる項だけを受理することなのでしょうか。

**単純型付きラムダ計算**（simply typed lambda calculus; STLC）は、非型付きラムダ項へ
型判断を与えます。本章ではChurch流のように変数へ型注釈を埋め込む構文ではなく、同じ
生の項に対して外側から判断を定義します。この選択により「項の構文」と「項を受理する
型付け規則」を分離して観察できます。文脈、変数、適用、抽象の規則から実際の導出木を作り、
最後に進行・保存・強正規化が互いに異なるメタ定理であることまで見通します。

## 生のラムダ項に型判断を与える

対象言語の型と項を

$$
A,B ::= \iota\mid A\Rightarrow B,
\qquad
t,u ::= x\mid t\,u\mid\lambda x.t
$$

で生成し、判断 `Γ ⊢ t : A` を変数・適用・抽象の三規則で帰納的に定めます。このBNF風の
記法は構文の生成規則であり、Lean自身の型宣言ではありません。下ではこの対象言語と判断を
Leanの帰納型として別々に形式化します。
-/

namespace FormalLab.TypeTheory.SimplyTypedLambdaCalculus

open FormalLab.Foundation.UntypedLambdaCalculus

/-!
## 単純型と文脈をデータとして定義する

最小の単純型は、原子型と関数型から帰納的に作れます。`A ⇒ B` は、`A` 型の入力を
受け取り `B` 型の出力を返す関数の型です。ここでは対象言語の型とLeanの関数型を
区別するため、独自の構文木を定義します。
-/

/-- 単純型の構文。 -/
inductive SimpleType where
  | atom : SimpleType
  | arrow : SimpleType → SimpleType → SimpleType
  deriving DecidableEq

infixr:60 " ⇒ " => SimpleType.arrow

/-- 文脈は、最も近い束縛変数の型を先頭に置く型の列である。 -/
abbrev Context := List SimpleType

/-!
文脈 `Γ` は、自由変数について現在仮定している型を記録します。de Bruijn添字 `0` は
先頭、`n + 1` は一つ外側の仮定を参照します。`Lookup Γ n A` は「`Γ` の `n` 番目の
変数は型 `A` を持つ」という判断です。文脈は実行時に関数へ渡す値の列ではなく、導出を
検査するときに利用できる仮定の列です。同じ生の変数 `.var 0` でも、文脈が変われば
割り当てられる型は変わります。
-/

/-- 文脈中のde Bruijn添字へ型を割り当てる導出関係。 -/
inductive Lookup : Context → Nat → SimpleType → Prop where
  | zero : Lookup (A :: Γ) 0 A
  | succ : Lookup Γ index A → Lookup (B :: Γ) (index + 1) A

/-- 固定した文脈と添字に対する変数の型は一意です。 -/
theorem lookup_unique {Γ : Context} {index : Nat} {A B : SimpleType}
    (left : Lookup Γ index A) (right : Lookup Γ index B) : A = B := by
  induction left generalizing B with
  | zero =>
      cases right
      rfl
  | succ left inductionHypothesis =>
      cases right with
      | succ right => exact inductionHypothesis right

/-!
## 型判断

`HasType Γ term A` に対応する型付け判断を `Γ ⊢ term : A` と書きます。これは真偽を計算する関数では
なく、次の三規則から有限な導出を構成できるという命題です。

$$
\frac{\Gamma(n)=A}{\Gamma\vdash n:A}\;(\mathsf{var})
\qquad
\frac{\Gamma\vdash f:A\Rightarrow B\qquad\Gamma\vdash a:A}
     {\Gamma\vdash f\,a:B}\;(\mathsf{app})
$$

$$
\frac{A::\Gamma\vdash t:B}
     {\Gamma\vdash \lambda.t:A\Rightarrow B}\;(\mathsf{lam}).
$$

規則名は証明項の構成子です。したがって型検査の結果だけでなく、なぜその型を持つかという
導出木そのものをLeanの値として構成できます。
-/

/-- 文脈の下で生のラムダ項が単純型を持つ、という型判断。 -/
inductive HasType : Context → Term → SimpleType → Prop where
  | var : Lookup Γ index A → HasType Γ (.var index) A
  | app : HasType Γ function (A ⇒ B) → HasType Γ argument A →
      HasType Γ (.app function argument) B
  | lam : HasType (A :: Γ) body B → HasType Γ (.lam body) (A ⇒ B)

/-! ## 有限単純型は自分自身を真部分として含めない -/

/-- 型構文木の節点数です。 -/
def SimpleType.size : SimpleType → Nat
  | .atom => 1
  | .arrow domain codomain => domain.size + codomain.size + 1

/-- 型は、その型を始域に持つ関数型より真に小さい。 -/
theorem SimpleType.size_lt_self_arrow (A B : SimpleType) : A.size < (A ⇒ B).size := by
  simp only [SimpleType.size]
  omega

/-- 有限に生成された単純型では方程式 `A = A ⇒ B` は解を持ちません。 -/
theorem SimpleType.ne_self_arrow (A B : SimpleType) : A ≠ A ⇒ B := by
  intro equality
  exact (Nat.ne_of_lt (A.size_lt_self_arrow B)) (congrArg SimpleType.size equality)

/-!
## 導出を構成する

恒等関数の本体 `0` は、拡張された文脈の先頭にある型 `A` を持ちます。その一段の
変数導出を `lam` 規則で閉じれば、空文脈でも `A ⇒ A` が得られます。
-/

theorem identity_has_type (A : SimpleType) :
    HasType [] identity (A ⇒ A) :=
  .lam (.var .zero)

theorem constant_has_type (A B : SimpleType) :
    HasType [] constant (A ⇒ B ⇒ A) :=
  .lam (.lam (.var (.succ .zero)))

theorem identity_applied_has_type (A : SimpleType) :
    HasType [] (.app identity identity) (A ⇒ A) :=
  .app (identity_has_type (A ⇒ A)) (identity_has_type A)

/-- Curry流では、同じ生の恒等項が異なる単純型の導出を持ちます。 -/
theorem identity_has_distinct_typings :
    HasType [] identity (.atom ⇒ .atom) ∧
      HasType [] identity ((.atom ⇒ .atom) ⇒ (.atom ⇒ .atom)) :=
  ⟨identity_has_type .atom, identity_has_type (.atom ⇒ .atom)⟩

example : (.atom ⇒ .atom) ≠ ((.atom ⇒ .atom) ⇒ (.atom ⇒ .atom)) := by
  decide

/-!
`identity_applied_has_type` の導出を下から上へ読むと、結論は `identity identity : A ⇒ A`
です。適用規則は、関数位置の恒等項へまず `(A ⇒ A) ⇒ (A ⇒ A)` を要求し、引数位置の
同じ恒等項へ `A ⇒ A` を要求します。同じ生の項が二か所で異なる型を持つのは矛盾では
ありません。それぞれ別の導出で型変数 `A` の具体化が異なるからです。

$$
\frac{\vdash \mathsf{id}:(A\Rightarrow A)\Rightarrow(A\Rightarrow A)
      \qquad
      \vdash \mathsf{id}:A\Rightarrow A}
     {\vdash \mathsf{id}\;\mathsf{id}:A\Rightarrow A}.
$$

型は同じ項の全ての部分に独立に付くのではありません。適用規則では、関数の入力型と
引数の型が同じでなければ導出を組み立てられません。また `λ x. x x` の自己適用を
単純型付けしようとすると、同じ `x` に `A` と `A ⇒ B` を同時に要求します。有限な
単純型ではこの方程式を解けません。非型付き計算で書ける項を、型規則が選別しています。

`SimpleType.ne_self_arrow` は「有限な単純型では解けない」という説明を、型構文木の大きさが
$A<A\Rightarrow B$ と真に増えることへ還元します。自己適用の型付け失敗をelaboratorの診断だけに委ねず、
規則から生じる型方程式そのものが矛盾する理由をLeanで検査しています。

ここで「型がない」とは、項が無意味な文字列だという意味ではありません。`λ x. x x` は
非型付きラムダ計算の正当な構文ですが、このSTLCの規則では型導出を持たないという意味です。
構文の整形式性と型付け可能性を分離しておきます。

## 型安全性を三つに分解する

STLCの基本的なメタ定理は次の三段階で述べます。

1. **置換補題**：型の合う項を代入しても型判断が保存される。
2. **保存定理**（subject reduction / preservation）：`t : A` かつ `t → t'` なら
   `t' : A`。
3. **進行定理**（progress）：閉じた型付き項は値であるか、一段簡約できる。

保存と進行を合わせた性質を通常 **型安全性**と呼びます。さらにSTLCでは全ての型付き項が
有限回のβ簡約で正規形へ到達する **強正規化**が成り立ちます。これらは型判断の定義そのもの
ではなく、その定義について証明すべきメタ定理です。本章は型判断の構成に焦点を絞ります。
続く四章で構造規則、操作的意味論、型安全性、正規化を扱います。代入から一段簡約、保存、進行、
停止性へ進み、互いに依存する別の主張として順に構成します。

進行だけでは「簡約後も正しい」とはいえず、保存だけでは「行き詰まらない」とはいえません。
また両方が成り立っても、無限に簡約し続けないことまでは従いません。強正規化は型安全性
より強い、別の停止性の主張です。定理名を覚えるより、各定理の仮定と結論を比較します。

## 単純型から依存型へ

関数型 `A ⇒ B` では、出力型 `B` は入力値を見ません。「型族・依存関数型・依存対型」ではこれを
`(x : A) → B x` へ一般化し、型が項 `x` に依存できるようにします。単純関数型は、
`B` が `x` を使わない依存関数型の特殊例として回収されます。

## 対象言語の型判断をLeanで検査する

`HasType Γ t A : Prop` は、判断 `Γ ⊢ t : A` をLean内の帰納的命題として表したものです。
この命題の構成子はSTLCの導出規則であり、Lean自身の型付け規則ではありません。Leanのkernelが
直接検査するのは「与えた値が `HasType Γ t A` の証明項か」です。この一段の引用を意識すると、
対象言語のメタ定理と、メタ言語Leanの健全性を混同せずに読めます。

`HasType` の値域を `Prop` にしたため、Leanでは同じ判断の二つの導出は証明無関係性により等しいと扱われます。
導出の存在を証明する目的には適しますが、導出木の違いを計算データとして分析する表現ではありません。
その違いを保持したい場合は、第10章の `NaturalDeduction : ... → Type` のように値域を `Type` に選びます。

## この型判断が扱う範囲

この `HasType` は本章で定義したSTLCの外在的な型判断であり、Lean kernel自身の
型検査器ではありません。また、型が一つ付けばプログラムが停止するという主張は任意の
型システムには成り立ちません。ここでの強正規化はSTLCの規則を選んだ結果です。

この章では「型を導出できる」という関係だけを定義し、型推論アルゴリズムは実装して
いません。宣言的な規則が何を正しいと認めるかと、それを決定する手続きを区別します。

## 要点

* 生の項は構文、単純型は型の構文、`HasType` は両者を文脈の下で結ぶ判断である。
* 型導出は、変数・適用・抽象の規則を組み合わせた有限の証拠である。
* 適用では関数の入力型と引数の型が一致しなければならない。
* 保存・進行・強正規化は、それぞれ異なるメタ定理である。
* 依存型は、関数の出力型が入力項を参照できるようSTLCを一般化する。

## 研究史と文献案内

Churchの1940年の単純型理論は、ラムダ変換と単純型を結びつけた基準文献です [CHU40]。
同時期までにCurryは、項の構文へ型を埋め込まず型を割り当てる体系を研究していました。
現在いうChurch-style / Curry-styleの区別は、この構文上の差を整理する後世の用語です。
構文と型判断から、反転補題・置換・保存・進行へ進むには [TAPL02] を参照してください。
判断体系を言語設計の中心に置く見方は [PFPL16]、正規化とproof theoryは [GLT89] が扱います。
本章の `HasType` は、これらの特定の体系を完全再現したものではありません。

## 問題

### 証明項を型導出木へ戻す

文脈、型判断、型導出をそれぞれ定義し、同じ判断に複数の導出があり得るか検討せよ。
`identity_has_type` と `constant_has_type` のLean証明項を推論規則による導出木へ変換し、各構成子が変数・
抽象・適用のどの規則に対応するかを注記する。

`identity_applied_has_type` では適用規則の関数側と引数側で共有される型を全て書き出せ。導出木の
枝が独立ではなく、中間型によって整合させられていることを確認する。

### 型の付く項と付かない項の境界を探る

de Bruijn表現で `λ f. λ x. f x` を定義し、`(A ⇒ B) ⇒ A ⇒ B` の型導出をLeanで構成せよ。
添字 `0` と `1` がどの束縛変数を指すかを各文脈で示し、添字のずれを型エラーから診断する。

次に自己適用 `λx. x x` へ単純型を割り当てようとし、`X = X ⇒ Y` という形の型方程式が生じる
ことを導け。単にLeanが拒否したと報告せず、有限に生成される単純型では方程式を解けない理由を
構造の大きさから説明すること。

### 型安全性の三つの主張を分ける

置換補題、保存定理、進行定理を、それぞれ仮定と結論を省略せずに書け。保存と進行を組み合わせると
何が保証され、停止まではなぜ保証されないかを説明する。強正規化が追加する主張も区別せよ。

最後に [CHU40] の項に型を記す構文と、本章の外在的判断 `HasType` を比較する。後世の名称だけに
頼らず、項の構文、型検査へ渡る情報、同じ無型項に複数の型を導出できる可能性という観点で表にせよ。
通常の関数型が定数族に対する依存関数型であることまで説明すれば、次の依存型へ接続できる。
-/

end FormalLab.TypeTheory.SimplyTypedLambdaCalculus