import FormalLab.Recursion.DomainTheory import FormalLab.CategoryTheory.InitialAlgebras import FormalLab.CategoryTheory.FinalCoalgebras /-! # 第79章：再帰型の意味論——構文・近似・関手不動点を接続する 型方程式 $$ X\cong1+X. $$ は、自然数らしい一層構造を表します。しかし、この一行だけでは何を解とするかが決まりません。型構文では `μX.1+X` を一層展開する規則として読めます。順序理論では、連続作用素を最下元から反復した極限を最小不動点と して選びます。圏論では、自己関手 `F(X)=1+X` の不動点対象を考え、始代数ならば全ての構造再帰を一意にします。 これらは同じ記号を共有しますが、対象も普遍性も異なります。本章では、まず四つの意味を混同できない形に分けます。 次に有限段階の近似、明示的な折畳みと展開、始代数、代数的コンパクト性を順に接続します。最後に操作的意味論と 表示的意味論を比較し、再帰プログラムの表示が存在することと、その表示が実行結果を正しく予測することを区別します。 ## 構文上の一層展開は型の等号ではない 第14章の再帰型構文で $$ \mathsf{recursiveNat}:=\mu X.\,1+X. $$ と置きました。一層展開は型変数への代入であり、Leanの構文木としての等号ではありません。 -/ namespace FormalLab.Bridges.RecursiveTypeSemantics open _root_.CategoryTheory open _root_.CategoryTheory.Endofunctor open _root_.CategoryTheory.Limits open FormalLab.TypeTheory.RecursiveTypes open FormalLab.Recursion.DomainTheory open FormalLab.CategoryFoundations.InitialAlgebras universe u example : unfoldType natBody = .sum .unit recursiveNat := rfl example : recursiveNat ≠ .sum .unit recursiveNat := by decide /-! iso-recursive体系は `roll` と `unroll` を項に残し、equi-recursive体系は展開を型同値判断へ移します。どちらでも `μX.T` と `T[μX.T/X]` をLeanの構文木として定義的に同じにする必要はありません。この構文上の選択と、意味論で 二つの解釈対象が同型になることも別の主張です。 ## 関手不動点は折畳みと展開を互いに逆にする 自己関手 `F:Type→Type` の不動点対象を、型 `D` と二つの関数 $$ \mathsf{roll}:F(D)\to D, \qquad\mathsf{unroll}:D\to F(D). $$ および二つの逆法則として記録します。方程式の記号 `D≅F(D)` は、このデータの存在を省略したものです。 -/ structure FixedObject (F : Type u ⥤ Type u) where carrier : Type u roll : F.obj carrier → carrier unroll : carrier → F.obj carrier roll_unroll : ∀ value, roll (unroll value) = value unroll_roll : ∀ layer, unroll (roll layer) = layer def FixedObject.algebra {F : Type u ⥤ Type u} (D : FixedObject F) : Algebra F where a := D.carrier str := ↾D.roll def FixedObject.coalgebra {F : Type u ⥤ Type u} (D : FixedObject F) : Coalgebra F where V := D.carrier str := ↾D.unroll /-! `F(X)=1+X` では、零を左注入へ、後者を右注入へ展開します。折畳みは第55章の自然数代数の構造射です。 -/ def natUnroll : Nat → Unit ⊕ Nat | 0 => .inl () | n + 1 => .inr n def natFixedObject : FixedObject onePlusFunctor where carrier := Nat roll := natStructure unroll := natUnroll roll_unroll value := by cases value <;> rfl unroll_roll layer := by cases layer with | inl inhabitant => cases inhabitant; rfl | inr n => rfl example (n : Nat) : natFixedObject.roll (natFixedObject.unroll n) = n := natFixedObject.roll_unroll n example (layer : Unit ⊕ Nat) : natFixedObject.unroll (natFixedObject.roll layer) = layer := natFixedObject.unroll_roll layer example : IsInitial natFixedObject.algebra := natIsInitial /-! 最後の行は自然数が不動点であるだけでなく、`1+X`-代数の始対象であることを検査しています。始性から構造射が 同型になる向きはLambekの補題です。ここでは逆に、二つの逆関数を書いただけで始性を得たのではありません。 `natIsInitial` の証明は、任意の代数へのfoldの存在と自然数帰納法による一意性を別に使っています。 ## 始鎖は有限の深さから解へ近づく `F(X)=1+X` を空型から反復すると $$ 0\longrightarrow1+0\longrightarrow1+(1+0)\longrightarrow\cdots. $$ という始鎖を得ます。第 `n` 段階には、深さが `n` 未満の自然数だけが現れます。次の型族はこの反復を定義通りに 表します。 -/ def OnePlusStage : Nat → Type | 0 => Empty | n + 1 => Unit ⊕ OnePlusStage n def includeStage : {n : Nat} → OnePlusStage n → OnePlusStage (n + 1) | 0, value => nomatch value | _ + 1, .inl inhabitant => .inl inhabitant | n + 1, .inr value => .inr (includeStage (n := n) value) def stageValue : {n : Nat} → OnePlusStage n → Nat | 0, value => nomatch value | _ + 1, .inl _ => 0 | _ + 1, .inr value => stageValue value + 1 theorem includeStage_preserves_value {n : Nat} (value : OnePlusStage n) : stageValue (includeStage value) = stageValue value := by induction n with | zero => exact Empty.elim value | succ n ih => cases value with | inl inhabitant => rfl | inr rest => simp only [includeStage, stageValue] rw [ih rest] def natAtStage : (n : Nat) → OnePlusStage (n + 1) | 0 => .inl () | n + 1 => .inr (natAtStage n) theorem natAtStage_value (n : Nat) : stageValue (natAtStage n) = n := by induction n with | zero => rfl | succ n ih => simp [natAtStage, stageValue, ih] /-! `includeStage_preserves_value` は結合写像が既に得た情報を変えないことを示します。`natAtStage_value` は各自然数が 有限段階で現れることを示します。始鎖の余極限が自然数になる一般定理には、関手がこの種の余極限を保存することと、 余極限の普遍性が必要です。本章の二補題だけから任意の自己関手の不動点存在を結論しません。 ## 値の不動点と型方程式の解は異なる 領域理論のKleene不動点定理が扱うのは、固定した領域 `D` 上の連続な作用素 `f:D→D` です。 $$ \bot\sqsubseteq f(\bot)\sqsubseteq f^2(\bot)\sqsubseteq\cdots, \qquad \operatorname{fix}(f):=\bigsqcup_n f^n(\bot). $$ これは再帰関数の値を選ぶ定理です。一方、再帰領域方程式 `D≅F(D)` は領域そのものを未知数にします。前者では 反復されるものは値、後者では対象または領域です。両方に連続性と近似が現れても、型を値と同一視しません。 -/ example {D : Type u} (domain : PointedOmegaCPO D) (f : D → D) (continuous : ScottContinuous domain f) : f (kleeneFixedPoint domain f continuous) = kleeneFixedPoint domain f continuous := kleene_is_fixed domain f continuous /-! 有限燃料による計算は、値の近似を最も直接に観察できます。`delayedValue steps value fuel` は必要な段数を越えるまで 未定義で、その後は確定値を返します。 -/ def delayedValue (steps value fuel : Nat) : Option Nat := if steps < fuel then some value else none theorem delayedValue_increasing (steps value fuel : Nat) : FlatLe (delayedValue steps value fuel) (delayedValue steps value (fuel + 1)) := by by_cases current : steps < fuel · have next : steps < fuel + 1 := by omega simp [delayedValue, current, next, FlatLe] · by_cases next : steps < fuel + 1 · simp [delayedValue, current, next, FlatLe] · simp [delayedValue, current, next, FlatLe] example (steps value : Nat) : delayedValue steps value (steps + 1) = some value := by simp [delayedValue] theorem delayedValue_before (steps value fuel : Nat) (early : fuel ≤ steps) : delayedValue steps value fuel = none := by simp [delayedValue, Nat.not_lt.mpr early] /-! この列が平坦な情報順序で増大することは、燃料を増やすと既知の結果を撤回しないことです。一般の再帰プログラムを Kleene定理へ接続するには、プログラムから連続作用素を作り、各有限実行と反復近似の対応を証明しなければなりません。 単に `Option` を返す関数を書いただけでは、極限での意味や発散の完全な特徴づけは得られません。 ## 正の再帰出現は自己関手を作る `1+X` や `A×X` では、関数 `f:X→Y` を同じ向きの関数 `F(f):F(X)→F(Y)` へ写せます。これが型式を自己関手として 読むための基礎です。ところが関数型の入力位置は向きを反転します。 -/ def predicatePullback {X Y : Type u} (f : X → Y) : (Y → Bool) → (X → Bool) := fun predicate x => predicate (f x) theorem predicatePullback_id {X : Type u} : predicatePullback (fun x : X => x) = id := rfl theorem predicatePullback_comp {X Y Z : Type u} (f : X → Y) (g : Y → Z) : predicatePullback (g ∘ f) = predicatePullback f ∘ predicatePullback g := rfl /-! `X↦X→Bool` はこの写像について反変です。`μX.X→Bool` のような負の再帰出現を、通常の共変自己関手の始代数として 直ちに扱うことはできません。正値性検査は単なる実装上の保守性ではなく、型式を関手として作用させる向きを守ります。 関数空間を含む領域方程式では、未知領域が正と負の両方の位置に現れます。Smyth–Plotkin流の構成は、射に順序を持つ 圏と埋込み・射影対（embedding–projection pair）を用いてこの混合変性を制御します。集合と全関数の圏で形式的な式だけを書き、任意の 負の再帰型に解があるとは結論しません。 ## 代数的完備性と代数的コンパクト性 圏が自己関手 `F` に関して代数的に完備であるとは、始 `F`-代数が存在することです。代数的コンパクト性はさらに、 その始代数の構造射の逆が終 `F`-余代数になることを要求します。本章では一つの関手に対する証人を次のように分けます。 -/ def AlgebraicallyCompleteFor (F : Type u ⥤ Type u) : Prop := Nonempty (Σ A : Algebra F, IsInitial A) structure AlgebraicallyCompactSolution (F : Type u ⥤ Type u) where fixed : FixedObject F initial : IsInitial fixed.algebra terminal : IsTerminal fixed.coalgebra theorem compact_is_complete {F : Type u ⥤ Type u} (solution : AlgebraicallyCompactSolution F) : AlgebraicallyCompleteFor F := ⟨⟨solution.fixed.algebra, solution.initial⟩⟩ example : AlgebraicallyCompleteFor onePlusFunctor.{0} := ⟨⟨natAlgebra, natIsInitial⟩⟩ /-! 自然数は `1+X` の始代数ですが、同じ展開射を持つ余代数は終対象ではありません。終解には、有限回後者を観察した 後も止まらない無限要素が必要です。次のループ状態は毎段右注入を返すので、有限自然数へ観察を保存して写せません。 -/ def loopingCoalgebra : Coalgebra onePlusFunctor where V := Unit str := ↾fun _ => Sum.inr () theorem natUnroll_ne_self_inr (n : Nat) : natUnroll n ≠ Sum.inr n := by cases n <;> simp [natUnroll] theorem no_loop_to_nat (f : loopingCoalgebra ⟶ natFixedObject.coalgebra) : False := by have preservation := types_congr_hom f.h () exact natUnroll_ne_self_inr (f.f ()) preservation.symm theorem natFixed_not_terminal : IsEmpty (IsTerminal natFixedObject.coalgebra) := ⟨fun terminal => no_loop_to_nat (terminal.from loopingCoalgebra)⟩ /-! 従って「始代数の構造射は同型」というLambekの補題だけでは代数的コンパクト性になりません。始代数と終余代数が 同じ不動点で一致するのは強い性質です。領域意味論でこの一致を得るには、底、射の近似順序、適切な鎖の余極限、 関手の連続性などを組み合わせます。どの関手まで解けるかも圏の構造に依存します。 ## 操作的展開と表示的同型を対応させる iso-recursive言語の簡約 $$ \mathsf{unroll}(\mathsf{roll}(v))\longrightarrow v. $$ は、意味論では `unroll ∘ roll = id` によって健全になります。反対向きの `roll ∘ unroll = id` はη則に対応します。 対象言語がη簡約を持たなくても、表示モデルが外延的な等式を追加で同一視することはあります。したがってモデル内の 等しさから構文上の一段簡約を逆算せず、健全性と完全性を分けて調べます。 equi-recursive体系ではroll/unroll項を消し、型同値 `μX.T≈T[μX.T/X]` を型検査時に使います。意味論上の同型はその 妥当性を支えますが、型同値の決定手続きまでは与えません。無限正則木としての比較、分散、部分型が加わると、構文側の 可決定性と計算量を別に証明する必要があります。 ## 再帰意味論に必要な三種類の定理 再帰を含む言語のモデルを構成した後には、少なくとも次の三方向を区別します。 | 定理 | 比較するもの | 典型的な主張 | |---|---|---| | 健全性 | 構文の簡約と表示の等式 | `t→t'` なら `⟦t⟧=⟦t'⟧` | | 適切性 | 表示と観察可能な実行 | `⟦t⟧≠⊥` なら `t` は値へ到達する | | 完全抽象性 | 表示の等しさと文脈的等価 | `⟦t⟧=⟦u⟧` と全プログラム文脈での同じ観察が同値 | 不動点演算が存在するだけでは、これらは自動的に従いません。適切性には有限近似と有限実行の対応が必要です。 完全抽象性には、モデルが区別する差とプログラム文脈が観察できる差の一致が必要です。Leanで不動点方程式を証明した ことと、対象言語全体の意味論的正しさを証明したことを区別します。 ## 四つの不動点を見分ける | 層 | 未知のもの | 方程式・普遍性 | 解を選ぶ条件 | |---|---|---|---| | 再帰型構文 | 型式 | `μX.T ≈ T[μX.T/X]` | roll/unroll規則または型同値規則 | | 順序理論 | 領域の値 | `f(x)=x` | 最下元、ω鎖上限、連続性による最小解 | | 圏論的な不動点対象 | 圏の対象 | `F(D)≅D` | 同型だけでは一般に選択原理なし | | 始代数・終余代数 | 構造を持つ対象 | 全代数への一意射／全余代数からの一意射 | 普遍性による最小／最大の解 | ここで「最小」は常に同じ順序を指すわけではありません。Kleene最小不動点は領域内の情報順序によります。始代数の 「最小性」は代数圏の始性という射の一意性です。Smyth–Plotkinの圏論的構成は、hom集合の順序と対象の普遍性を 組み合わせて両者を接続します。 ## 要点 * 構文上の再帰型、領域内の値の不動点、関手の不動点対象、始代数は異なる定義である。 * 不動点対象は `roll:F(D)→D` と `unroll:D→F(D)` の逆法則を持つが、同型だけでは始性も終性も得られない。 * `F(X)=1+X` の始鎖は有限深さの近似を作り、その各段階は既知の自然数を保存して次段階へ埋め込まれる。 * Scott連続作用素のKleene不動点は再帰値を選び、再帰領域方程式は領域そのものを未知数にする。 * 負の再帰出現は関数の向きを反転するため、通常の共変自己関手としての始代数解釈を妨げる。 * 代数的コンパクト性は、始代数の逆構造が終余代数にもなることを要求する。 * 表示の存在、不動点方程式、健全性、適切性、完全抽象性はそれぞれ別に証明すべき主張である。 ## 研究史と文献案内 Scottの技術報告 [SCO70] は、データを情報の近似順序で捉え、連続写像と不動点をラムダ計算の表示的意味論へ 用いる研究計画を提示しました。Scottの連続格子論 [SCO72] は、その順序論的・位相的基礎を発展させます。 SmythとPlotkin [SP82] は、CPO上の連続写像の最小不動点から、順序豊穣圏上の連続関手の始不動点へ類比を拡張しました。 さらにembeddingの圏と極限・余極限の一致を用いて、再帰領域方程式を圏論的に解く枠組みを与えます。論文は1979年に 投稿され、1982年に刊行されたため両年を区別します。 Freyd [FRE91] は代数的完備性を一般の圏論的性質として研究し、再帰型と帰納型の関係を整理する後続研究の基準点です。 1990年のComo会議と1991年の会議録刊行を区別します。再帰型の構文的なiso/equiの比較と型同値については [AC93] と [TAPL02] を参照してください。本章のLeanコードは一般のO-categoryや逆極限構成を形式化したものではありません。 ## 問題 ### 始鎖の最初の五段階を完全に記述する `OnePlusStage 0` から `OnePlusStage 4` までを通常の余積記法で展開し、各型の要素を列挙してください。 `includeStage` が各要素をどこへ送るかを書き、`stageValue` との可換性を全要素について確かめます。最後に任意の自然数 `n` が 第 `n+1` 段階で初めて現れることを、存在とそれ以前の不在へ分けて証明してください。 ### 不動点同型から始性が従わない反例を強化する 恒等関手では全対象が不動点になる一方、全てが始代数ではないことを示してください。次に同じ台集合へ異なる自己写像を 代数構造として入れ、準同型の可換条件を比較します。不動点対象、代数、始代数の順に追加されるデータと命題を列挙し、 Lambekの補題の逆が失敗する箇所を明示できれば完了です。 ### `1+X` の終解に無限要素を加える 型 `Nat∞` を有限自然数と一つの無限要素から構成し、`Nat∞→1+Nat∞` とその逆を定義してください。有限要素では `natUnroll` と一致し、無限要素は右注入の中で自分自身へ戻るようにします。任意の `1+X`-余代数からの写像を、左注入へ 到達するか右注入を永遠に返すかで定め、終性の証明に必要な古典性または余帰納的原理を特定してください。 ### 負の再帰出現の向きを型で追跡する `X↦X→Bool`、`X↦Bool→X`、`X↦(X→Bool)→Bool` の三つについて、関数 `f:X→Y` から作れる写像の向きを書いてください。 共変、反変、二重反変を区別し、関手法則をLeanで証明します。混合変性の式を一変数の共変自己関手とみなせない理由を、 必要な射がどちら向きに不足するかまで示してください。 ### 有限燃料とKleene反復を接続する 一つの小さな再帰プログラムと、その意味作用素 `Φ` を平坦な関数領域上に定義してください。燃料 `n` の実行結果が `Φⁿ(⊥)` の対応する入力での値に等しいことを帰納法で証明します。その後に連続性を示し、反復上限の非底性と停止の同値を 証明してください。どの段階で有限実行の性質を使い、どこで領域の上限を使うかを分離できれば完了です。 ### 操作的意味論と表示的意味論の境界を監査する 第14章のiso-recursive小言語へ表示関数を定義し、`unroll (roll v)→v` に対する健全性を逆法則から証明してください。 次に表示モデルがη則を満たす場合、それが構文の一段簡約、文脈的等価、または単なるモデル内等式のどれを与えるかを 判定します。完全性または完全抽象性を主張するために不足する補題を具体的に列挙してください。 -/ end FormalLab.Bridges.RecursiveTypeSemantics