import FormalLab.TypeTheory.OperationalSemantics

/-!
# 第14章：再帰型・fold/unfold・型の無限展開

リストの型を `List A = 1 + A × List A` と書くと、定義しようとする型が右辺にも現れます。この式は
有限回の略記展開だけでは消えません。右辺を一層作る操作と、その一層を観察する操作を型体系へどう
組み込むかによって、再帰型には異なる設計が生じます。

本章では型変数を束縛する記法 `μα.T` を導入します。iso-recursive型では `μα.T` と
`T[μα.T/α]` の間を明示的な `roll` と `unroll` で往復させます。equi-recursive型では両者を
型同値関係で結びます。対象言語の構文、型付け、一段簡約をLean内に記述し、明示的な展開簡約が
型を保存することまで証明します。

## `μ` は型変数を一つ束縛する

型 `μα.T` の `α` は本体 `T` の中で束縛されます。本章では束縛変数を名前でなくde Bruijn添字で
表し、`bound 0` を最も内側の `μ` が束縛する変数と読みます。型の一層展開は次の置換です。

$$
\mathsf{unfoldType}(\mu\alpha.T)=T[\mu\alpha.T/\alpha].
$$

束縛子の下へ置換を進めるときは、代入する型の自由添字を一つずらします。この処理がなければ、内側の
`μ` が代入項の自由変数を誤って捕獲します。
-/

namespace FormalLab.TypeTheory.RecursiveTypes

inductive RType where
  | unit
  | sum (left right : RType)
  | product (left right : RType)
  | arrow (domain codomain : RType)
  | bound (index : Nat)
  | mu (body : RType)
  deriving DecidableEq, Repr

def shift (amount cutoff : Nat) : RType → RType
  | .unit => .unit
  | .sum left right => .sum (shift amount cutoff left) (shift amount cutoff right)
  | .product left right => .product (shift amount cutoff left) (shift amount cutoff right)
  | .arrow domain codomain => .arrow (shift amount cutoff domain) (shift amount cutoff codomain)
  | .bound index => if cutoff ≤ index then .bound (index + amount) else .bound index
  | .mu body => .mu (shift amount (cutoff + 1) body)

def substitute (target : Nat) (replacement : RType) : RType → RType
  | .unit => .unit
  | .sum left right =>
      .sum (substitute target replacement left) (substitute target replacement right)
  | .product left right =>
      .product (substitute target replacement left) (substitute target replacement right)
  | .arrow domain codomain =>
      .arrow (substitute target replacement domain) (substitute target replacement codomain)
  | .bound index =>
      if index = target then replacement
      else if target < index then .bound (index - 1) else .bound index
  | .mu body => .mu (substitute (target + 1) (shift 1 0 replacement) body)

def unfoldType (body : RType) : RType :=
  substitute 0 (.mu body) body

def natBody : RType :=
  .sum .unit (.bound 0)

def recursiveNat : RType :=
  .mu natBody

example : unfoldType natBody = .sum .unit recursiveNat := rfl

def nestedExample : RType :=
  .mu (.mu (.sum (.bound 1) (.bound 0)))

example : unfoldType (.mu (.sum (.bound 1) (.bound 0))) =
    .mu (.sum nestedExample (.bound 0)) := rfl

/-!
最初の計算は `μX.1+X` を一層展開して `1+(μX.1+X)` を得ます。二番目では外側の型を内側の
束縛子の下へ代入します。代入された型の自由添字を持ち上げるため、内側の `bound 0` は内側の
`μ` に束縛されたままです。

## iso-recursive型は同型を項で目に見える形にする

iso-recursive型では、折り畳まれた型 `μX.T` と展開型 `T[μX.T/X]` は型検査器にとって同じ型では
ありません。導入子 `roll` と除去子 `unroll` が両者を橋渡しします。

$$
\frac{\Gamma\vdash t:T[\mu X.T/X]}
     {\Gamma\vdash\mathsf{roll}[T]\,t:\mu X.T}
\qquad
\frac{\Gamma\vdash t:\mu X.T}
     {\Gamma\vdash\mathsf{unroll}\,t:T[\mu X.T/X]}.
$$

計算規則

$$
\mathsf{unroll}(\mathsf{roll}[T],v)\longrightarrow v
$$

は二型をLeanの定義的等しさにせず、項による往復の隣接対だけを消去します。

次の対象言語は単位、直和、直積、`roll`、`unroll` を持ちます。Lean自身の帰納型を再帰型と呼んでいる
のではなく、再帰型を持つ小言語の構文と型付けをLeanで表現しています。
-/

inductive Term where
  | unit
  | inl (term : Term)
  | inr (term : Term)
  | pair (left right : Term)
  | roll (body : RType) (term : Term)
  | unroll (term : Term)
  deriving Repr

inductive HasType : Term → RType → Prop where
  | unit : HasType .unit .unit
  | inl : HasType term left → HasType (.inl term) (.sum left right)
  | inr : HasType term right → HasType (.inr term) (.sum left right)
  | pair : HasType left leftType → HasType right rightType →
      HasType (.pair left right) (.product leftType rightType)
  | roll : HasType term (unfoldType body) → HasType (.roll body term) (.mu body)
  | unroll : HasType term (.mu body) → HasType (.unroll term) (unfoldType body)

inductive Value : Term → Prop where
  | unit : Value .unit
  | inl : Value term → Value (.inl term)
  | inr : Value term → Value (.inr term)
  | pair : Value left → Value right → Value (.pair left right)
  | roll : Value term → Value (.roll body term)

/-!
対 `pair left right` は、左右の項がそれぞれ型 $A$ と $B$ を持つとき直積型 $A\times B$ を持ちます。
値呼びでは左成分を先に進め、左が値になった後で右成分を進めます。直積の項構成子を型構文だけでなく
対象言語にも備えたため、章末問題の一層関手 $1+A\times X$ を実際の項として構成できます。
本章ではリストの一層を作ることに必要な導入側だけを扱い、射影による除去規則は加えていません。
-/

def zero : Term :=
  .roll natBody (.inl .unit)

def successor (number : Term) : Term :=
  .roll natBody (.inr number)

theorem zero_typed : HasType zero recursiveNat := by
  exact .roll (.inl .unit)

theorem one_typed : HasType (successor zero) recursiveNat := by
  exact .roll (.inr zero_typed)

/-!
零は展開型 `1+recursiveNat` の左注入を折り畳みます。後者は右注入へ既存の再帰的自然数を置いてから
折り畳みます。W型の自然数と同じ一層形を持ちますが、ここでは一般の型構文に `μ` を加え、折畳みを
対象言語の項として明示した点が異なります。

## 一段簡約は隣接するunrollとrollを打ち消す

`unroll (roll[T] v) → v` が再帰型固有の計算規則です。内側の項がまだ値でなければ、評価文脈に沿って
一段進めます。一段関係は入力、出力、保存すべき型を明確にするため、全体の評価関数より先に定義します。
-/

inductive Step : Term → Term → Prop where
  | inl : Step term term' → Step (.inl term) (.inl term')
  | inr : Step term term' → Step (.inr term) (.inr term')
  | pairLeft : Step left left' → Step (.pair left right) (.pair left' right)
  | pairRight : Value left → Step right right' → Step (.pair left right) (.pair left right')
  | roll : Step term term' → Step (.roll body term) (.roll body term')
  | unroll : Step term term' → Step (.unroll term) (.unroll term')
  | cancel : Value value → Step (.unroll (.roll body value)) value

example : Step (.unroll zero) (.inl .unit) :=
  .cancel (.inl .unit)

theorem preservation {term term' : Term} {type : RType}
    (typing : HasType term type) (reduction : Step term term') :
    HasType term' type := by
  induction reduction generalizing type with
  | inl step ih =>
      cases typing with
      | inl inner => exact .inl (ih inner)
  | inr step ih =>
      cases typing with
      | inr inner => exact .inr (ih inner)
  | pairLeft step ih =>
      cases typing with
      | pair left right => exact .pair (ih left) right
  | pairRight value step ih =>
      cases typing with
      | pair left right => exact .pair left (ih right)
  | roll step ih =>
      cases typing with
      | roll inner => exact .roll (ih inner)
  | unroll step ih =>
      cases typing with
      | unroll inner => exact .unroll (ih inner)
  | cancel value =>
      cases typing with
      | unroll rolled =>
          cases rolled with
          | roll inner => exact inner

/-!
`preservation` は一段簡約の前後で型が変わらないことを全構成子について証明します。最後の分岐では
`unroll` の型付けを逆に読み、その内側にある `roll` の前提から、結果 `value` が展開型を持つと
取り出します。値という前提は評価戦略を定めますが、この保存証明では型情報を追加しません。

## equi-recursive型は展開を型同値へ移す

equi-recursive型では `μX.T` と `T[μX.T/X]` を明示的な項なしで交換します。これをLean自身の
定義的等しさにしてしまわず、対象言語の型同値判断 `A ≈ B` として記述します。
-/

inductive TypeEquiv : RType → RType → Prop where
  | refl : TypeEquiv type type
  | symm : TypeEquiv left right → TypeEquiv right left
  | trans : TypeEquiv first second → TypeEquiv second third → TypeEquiv first third
  | sum : TypeEquiv left left' → TypeEquiv right right' →
      TypeEquiv (.sum left right) (.sum left' right')
  | product : TypeEquiv left left' → TypeEquiv right right' →
      TypeEquiv (.product left right) (.product left' right')
  | arrow : TypeEquiv domain domain' → TypeEquiv codomain codomain' →
      TypeEquiv (.arrow domain codomain) (.arrow domain' codomain')
  | mu : TypeEquiv body body' → TypeEquiv (.mu body) (.mu body')
  | unfold : TypeEquiv (.mu body) (unfoldType body)

theorem recursiveNat_equi_unfolded :
    TypeEquiv recursiveNat (.sum .unit recursiveNat) :=
  .unfold

example : recursiveNat ≠ .sum .unit recursiveNat := by decide

/-!
最後の不等式は重要です。対象言語で `recursiveNat ≈ 1+recursiveNat` を導出できても、型構文を表す
Lean値は等しくありません。equi-recursive体系の型検査には、有限グラフや無限正則木を比較する
アルゴリズムと、そのアルゴリズムが型同値を正しく判定する証明が別に必要です。本章の `TypeEquiv` は
同値判断の規則を与えますが、その決定手続きや完全性までを実装したものではありません。

負の位置を含む再帰型も構文上は書けます。たとえば `μX.X→A` は関数入力側に `X` を含みます。
そのような型は一般再帰を表現し、単純型付きラムダ計算の強正規化を失わせ得ます。これは直ちに型保存が
壊れるという主張ではありません。正規化、型安全性、型同値の可決定性は別々の性質です。

## 要点

* `μα.T` は型変数 `α` を本体 `T` の中で束縛し、一層展開は `T[μα.T/α]` である。
* de Bruijn添字による型置換では、束縛子の下で代入型をshiftして変数捕獲を避ける。
* iso-recursive型は展開と折畳みを `roll` と `unroll` の明示的な項で行う。
* equi-recursive型は同じ関係を型同値判断へ移すが、構文上の等しさにはしない。
* 型保存、強正規化、型同値の可決定性は互いに異なるメタ定理である。

## 研究史と文献案内

再帰型は再帰的データ、再帰的手続き、無限木としての型という複数の問題から発展しました。iso-recursive型と
equi-recursive型を比較する現代的な規則体系は [TAPL02] が読みやすい基準です。Amadio–Cardelli [AC93] は
再帰型の同値・部分型を、規則、アルゴリズム、無限木の意味論の対応として研究します。本章の小言語は
同論文の部分型計算を実装したものではなく、明示的展開と型保存へ範囲を限定しています。

## 問題

### 再帰リストを一層ずつ型付けする

要素型 `A` に対する本体 `1 + A × X` を `RType` で表し、空リストと二要素リストに相当する項を
`roll` で構成してください。各 `roll` の直前にある項の型を一層展開した式で書き、`HasType` の
導出木とLean証明を対応づけます。最外の `unroll` を一段進めた結果が同じ展開型を持つことを
`preservation` で確認すれば完了です。

### 型置換の変数捕獲を反例から調べる

束縛子の下でreplacementをshiftしない誤った置換を定義してください。開いた型変数 `.bound 0` を
`.mu (.bound 1)` へ代入し、正しい結果の `.bound 1` と誤った結果の `.bound 0` がどの位置を指すかを
図示します。両結果が異なることをLeanで証明し、`nestedExample` の各添字も同じ規則で追跡してください。
一般の置換補題に必要な自由変数の不変条件を述べれば完了です。

### isoとequiの型付け導出を翻訳する

`recursiveNat` の零と後者について、明示的な `roll` を持つiso-recursive導出を書いてください。次に
`TypeEquiv.unfold` と型変換規則を仮定したequi-recursive導出から `roll` を除きます。項の実行時構文、
型同値を調べる負担、型保存証明の各差を比較し、二体系を単なる表記違いと呼べない理由を説明します。
-/

end FormalLab.TypeTheory.RecursiveTypes