Solutions · Part 3
第3部 型付き計算の理論
第17–19章 · 9問
第17章
System Fとインプレディカティブ多相
問題本文問題1型抽象の下で二つの添字を追う
Problem
問題
章本文の位置で見る型変数を一つ、項変数を二つ持つ文脈を作り、さらに typeLam の下へ移してください。型変数添字と
項変数添字を別々の列にし、liftTypeContext が項変数型へ施す shiftTy を一段ずつ計算します。
持ち上げを省いた誤った文脈で、どの .var 0 の意味が変わるか示せば完了です。
ヒント
項変数と型変数の添字を別の名前空間で数え、型抽象を越えるときだけ型添字をずらします。
解答
Λα. λx:α. x では、項 x は直近の項束縛子を指す項添字0、注釈の α は直近の型束縛子を指す型添字0です。
内側へ Λβ を挿入すると、同じαを指す型添字は1へ変わりますが、項添字は変わりません。逆に λy を挿入すれば
項の x は1へ変わり、型添字は変わりません。二種類のshiftを混ぜると、構文上は自然数でも別の束縛子を指します。
依存型では項が型に現れます。それでも名前空間と持ち上げ操作を型で区別すると、捕獲事故を局所化できます。
問題2多相関数を三つの型へ特殊化する
Problem
問題
章本文の位置で見るpolymorphicIdentity を原子型、関数型、全称型自身へ型適用し、三つの HasType 導出を作ってください。
各場合に instantiate が計算する型を通常の記法へ戻します。三導出が一つの型抽象を共有する点と、
STLCで三つの型導出を別々に与える場合の差を説明してください。
ヒント
多相恒等関数 idF : ∀α. α→α の型適用と項適用を一段ずつ書きます。
解答
idF [Nat] 3 : Nat、idF [Bool] true : Bool、idF [Nat→Nat] succ : Nat→Nat です。型適用
(Λα.λx:α.x)[A] は型β簡約で λx:A.x となり、その後の項β簡約で引数を返します。三例で同じ項本体を使い、
型だけを差し替えています。三つ目ではα自体が関数型であり、多相性が基底型の列挙ではないことも分かります。
∀α. α→α→α など別の型では可能な実装を型から絞り、後のパラメトリシティの予想を立てます。
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問題3一様性が型付けだけから読めるか検討する
Problem
問題
章本文の位置で見る閉じた項が ∀X. X → X を持つとき、各型で異なる処理を選べる構文がSystem Fにあるかを規則から
調べてください。型検査時の型情報と実行時の項構文を区別し、恒等性を結論するために必要な関係解釈を
予想します。宇宙多相との比較表に量化対象、階層、実行時情報、許される特殊化を含めれば完了です。
ヒント
構文的に型を調べる演算を許す体系と、純粋なSystem Fを比較します。
解答
純粋なSystem Fでは型抽象されたαの値を分解する構文がなく、閉項はαごとに専用分岐を選べません。しかし 「型付け可能だから一様」という主張を定理にするには論理関係が必要です。型検査、型キャスト、一般再帰、例外を 拡張すると、同じ表面型でも観察可能な振る舞いが増えます。従って一様性は型の字面だけでなく、言語の操作的意味論と 観察同値に相対的な性質です。
実用言語の多相APIを評価するときは、型キャスト、底値、効果を含むfree theoremの条件を明記します。
第18章
論理関係と基本補題
問題本文問題1三つの関係を関数型へ持ち上げる
Problem
問題
章本文の位置で見る自然数上の等式、自然数から偶数への倍写像のグラフ、大小関係を Relation として定義してください。
各関係を入力と出力へ置いた四つの arrowRelation について、関連する関数対と関連しない関数対を
一つずつ示します。失敗例では、関係する入力と関係しない出力を具体的な反証証人として挙げてください。
ヒント
等号、全関係、空関係を R⇒S の定義へ代入し、始域と終域を別々に調べます。
解答
関数関係は (R⇒S)(f,g) ≔ ∀x y, R(x,y) → S(f x,g y) です。RとSが等号なら、同じ入力への出力が等しいという
外延的等号になります。RとSが全関係なら条件も結論も常に成り立ち、任意の関数対が関係します。Rが空関係なら
前提を満たす入力対がなく、Sによらず任意の関数対が関係します。一方、Rが全関係でSが空関係なら、始域が空で
ない限り関係する関数対はありません。
部分的関数や効果付き計算では出力関係へ停止や効果の観察を組み込み、同じ持ち上げを使います。
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問題2基本補題の抽象場合を導出する
Problem
問題
章本文の位置で見るΓ, x:A ⊢ t:B の帰納仮定から Γ ⊢ λx.t:A→B の関係保存を導いてください。任意の関連引数を
左右の代入へ追加し、帰納仮定へ渡す順序を数式で書きます。変数捕獲を避ける持ち上げが必要な位置を
第40章の代入と照合します。帰納仮定が出力関係を返した後、関数関係の全称量化をどの順で畳むかも
明示してください。抽象規則の仮定と結論を一度ずつ使う導出になれば完了です。
ヒント
型抽象の帰納仮定は、型変数へ任意の関係を割り当てた拡張環境で適用します。
解答
項が Λα.t で型が ∀α.A とします。二つの型 X,Y と任意の関係 R⊆X×Y を取ります。関係環境を
ρ[α↦R] と拡張すると、型付け導出の帰納仮定から二つの型代入後の本体
t[X/α] と t[Y/α] が ⟦A⟧_{ρ[α↦R]} で関係します。これは全称型の論理関係の定義そのものなので、
二つの型抽象が ⟦∀α.A⟧ρ で関係します。
存在型の抽象データ型では、実装型同士を結ぶ関係を一つ提示することで表現独立性を証明できます。
問題3単項と二項の論理関係を比較する
Problem
問題
章本文の位置で見るSTLC強正規化の計算可能性とSystem Fパラメトリシティの関係解釈を、項数、型変数環境、全称型、 導かれる定理という四項目で比較してください。どちらにも必要な基本補題の形を書き、一方の証明を そのまま他方へ転用できない分岐を特定します。共通構造と相違点を一つずつ説明できれば完了です。
ヒント
単項は一つの項の性質、二項は二つの項の対応を型に沿って持ち上げます。
解答
単項関係 P_A(t) は正規化や安全性のような性質を表し、基本補題から型付け可能な各項がその性質を持つと示します。
二項関係 R_A(t,u) は文脈同値、実装間対応、一様性を表します。二項関係の対角 R_A(t,t) が単項の主張を
与える場合もありますが、任意の単項述語が自然な二項対応を定めるわけではありません。目的とする観察が一項か
比較かによって選びます。
コンパイラ正当性ではソースとターゲットを結ぶ異種二項関係を使い、段階ごとの意味保存を合成します。
第19章
パラメトリシティとfree theorem
問題本文問題1グラフ関係からfree theoremを導出する
Problem
問題
章本文の位置で見るcommutesWithEveryFunction の証明を、関係の選択、入力の関連、出力の関連、方程式への展開という
四段階の数式へ戻してください。g を後者関数、リスト長、符号化関数へ変え、得られる等式を具体化します。
各具体化でグラフ関係の左右型を明記します。どの段階でも f の実装を使わず、型と関係保存だけを
使っていることを証明行ごとに確認すれば完了です。
ヒント
関数 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による型変更と可換である
ことを表します。
木や任意の関手的データ型でも、写像のグラフを関係として選ぶと自然性に似た等式を導けます。
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問題2一点関係の左右を変えて恒等性を再証明する
Problem
問題
章本文の位置で見る左を任意の型 A、右を単位型にした関係でも何が導けるか調べてください。次に本章の pointRelation を
真偽値で実装し、関係保存が f A x = x を強制する一段をLeanで再構成します。単位型の一意性を使う位置と、
右側の一点条件を使う位置を別々に示します。左右を交換した証明が同じ結論を与えるかを比較し、
与えない場合は量化のどの向きに情報が不足するか説明できれば完了です。
ヒント
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は各型で
恒等関数です。
多相型が許す実装を分類するときは、空関係、一点関係、グラフ関係を順に試すと制約を段階的に抽出できます。
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問題3効果がfree theoremを変える反例を作る
Problem
問題
章本文の位置で見る発散、例外、実行時型検査のうち一つをSystem Fへ加えた仮想言語を選び、∀X. X → X の新しい閉項を
構成してください。本章のどの関係または基本補題がその項を排除できなくなるかを特定します。純粋な結論、
効果を含む修正版、必要な観察同値を比較し、仮定を省略しないfree theoremを書けば完了です。
ヒント
発散を許し、∀α. α→α の閉項として常に発散する関数を考えます。
解答
一般再帰があれば bottom : ∀α. α を定義でき、Λα.λx:α.bottom[α] は型を保ちながら入力を返しません。
従って「この型の全項は恒等関数」という全停止を前提にした結論は壊れます。部分計算を含む関係で読むなら、
可能な振る舞いは入力を返すか発散するかです。状態や例外があれば、呼出回数や例外の観察もfree theoremへ
組み込む必要があります。
効果付き言語では、値だけでなく計算を関係づけるモナド的論理関係や段階付き関係を選びます。