import FormalLab.TypeTheory.SimplyTypedLambdaCalculus import FormalLab.TypeTheory.StructuralRules import FormalLab.TypeTheory.OperationalSemantics import FormalLab.TypeTheory.RecursiveTypes import FormalLab.TypeTheory.TypeSafety import FormalLab.TypeTheory.Normalization import FormalLab.TypeTheory.SystemF import FormalLab.TypeTheory.LogicalRelations import FormalLab.TypeTheory.Parametricity /-! # 全問題の解答：型システム ## 第11章：単純型付きラムダ計算——型判断を規則として読む ### 問題1：証明項を型導出木へ戻す #### ヒント 文脈は自由変数の型を並べた有限列、型判断は文脈の下で項が型を持つという主張、型導出はその主張を 規則から組み立てた木です。 #### 解答 `identity_has_type` は、文脈 `[A]` の添字0へ変数規則を使い、抽象規則で仮定を閉じる導出です。結論は `[] ⊢ λ.0 : A ⇒ A` です。`constant_has_type` では `[B,A]` の添字1が外側の `A` を指し、二回の抽象で `[] ⊢ λ.λ.1 : A ⇒ B ⇒ A` を得ます。`identity_applied_has_type` の適用規則では関数枝が `A ⇒ A`、引数枝が `A` を持ち、共有する中間型は `A` です。同じ判断に、規則の選択や無関係な変換が ある体系なら複数の導出があり得ます。 証明項を読むときは、構成子を推論規則へ、構成子の引数を前提導出へ戻します。圏論的意味論では同じ木を 射の合成へ翻訳できます。 ### 問題2：型の付く項と付かない項の境界を探る #### ヒント 内側の文脈では添字0が `x : A`、添字1が `f : A ⇒ B` を指します。自己適用では入力型と関数型を同じ変数へ 同時に要求します。 #### 解答 項は `λf.λx.f x`、de Bruijn表現では `.lam (.lam (.app (.var 1) (.var 0)))` です。内側で `.var 1 : A ⇒ B` と `.var 0 : A` を適用し、二回抽象して `(A ⇒ B) ⇒ A ⇒ B` を得ます。 一方 `λx.x x` では、同じ `x` が適用の関数として `X ⇒ Y`、引数として `X` を持つ必要があります。 従って `X = X ⇒ Y` が必要です。有限木として作る単純型では右辺が左辺を真部分木として含み、型の大きさが `|X| = |X| + |Y| + 1` を満たせないため解がありません。 再帰型を許す体系では型方程式を明示的に解けますが、roll/unrollが必要です。同じ項が型付け可能になる条件を、 体系の型形成規則まで含めて述べます。 ### 問題3：型安全性の三つの主張を分ける #### ヒント 代入は導出の構造、保存は一段簡約、進行は閉項の現在状態について述べます。 #### 解答 置換補題は `Γ,x:A ⊢ t:B` と `Γ ⊢ s:A` から `Γ ⊢ t[x:=s]:B` を導きます。保存定理は `Γ ⊢ t:A` と `t→t'` から `Γ ⊢ t':A`、進行定理は `[] ⊢ t:A` なら `t` が値であるか `∃t',t→t'` と述べます。保存と進行を反復すれば、型付き閉項は有限到達した各段階で行き詰まりません。 しかし無限に進み続ける可能性を排除しないため停止は従いません。強正規化は全ての簡約列が有限だと追加します。 外在的判断は無型項と型を別に関係づけ、Church流の型付き構文は項自体に型情報を持たせます。 依存型では通常の関数型を定数族のΠ型として回収できます。外在的・内在的表現の比較は、後の型安全性証明で 証明量が変わる理由にもなります。 #### 補足 保存だけでは最初から行き詰まった型付き項を排除できず、進行だけでは一段進んだ後に同じ型判断を再利用できません。 全実行の安全性には、進行で次の一歩を得て、保存でその到達点へ型を運ぶ反復が必要です。言語へ新しい構文を 加えるときは、進行証明の値の形と保存証明の代入場合を別々に監査します。 ## 第12章：弱化・交換・縮約・代入 ### 問題1：四つの変換を導出木として復元する #### ヒント 文脈の変換と、各変数を新しい文脈のどの添字へ送るかを同じ表にします。 #### 解答 弱化は `Γ ⊢ t:A` から `B,Γ ⊢ rename succ t:A` を作り、全自由添字を1増やします。先頭交換は `A,B,Γ` を `B,A,Γ` へ替え、添字0と1を交換し2以上を保ちます。縮約は同型の二仮定 `A,A,Γ` を `A,Γ` へまとめ、添字0と1をともに0へ、2以上を1減らして送ります。先頭代入は `A,Γ ⊢ t:B` と `Γ ⊢ s:A` から `Γ ⊢ t[0:=s]:B` を作ります。文脈だけを交換して項の添字を保つと、 元の添字0が `A` から `B` へ変わり、変数規則の結論型が壊れます。 文脈の並べ替えを実装するときは、型の列だけでなく変数の証拠も同じ写像で移します。この原則は再添字付けや ファイブレーションにも現れます。 ### 問題2：ラムダの下の代入を一段ずつ追跡する #### ヒント 新しい束縛変数は添字0のままにし、外側から来る置換項だけを弱化します。 #### 解答 外側の自由変数を添字0、ラムダ内の束縛変数を新しい添字0とすると、外側の変数はラムダ下で添字1になります。 `liftSubstitution σ` は内側の0を `.var 0` へ送り、外側の `n+1` を `weaken (σ n)` へ送ります。 たとえば置換項が外側の `.var 0` なら、ラムダ下では `.var 1` に弱化されます。弱化しない素朴な代入では `.var 0` のままになり、新しいラムダに捕獲されます。不変条件は「再帰先の文脈で各像が元と同じ型を持つ」です。 型変数の下で項変数型を持ち上げるSystem Fでも、同じ「新しい0を固定し外側を弱化する」構造を使います。 ### 問題3：構造規則を制限した体系を比較する #### ヒント 各仮定を0回、1回、複数回使えるかで三体系を比較します。 #### 解答 通常のSTLCは弱化と縮約を許すため仮定を0回または複数回使えます。アフィン型は弱化を許して縮約を禁じるため、 各仮定は高々1回です。線形型は両方を禁じ、各仮定をちょうど1回使います。`K=λx.λy.x` は `y` を 使わないため線形体系では型付けできませんが、アフィン体系では可能です。`W=λf.λx.f x x` は `x` を 二回使うためアフィン・線形の両方で不可能です。交換を許せば順序は変えられますが、使用回数は変えられません。 資源型では構成子を削るだけでなく、文脈分割と使用回数の不変条件を型へ持たせます。第76章の線形論理へ 同じ表を持ち越せます。 ## 第13章：操作的意味論・一段簡約・評価戦略 ### 問題1：一つの評価列を二つの表現で追う #### ヒント 値呼びでは関数位置を先に値へし、次に引数位置、最後にβ簡約します。 #### 解答 例として `((λx.x) (λy.y)) ((λz.z) (λw.w))` を取ります。最初は外側の関数位置を `appLeft` で `λy.y` へ進めます。次に外側の関数が値なので、引数内部を `appRight` で `λw.w` へ進めます。 最後に両方が値なので `beta` で `λw.w` を得ます。各段の `step?` はこの唯一の次項を返します。最終項は ラムダなので値かつβ正規形であり、単なる行き詰まりではありません。 条件分岐や積を追加した評価器でも、優先順位を推論関係の前提と実行関数の分岐順の双方で照合します。 ### 問題2：名前呼びと値呼びの停止挙動を分離する #### ヒント 使われない引数の位置へ自己適用 `omega` を置きます。 #### 解答 `K=λx.λy.x`、値 `v`、発散項 `Ω` とします。項 `(K v) Ω` は名前呼びなら `(λy.v) Ω → v` と進み、Ωを評価せず停止します。値呼びでは関数が `λy.v` になった後に引数Ωを値へ しようとして無限に進みます。一方 `(λx.x) Ω` は名前呼びでも `Ω` へ簡約するため発散します。 従って名前呼びが常に停止するわけではなく、未使用引数を捨てられる配置だけで差が出ます。 遅延評価や短絡評価でも、評価されない式が効果を持つと観察結果まで変わります。停止性だけでなく効果の順序も 別の列で比較します。 ### 問題3：関係と実行関数の対応を証明する #### ヒント 実行関数の各成功分岐から対応する `Step` 構成子を作り、逆向きは `Step` の導出へ帰納します。 #### 解答 健全性は項 `t` への構造帰納で示します。適用の関数位置が進めば帰納仮定と `appLeft`、関数が値で引数が 進めば `appRight`、両方が値のラムダなら `beta` を使います。関数位置がラムダ値なら `valueCannotStep` により `appLeft` の前提は不可能です。完全性は `Step t u` の導出帰納で、各構成子に対し `step? t = some u` を計算します。二方向と関数結果の一意性から、二つの関係後続は同じだと分かります。 仕様関係とインタプリタを併置するときは、健全性だけでなく完全性も検査します。片方向だけでは実装が合法な 一歩を見落としていても検出できません。 ## 第14章：再帰型・fold/unfold・型の無限展開 ### 問題1：再帰リストを一層ずつ型付けする #### ヒント `ListF A X = 1 + A × X` と置き、再帰リスト型を `μX.ListF A X` とします。 #### 解答 空リストは展開型 `1 + A × μX.(1+A×X)` の左注入を作り、`roll` で再帰型へ戻します。要素 `a` と尾 `xs` から 作るconsは右注入 `inr ⟨a,xs⟩` を同じ展開型で作り、再び `roll` します。二要素リストはこの操作を二回重ねます。 最外の `unroll (roll body)` は一段で `body` へ進み、保存定理により展開型 `1 + A × μX.(1+A×X)` を保ちます。 木では一層関手を `1 + A × X × X` などへ替えるだけで、roll前の一層と再帰位置の対応を同じ方法で追えます。 ### 問題2：型置換の変数捕獲を反例から調べる #### ヒント `μ` の下では新しい添字0が導入されるため、外から入れる型の自由添字を1増やします。 #### 解答 正しい置換は `μ body` の下へ入るとき、対象添字を1増やしreplacementを `shift 1 0` します。これを省くと、 replacement中の自由な `.bound 0` が内側のμに捕獲されます。最小例では、正しい結果 `.mu (.bound 1)` の添字1は外側を指し続けますが、誤った結果 `.mu (.bound 0)` は直近のμを指します。 `nestedExample` の添字も同じく、0は最内、1は一つ外の束縛子を指します。不変条件は、置換前に自由だった 各型変数が置換後も対応する外部束縛を指すことです。 項代入、型代入、再添字付けのいずれでも、束縛子を越えるときの持ち上げを自由変数保存の補題として先に定めます。 ### 問題3：isoとequiの型付け導出を翻訳する #### ヒント iso-recursive型では型の折り畳みを項構文に、equi-recursive型では型同値判断に置きます。 #### 解答 `recursiveNat = μX.(1+X)` とすると、零は `roll (inl unit)`、後者は `roll (inr n)` です。iso体系では 導入・除去に `roll` と `unroll` が明示され、その簡約が実行時構文に現れます。equi体系では `μX.(1+X) ≡ 1+μX.(1+X)` を `TypeEquiv.unfold` で認め、型変換規則により注入項を再帰型として扱います。 項は短くなりますが、型検査器は再帰的な型同値を決定する必要があります。保存証明も、isoではroll/unroll規則、 equiでは型同値の閉性を扱うため、単なる表記差ではありません。 抽象データ型やnewtypeでも、変換を実行時に持つか型等式に吸収するかを、検査負担と意味論の両面から比較します。 ## 第15章：保存・進行・型安全性 ### 問題1：進行証明の全分岐を導出木へ戻す #### ヒント 適用 `f a` について、まず関数側の進行を場合分けし、関数が値のときだけ引数側へ進みます。 #### 解答 関数側が進めるなら `f a → f' a` を `appLeft` で作ります。関数側が値で引数側が進めるなら `f a → f a'` を `appRight` で作ります。両方が値なら、関数値の標準形補題から `f` はラムダであり、 `beta` により本体へ引数を代入します。形式上の四組合せのうち、関数が進める場合には値ではないため引数側の 選言を調べる必要がなく、残る三分岐だけが評価戦略に沿います。名前呼びなら引数の進行分岐を飛ばしてβへ進みます。 新しい値構成子を追加したら、対応する標準形補題と進行分岐を対で増やします。規則だけ追加して補題を更新しない 不整合を防げます。 ### 問題2：外在的な保存定理を復元する #### ヒント 外在的定式化では、簡約前後の無型項と共通の型を明示的に関係づけます。 #### 解答 定理は `HasType Γ t A → Step t t' → HasType Γ t' A` です。βの場合は `Γ,x:B ⊢ body:A` と `Γ ⊢ arg:B` から `Γ ⊢ body[x:=arg]:A` を得る代入補題が必要です。 関数位置・引数位置の簡約では、それぞれの部分項に対する保存の帰納仮定を適用し、適用規則を再構成します。 本章の内在的な一段関係は、始域と終域が同じ型で添字付けされているため、保存が関係の型そのものに組み込まれます。 証明が短いのは主張が弱いからではなく、不変条件をデータ表現へ移したからです。 内在的構文を選ぶと不可能状態を表現できなくなりますが、変換・等式の依存型が複雑になります。証明量だけでなく APIと帰納原理も比較します。 ### 問題3：言語拡張が壊す箇所を診断する #### ヒント 真偽値の構成子と条件分岐の三つの簡約規則を揃え、どれか一つを欠かした反例を作ります。 #### 解答 型に `Bool`、項に `true`、`false`、`if c then t else u` を加えます。条件式はまず `c` を進め、 `if true then t else u → t`、`if false then t else u → u` とします。標準形補題は、閉じたBool型の値が trueかfalseであることです。`if false` の規則を欠かすと、両枝が同じ型を持つ閉項 `if false then true else false : Bool` が値でも進めもしないため、進行が失敗します。型は変化していないので 保存の反例ではありません。規則を戻せば標準形、進行、到達状態の非行き詰まりを順に回復できます。 和・積・例外を加えるときも、型付け規則と値、標準形と簡約規則、保存と進行を同じ順で更新します。 ## 第16章：正規形・弱正規化・強正規化 ### 問題1：三種類の停止主張を反例で分ける #### ヒント 正規形を持つこと、正規形へ至る経路があること、すべての経路が停止することを別々に量化します。 #### 解答 正規形は後続を持たない項です。弱正規化は正規形へ至る有限列の存在、強正規化はその項から始まる無限列の 不存在です。β簡約を任意の位置で許すと、`(λx.y) Ω` は外側を先に縮約して `y` へ至るので弱正規化します。 しかし捨てられる引数Ωだけを縮約し続ける無限列もあるため、強正規化しません。正規形そのものは強正規化し、 強正規化する項は最長の簡約列を辿れば正規形へ至るので弱正規化します。 決定的評価戦略の停止と、非決定的な全簡約関係の強正規化を混同しないよう、関係と戦略を先に固定します。 ### 問題2：計算可能性述語の関数型場合を読む #### ヒント 関数自身の停止だけでなく、計算可能な引数を計算可能な結果へ送ることを定義に含めます。 #### 解答 基底型では `Comp_A(t)` を「`t : A` かつ `t` は強正規化する」と置きます。関数型では `Comp_{A→B}(f) ≔ f : A→B ∧ ∀a, Comp_A(a) → Comp_B(f a)` と定めます。単に `f` の強正規化だけを 要求しても、適用後に現れる計算を制御できません。恒等関数では任意の計算可能な `a` に対し `(λx.x) a → a` なので、簡約に対する閉性から結果も計算可能です。 積型なら各射影、和型なら各場合分けについて計算可能性を定めます。型構成子の観察方法が述語の形を決めます。 ### 問題3：正規化器から等式判定器までの欠落を埋める #### ヒント 停止する正規化手続きだけでは足りません。正しさ、一意性、正規形の構文的比較可能性を列挙します。 #### 解答 型付き項 `t,u` を正規化し、得た正規形をα同値を除いて比較します。必要なのは、正規化器の停止、出力が入力と 変換可能である健全性、変換可能な項が同じ正規形を持つ完全性です。完全性には合流性と正規形の一意性を使えます。 さらに束縛変数をde Bruijn添字などで表し、正規形の構文等値を決定できなければなりません。これらから `t ≡ u` であることと正規形の一致が同値になり、判定器が得られます。 型検査器の変換可能性判定でも同じ分解を使います。η規則を加えるなら正規形と合流性を再確認します。 ## 第17章：System Fとインプレディカティブ多相 ### 問題1：型抽象の下で二つの添字を追う #### ヒント 項変数と型変数の添字を別の名前空間で数え、型抽象を越えるときだけ型添字をずらします。 #### 解答 `Λα. λx:α. x` では、項 `x` は直近の項束縛子を指す項添字0、注釈の `α` は直近の型束縛子を指す型添字0です。 内側へ `Λβ` を挿入すると、同じαを指す型添字は1へ変わりますが、項添字は変わりません。逆に `λy` を挿入すれば 項の `x` は1へ変わり、型添字は変わりません。二種類のshiftを混ぜると、構文上は自然数でも別の束縛子を指します。 依存型では項が型に現れます。それでも名前空間と持ち上げ操作を型で区別すると、捕獲事故を局所化できます。 ### 問題2：多相関数を三つの型へ特殊化する #### ヒント 多相恒等関数 `idF : ∀α. α→α` の型適用と項適用を一段ずつ書きます。 #### 解答 `idF [Nat] 3 : Nat`、`idF [Bool] true : Bool`、`idF [Nat→Nat] succ : Nat→Nat` です。型適用 `(Λα.λx:α.x)[A]` は型β簡約で `λx:A.x` となり、その後の項β簡約で引数を返します。三例で同じ項本体を使い、 型だけを差し替えています。三つ目ではα自体が関数型であり、多相性が基底型の列挙ではないことも分かります。 `∀α. α→α→α` など別の型では可能な実装を型から絞り、後のパラメトリシティの予想を立てます。 ### 問題3：一様性が型付けだけから読めるか検討する #### ヒント 構文的に型を調べる演算を許す体系と、純粋なSystem Fを比較します。 #### 解答 純粋なSystem Fでは型抽象されたαの値を分解する構文がなく、閉項はαごとに専用分岐を選べません。しかし 「型付け可能だから一様」という主張を定理にするには論理関係が必要です。型検査、型キャスト、一般再帰、例外を 拡張すると、同じ表面型でも観察可能な振る舞いが増えます。従って一様性は型の字面だけでなく、言語の操作的意味論と 観察同値に相対的な性質です。 実用言語の多相APIを評価するときは、型キャスト、底値、効果を含むfree theoremの条件を明記します。 ## 第18章：論理関係と基本補題 ### 問題1：三つの関係を関数型へ持ち上げる #### ヒント 等号、全関係、空関係を `R⇒S` の定義へ代入し、始域と終域を別々に調べます。 #### 解答 関数関係は `(R⇒S)(f,g) ≔ ∀x y, R(x,y) → S(f x,g y)` です。RとSが等号なら、同じ入力への出力が等しいという 外延的等号になります。RとSが全関係なら条件も結論も常に成り立ち、任意の関数対が関係します。Rが空関係なら 前提を満たす入力対がなく、Sによらず任意の関数対が関係します。一方、Rが全関係でSが空関係なら、始域が空で ない限り関係する関数対はありません。 部分的関数や効果付き計算では出力関係へ停止や効果の観察を組み込み、同じ持ち上げを使います。 ### 問題2：基本補題の抽象場合を導出する #### ヒント 型抽象の帰納仮定は、型変数へ任意の関係を割り当てた拡張環境で適用します。 #### 解答 項が `Λα.t` で型が `∀α.A` とします。二つの型 `X,Y` と任意の関係 `R⊆X×Y` を取ります。関係環境を `ρ[α↦R]` と拡張すると、型付け導出の帰納仮定から二つの型代入後の本体 `t[X/α]` と `t[Y/α]` が `⟦A⟧_{ρ[α↦R]}` で関係します。これは全称型の論理関係の定義そのものなので、 二つの型抽象が `⟦∀α.A⟧ρ` で関係します。 存在型の抽象データ型では、実装型同士を結ぶ関係を一つ提示することで表現独立性を証明できます。 ### 問題3：単項と二項の論理関係を比較する #### ヒント 単項は一つの項の性質、二項は二つの項の対応を型に沿って持ち上げます。 #### 解答 単項関係 `P_A(t)` は正規化や安全性のような性質を表し、基本補題から型付け可能な各項がその性質を持つと示します。 二項関係 `R_A(t,u)` は文脈同値、実装間対応、一様性を表します。二項関係の対角 `R_A(t,t)` が単項の主張を 与える場合もありますが、任意の単項述語が自然な二項対応を定めるわけではありません。目的とする観察が一項か 比較かによって選びます。 コンパイラ正当性ではソースとターゲットを結ぶ異種二項関係を使い、段階ごとの意味保存を合成します。 ## 第19章：パラメトリシティとfree theorem ### 問題1：グラフ関係からfree theoremを導出する #### ヒント 関数 `h : A→B` のグラフ `R(a,b) ≔ h a=b` を型変数の関係として選びます。 #### 解答 `f : ∀α. List α→List α` とします。パラメトリシティをhのグラフへ適用すると、関係するリスト、すなわち `xs : List A` と `map h xs : List B` に対し、出力も要素ごとにhのグラフで関係します。従って `map h (f_A xs) = f_B (map h xs)` を得ます。これはfが要素の具体的な型を調べず、mapによる型変更と可換である ことを表します。 木や任意の関手的データ型でも、写像のグラフを関係として選ぶと自然性に似た等式を導けます。 ### 問題2：一点関係の左右を変えて恒等性を再証明する #### ヒント `f : ∀α. α→α` に対し、任意の `a:A` と一要素型の点を結ぶ関係を選びます。 #### 解答 一要素型 `Unit` と `R⊆A×Unit` を `R(x,()) ≔ x=a` で定めます。`a` と `()` は関係するので、 パラメトリシティから `f_A a` と `f_Unit ()` も関係し、定義より `f_A a=a` です。左右を逆にして `R'⊆Unit×A` を `R'((),x) ≔ x=a` としても同じ結論になります。任意のAとaについて成り立つためfは各型で 恒等関数です。 多相型が許す実装を分類するときは、空関係、一点関係、グラフ関係を順に試すと制約を段階的に抽出できます。 ### 問題3：効果がfree theoremを変える反例を作る #### ヒント 発散を許し、`∀α. α→α` の閉項として常に発散する関数を考えます。 #### 解答 一般再帰があれば `bottom : ∀α. α` を定義でき、`Λα.λx:α.bottom[α]` は型を保ちながら入力を返しません。 従って「この型の全項は恒等関数」という全停止を前提にした結論は壊れます。部分計算を含む関係で読むなら、 可能な振る舞いは入力を返すか発散するかです。状態や例外があれば、呼出回数や例外の観察もfree theoremへ 組み込む必要があります。 効果付き言語では、値だけでなく計算を関係づけるモナド的論理関係や段階付き関係を選びます。 -/ namespace FormalLab.Appendix.Solutions.Chapter011Exercise001 open FormalLab.Foundation.UntypedLambdaCalculus open FormalLab.TypeTheory.SimplyTypedLambdaCalculus example (A : SimpleType) : HasType [] identity (A ⇒ A) := .lam (.var .zero) example (A B : SimpleType) : HasType [] constant (A ⇒ B ⇒ A) := .lam (.lam (.var (.succ .zero))) example (A : SimpleType) : HasType [] (.app identity identity) (A ⇒ A) := .app (identity_has_type (A ⇒ A)) (identity_has_type A) end FormalLab.Appendix.Solutions.Chapter011Exercise001 namespace FormalLab.Appendix.Solutions.Chapter011Exercise002 open FormalLab.Foundation.UntypedLambdaCalculus open FormalLab.TypeTheory.SimplyTypedLambdaCalculus def applyTerm : Term := .lam (.lam (.app (.var 1) (.var 0))) theorem applyTermHasType (A B : SimpleType) : HasType [] applyTerm ((A ⇒ B) ⇒ A ⇒ B) := .lam (.lam (.app (.var (.succ .zero)) (.var .zero))) example (X Y : SimpleType) : X ≠ X ⇒ Y := X.ne_self_arrow Y end FormalLab.Appendix.Solutions.Chapter011Exercise002 namespace FormalLab.Appendix.Solutions.Chapter012Exercise001 #check FormalLab.TypeTheory.StructuralRules.weakenFront #check FormalLab.TypeTheory.StructuralRules.exchangeFront #check FormalLab.TypeTheory.StructuralRules.contraction #check FormalLab.TypeTheory.StructuralRules.substituteTop end FormalLab.Appendix.Solutions.Chapter012Exercise001 namespace FormalLab.Appendix.Solutions.Chapter012Exercise002 open FormalLab.TypeTheory.SimplyTypedLambdaCalculus open FormalLab.TypeTheory.StructuralRules def outerVariableUnderBinder (A C : SimpleType) : Tm [A] (C ⇒ A) := .lam (.var (.succ .zero)) example {A C : SimpleType} (argument : Tm [] A) : substituteTop (B := C ⇒ A) argument (outerVariableUnderBinder A C) = .lam (weakenFront (B := C) argument) := rfl end FormalLab.Appendix.Solutions.Chapter012Exercise002 namespace FormalLab.Appendix.Solutions.Chapter013Exercise001 open FormalLab.Foundation.UntypedLambdaCalculus open FormalLab.TypeTheory.OperationalSemantics def threeApplications : Term := .app (.app identity identity) constant example : step? threeApplications = some (.app identity constant) := rfl example : step? (.app identity constant) = some constant := rfl example : step? constant = none := rfl end FormalLab.Appendix.Solutions.Chapter013Exercise001 namespace FormalLab.Appendix.Solutions.Chapter013Exercise003 open FormalLab.Foundation.UntypedLambdaCalculus open FormalLab.TypeTheory.OperationalSemantics theorem step?_complete {term next : Term} (reduction : FormalLab.TypeTheory.OperationalSemantics.Step term next) : step? term = some next := by induction term generalizing next with | var index => cases reduction | lam body => cases reduction | app function argument functionIH argumentIH => cases reduction with | beta value => cases value; rfl | appLeft functionStep => cases function with | var index => cases functionStep | lam body => exact False.elim (valueCannotStep .lam functionStep) | app left right => change (match step? (.app left right) with | some function' => some (Term.app function' argument) | none => none) = _ rw [functionIH functionStep] | appRight functionValue argumentStep => cases functionValue cases argument with | var index => cases argumentStep | lam body => exact False.elim (valueCannotStep .lam argumentStep) | app left right => change (match step? (.app left right) with | some argument' => some (Term.app (Term.lam _) argument') | none => none) = _ rw [argumentIH argumentStep] theorem stepDeterministic {term first second : Term} (left : FormalLab.TypeTheory.OperationalSemantics.Step term first) (right : FormalLab.TypeTheory.OperationalSemantics.Step term second) : first = second := by have leftResult := step?_complete left have rightResult := step?_complete right rw [leftResult] at rightResult exact Option.some.inj rightResult end FormalLab.Appendix.Solutions.Chapter013Exercise003 namespace FormalLab.Appendix.Solutions.Chapter014Exercise001 open FormalLab.TypeTheory.RecursiveTypes def listBody (element : RType) : RType := .sum .unit (.product element (.bound 0)) def emptyList (element : RType) : Term := .roll (listBody element) (.inl .unit) def unitListBody : RType := listBody .unit def emptyUnitList : Term := emptyList .unit def prepend (element : RType) (head tail : Term) : Term := .roll (listBody element) (.inr (.pair head tail)) def prependUnit (tail : Term) : Term := prepend .unit .unit tail def twoUnitList : Term := prependUnit (prependUnit emptyUnitList) theorem emptyUnitListHasType : HasType emptyUnitList (.mu unitListBody) := by exact .roll (.inl .unit) theorem prependUnitHasType {tail : Term} (typedTail : HasType tail (.mu unitListBody)) : HasType (prependUnit tail) (.mu unitListBody) := by exact .roll (.inr (.pair .unit typedTail)) theorem twoUnitListHasType : HasType twoUnitList (.mu unitListBody) := by exact prependUnitHasType (prependUnitHasType emptyUnitListHasType) example : HasType zero recursiveNat := zero_typed example : HasType (successor zero) recursiveNat := one_typed example : HasType (.inl .unit) (unfoldType natBody) := preservation (.unroll zero_typed) (.cancel (.inl .unit)) example : HasType (.inl .unit) (unfoldType unitListBody) := preservation (.unroll emptyUnitListHasType) (.cancel (.inl .unit)) end FormalLab.Appendix.Solutions.Chapter014Exercise001 namespace FormalLab.Appendix.Solutions.Chapter014Exercise002 open FormalLab.TypeTheory.RecursiveTypes def naiveSubstitute (target : Nat) (replacement : RType) : RType → RType | .unit => .unit | .sum left right => .sum (naiveSubstitute target replacement left) (naiveSubstitute target replacement right) | .product left right => .product (naiveSubstitute target replacement left) (naiveSubstitute target replacement right) | .arrow domain codomain => .arrow (naiveSubstitute target replacement domain) (naiveSubstitute target replacement codomain) | .bound index => if index = target then replacement else .bound index | .mu body => .mu (naiveSubstitute (target + 1) replacement body) example : naiveSubstitute 0 (.bound 0) (.mu (.bound 1)) = .mu (.bound 0) := rfl example : substitute 0 (.bound 0) (.mu (.bound 1)) = .mu (.bound 1) := rfl end FormalLab.Appendix.Solutions.Chapter014Exercise002 namespace FormalLab.Appendix.Solutions.Chapter016Exercise001 inductive ChoiceStep : Bool → Bool → Prop where | finish : ChoiceStep true false | loop : ChoiceStep true true theorem falseIsNormal : ¬∃ next, ChoiceStep false next := by rintro ⟨next, step⟩ cases step def infiniteLoop : Nat → Bool := fun _ => true theorem infiniteLoopSteps : ∀ n, ChoiceStep (infiniteLoop n) (infiniteLoop (n + 1)) := fun _ => .loop end FormalLab.Appendix.Solutions.Chapter016Exercise001 namespace FormalLab.Appendix.Solutions.Chapter017Exercise002 open FormalLab.TypeTheory.SystemF example : HasType emptyContext (.typeApp polymorphicIdentity .atom) (.atom ⟹ .atom) := identityAtAtomHasType example : HasType emptyContext (.typeApp polymorphicIdentity (.atom ⟹ .atom)) ((.atom ⟹ .atom) ⟹ (.atom ⟹ .atom)) := identityAtArrowHasType example : HasType emptyContext (.typeApp polymorphicIdentity (.all (.var 0 ⟹ .var 0))) (.all (.var 0 ⟹ .var 0) ⟹ .all (.var 0 ⟹ .var 0)) := identityAtUniversalHasType end FormalLab.Appendix.Solutions.Chapter017Exercise002 namespace FormalLab.Appendix.Solutions.Chapter018Exercise001 open FormalLab.TypeTheory.LogicalRelations def doubleGraph : Relation := graphRelation (fun n : Nat => 2 * n) def lessOrEqualRelation : Relation where Left := Nat Right := Nat relates := (· ≤ ·) example : (graphRelation (fun n : Nat => 2 * n)).relates (3 : Nat) (6 : Nat) := by change 2 * 3 = 6 decide example : ¬(graphRelation (fun n : Nat => 2 * n)).relates (3 : Nat) (7 : Nat) := by change 2 * 3 ≠ 7 decide example : RelatedFunctions lessOrEqualRelation lessOrEqualRelation (fun n : Nat => n + 1) (fun n : Nat => n + 1) := by change ∀ ⦃left right : Nat⦄, left ≤ right → left + 1 ≤ right + 1 intro left right related omega end FormalLab.Appendix.Solutions.Chapter018Exercise001 namespace FormalLab.Appendix.Solutions.Chapter019Exercise001 open FormalLab.TypeTheory.Parametricity theorem freeTheorem (f : (α : Type) → α → α) (parametric : PreservesAllRelations f) {A B : Type} (g : A → B) (x : A) : g (f A x) = f B (g x) := commutesWithEveryFunction f parametric g x end FormalLab.Appendix.Solutions.Chapter019Exercise001 namespace FormalLab.Appendix.Solutions.Chapter019Exercise002 open FormalLab.TypeTheory.LogicalRelations open FormalLab.TypeTheory.Parametricity def booleanPointRelation (point : Bool) : Relation where Left := PUnit Right := Bool relates := fun _ value => value = point theorem booleanEndomapFixesPoint (f : (α : Type) → α → α) (parametric : PreservesAllRelations f) (point : Bool) : f Bool point = point := by have related := parametric (booleanPointRelation point) have inputRelated : (booleanPointRelation point).relates PUnit.unit point := rfl exact related inputRelated end FormalLab.Appendix.Solutions.Chapter019Exercise002 namespace FormalLab.Appendix.Solutions.Chapter011Exercise003 variable {Term Ty : Type} def Preservation (HasType : Term → Ty → Prop) (Step : Term → Term → Prop) : Prop := ∀ ⦃term next type⦄, HasType term type → Step term next → HasType next type def Progress (HasType : Term → Ty → Prop) (Step : Term → Term → Prop) (Value : Term → Prop) : Prop := ∀ ⦃term type⦄, HasType term type → Value term ∨ ∃ next, Step term next def Stuck (Step : Term → Term → Prop) (Value : Term → Prop) (term : Term) : Prop := ¬Value term ∧ ¬∃ next, Step term next end FormalLab.Appendix.Solutions.Chapter011Exercise003