正本：FormalLab/TypeTheory/RecursiveTypes.lean

第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].

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

Leankernel-checked counterpartL28–75

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で表現しています。

Leankernel-checked counterpartL107–130

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$ を実際の項として構成できます。本章ではリストの一層を作ることに必要な導入側だけを扱い、射影による除去規則は加えていません。

Leankernel-checked counterpartL139–149

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 が再帰型固有の計算規則です。内側の項がまだ値でなければ、評価文脈に沿って一段進めます。一段関係は入力、出力、保存すべき型を明確にするため、全体の評価関数より先に定義します。

Leankernel-checked counterpartL162–200

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 として記述します。

Leankernel-checked counterpartL213–230

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 を除きます。項の実行時構文、型同値を調べる負担、型保存証明の各差を比較し、二体系を単なる表記違いと呼べない理由を説明します。