MoreStlc: 単純型付きラムダ計算についてさらに
Set Warnings "-notation-overridden,-parsing".
From PLF Require Import Maps.
From PLF Require Import Types.
From PLF Require Import Smallstep.
From PLF Require Import Stlc.
From Coq Require Import Strings.String.
単純型付きラムダ計算は理論的性質を興味深いものにするには十分な構造を持っていますが、プログラミング言語といえるようなものではありません。
この章では、型における扱いが明らかないくつもの馴染み深い機能を導入することで、実世界の言語とのギャップを埋め始めます。
数値
複雑な式を書くとき、部分式に名前をつけられると便利なことがよくあります。
同じことを繰り返すのを避けることができ、またしばしば可読性が向上します。
ほとんどの言語はこのための1つ以上の方法を持っています。
例えばOCaml（およびCoq）では、 let x=t1 in t2 と書くと「式t1を簡約して、その結果を名前xに束縛してt2を簡約する」ことを意味します。
ここで導入するlet束縛子はOCamlに従って値呼び(call-by-value)評価順序とします。
つまり、let本体の評価が始まる前にlet束縛項は完全に評価されます。
型付け規則T_Letは、letの型が次の手順で計算されることを示しています:
まずlet束縛項の型の計算、次にその型の束縛によるコンテキストの拡張、さらにこの拡張されたコンテキストでのlet本体の型の計算をします（これがlet式全体の型になります）。
本資料のこの時点では、新しい機能の定義のためにたくさんの日本語の文章を読み通すより、同じ情報を伝える規則を単に見る方が、おそらく簡単でしょう。以下がその規則です:
構文:
t ::= 項
| ... （前と同じ他の項）
| let x=t in t let束縛
簡約:
t1 --> t1'
---------------------------------- (ST_Let1)
let x=t1 in t2 --> let x=t1' in t2
---------------------------- (ST_LetValue)
let x=v1 in t2 --> [x:=v1]t2
型付け:
Gamma |- t1 \in T1 x|->T1; Gamma |- t2 \in T2
-------------------------------------------------- (T_Let)
Gamma |- let x=t1 in t2 \in T2
ここまでのCoqを用いた関数プログラミングの例では、値の対(pairs)を頻繁に使ってきました。
そのような対の型は「直積型(product type)」と呼ばれます。
対の形式化はほとんど議論する余地がないほど簡単です。
しかし、共通パターンを強調するため、定義のいろいろな部分をちょっと見てみましょう。
Coqでは、対の構成要素を抽出する基本的な方法は、パターンマッチング(pattern matching)です。
別の方法としては、fstとsnd、つまり、1番目と2番目の要素の射影操作を基本操作として持つ方法があります。
お遊びで、対をこの方法でやってみましょう。
例えば、数値の対をとり、その和と差の対を返す関数の書き方は次の通りです:
\x : Nat*Nat.
let sum = x.fst + x.snd in
let diff = x.fst - x.snd in
(sum,diff)
これから、単純型付きラムダ計算に対を追加するには、2つの新しい項の形を追加することが含まれます。
1つは対で (t1,t2) と書きます。もう1つは射影で、第1射影は t.fst、第2射影は t.sndと書きます。
さらに1つの型コンストラクタ T1*T2 を追加します。
これをT1とT2の直積と呼びます。
構文:
t ::= 項
| ...
| (t,t) 対
| t.fst 第1射影
| t.snd 第2射影
v ::= 値
| ...
| (v,v) 対値
T ::= 型
| ...
| T * T 直積型
簡約については、対と射影がどう振る舞うかを規定するいくつかの新しい規則が必要です。
t1 --> t1'
-------------------- (ST_Pair1)
(t1,t2) --> (t1',t2)
t2 --> t2'
-------------------- (ST_Pair2)
(v1,t2) --> (v1,t2')
t1 --> t1'
------------------ (ST_Fst1)
t1.fst --> t1'.fst
------------------ (ST_FstPair)
(v1,v2).fst --> v1
t1 --> t1'
------------------ (ST_Snd1)
t1.snd --> t1'.snd
------------------ (ST_SndPair)
(v1,v2).snd --> v2
規則ST_FstPairとST_SndPairは、完全に簡約された対が第1射影または第2射影に遭遇したとき、結果が対応する要素であると言っています。
合同規則ST_Fst1とST_Snd1は、射影の対象の項が完全に評価されきっていないとき、対象の簡約を認めるものです。
ST_Pair1とST_Pair2は対の構成部分の簡約です。
最初に左の部分を簡約し、それが値となったら、次に右の部分を簡約します。
これらの規則内におけるメタ変数vとtの使い方は、対に関して左から右に評価する戦略(left-to-right evaluation strategy)であることを規定します。
（暗黙の慣習として、vやv1などのメタ変数は値のみを指すものとしています。）
また値の定義に節を加え、(v1,v2) が値であることを規定しています。
値の対自体が値でなければならないという事実は、関数の引数として渡された対が、関数の本体の実行が開始される前に完全に簡約されることを保証します。
対と射影の型付け規則はそのまま直ぐに得られます。
Gamma |- t1 \in T1 Gamma |- t2 \in T2
----------------------------------------- (T_Pair)
Gamma |- (t1,t2) \in T1*T2
Gamma |- t \in T1*T2
--------------------- (T_Fst)
Gamma |- t.fst \in T1
Gamma |- t \in T1*T2
--------------------- (T_Snd)
Gamma |- t.snd \in T2
T_Pairは、t1が型T1を持ち、t2が型T2を持つならば、 (t1,t2) が型 T1*T2 を持つことを言っています。
逆に、T_FstとT_Sndは、tが直積型T1*T2を持つ（つまり評価結果が対になる）ならば、射影の型はT1とT2になることを定めます。
Unit型
もう一つの便利な基本型は、MLファミリーの言語に特に見られるものですが、1要素の型Unitです。
この型は要素を1つ持ちます。それは項定数unitです（先頭の文字は小文字のuです）。
型付け規則は unitをUnitの要素と定めます。
取りうる値の集合にもunitを加えます。
実際、unitは型Unitの式の評価結果としてとり得る唯一の値です。
構文:
t ::= 項
| ... （前と同様）
| unit unit値
v ::= 値
| ...
| unit unit
T ::= 型
| ...
| Unit Unit型
型付け:
---------------------- (T_Unit)
Gamma |- unit \in Unit
1つの要素だけしか持たない型を定義することにわずらわされるのは、少々奇妙なことに見えるかもしれません。
結局のところ、このような型に属する計算は自明なものだけではないのでしょうか？
これは妥当な質問です。
実際STLCではUnit型は特別、問題ではありません（ちょっと後でこの型の使い道を二つ見ることになりますが）。
Unitが本当に便利なのはよりリッチな言語で副作用(side effects)を持つ場合です。
例えば、変更可能な変数やポインタについての代入文や、例外その他のローカルではないコントロール機構を持つ場合、などです。
そのような言語では、副作用のためだけに評価される式の(どうでもよい)結果のための型が便利なのです。
多くのプログラムでは2つの異なった形を持つ値を扱うことが求められます。
例えば大学のデータベースから学生を調べるのに、名前か、「または」、IDナンバーを使うという場合があります。
検索関数は、マッチした値か、「または」、エラーコードを返すかもしれません。
これらは、2項の直和型(sum type または disjoint union)の例です。
直和型は2つの与えられた型の一方から抽出した値の集合にあたります。
例えば次のようなものです。
Nat + Bool
この型の要素を、それぞれの構成部分の型の要素にタグ付けする(tagging)ことで生成します。
例えば、nがNatならば inl n は Nat+Bool の要素です。
同様に、bがBoolならば inr b は Nat+Bool の要素です。
タグの名前inlとinrは、これらのタグを関数と考えるところから出ています。
inl \in Nat -> Nat + Bool
inr \in Bool -> Nat + Bool
これらの関数は、NatまたはBoolの要素を直和型Nat+Boolの左部分または右部分に注入("inject")します。
（しかし、実際にはこれらを関数としては扱いません。
inlとinrはキーワードで、inl t と inr t は基本構文形であり、関数適用ではありません。）
Coqでのプログラミングで見たように、直和型の重要な用途の一つに、エラー通知があります。
div \in Nat -> Nat -> (Nat + Unit)
div =
\x:Nat. \y:Nat.
test iszero y then
inr unit
else
inl ...
この型 Nat + Unit は Coq における option nat と同型です。
つまり、簡単に両方向へ変換する関数が書けます。
直和型の要素を「利用する」ために、分解する構文としてcase構文を導入します（これはCoqのmatchの非常に単純化された形です）。
例えば、以下の手続きは、Nat+Bool をNatに変換します:
getNat \in Nat+Bool -> Nat
getNat =
\x:Nat+Bool.
case x of
inl n => n
| inr b => if b then 1 else 0
より形式的に...
構文:
t ::= 項
| ... （前と同様）
| inl T t タグ付け（左）
| inr T t タグ付け（右）
| case t of case
inl x => t
| inr x => t
v ::= 値
| ...
| inl T v タグ付き値（左）
| inr T v タグ付き値（右）
T ::= 型
| ...
| T + T 直和型
簡約:
t1 --> t1'
------------------------ (ST_Inl)
inl T2 t1 --> inl T2 t1'
t2 --> t2'
------------------------ (ST_Inr)
inr T1 t2 --> inr T1 t2'
t0 --> t0'
------------------------------------------- (ST_Case)
case t0 of inl x1 => t1 | inr x2 => t2 -->
case t0' of inl x1 => t1 | inr x2 => t2
----------------------------------------------- (ST_CaseInl)
case (inl T2 v1) of inl x1 => t1 | inr x2 => t2
--> [x1:=v1]t1
----------------------------------------------- (ST_CaseInr)
case (inr T1 v2) of inl x1 => t1 | inr x2 => t2
--> [x2:=v1]t2
型付け:
Gamma |- t1 \in T1
------------------------------ (T_Inl)
Gamma |- inl T2 t1 \in T1 + T2
Gamma |- t2 \in T2
------------------------------- (T_Inr)
Gamma |- inr T1 t2 \in T1 + T2
Gamma |- t \in T1+T2
x1|->T1; Gamma |- t1 \in T
x2|->T2; Gamma |- t2 \in T
---------------------------------------------------- (T_Case)
Gamma |- case t of inl x1 => t1 | inr x2 => t2 \in T
inlとinrに型を付記する理由は、関数に対して行ったのと同様、型付け規則を単純にするためです。
この情報がなければ、型推論規則T_Inlは、例えば、t1が型T1の要素であることを示した後、「任意の」型T2について inl t1 が T1 + T2 の要素であることを導出できます。
例えば、inl 5 : Nat + Nat と inl 5 : Nat + Bool の両方（および無数の型）が導出できます。
この奇妙さ（技術的に言えば型の一意性の欠如）は、型チェックアルゴリズムを、ここまでやってきたように「規則を下から上に読む」という単純な方法で構築することができなくなることを意味します。
この問題を扱うのにはいろいろな方法があります。
簡単なものの1つは、ここで採用する方法ですが、単射を実行するときに直和型の「別の側」をプログラマが明示的に付記することを強制するというものです。
これはプログラマにはかなり重い作業です（そのため実際の言語は別の解法を採用しています）。
しかし、理解と形式化は容易な方法です。
ここまで見てきた型付け機能は、Boolのような基本型(base types)と、古い型から新しい型を構築する->や*のような型コンストラクタ(type constructors)に分類できます。
もう一つの有用な型コンストラクタがListです。
すべての型Tについて、型 List T はTから抽出したものを要素とする有限長リストを表します。
原理的には、直積型や直和型、再帰型(recursive types)を用いることでリストを定義できます。
しかし、再帰型に意味を与えることは簡単ではありません。
その代わりに、リストの特別な場合を直接議論します。
以下にリストの構文、意味、型付け規則を与えます。
nilに対して明示的に型を付記することが必須であり、consには付記できないという点を除けば、ここで定義されたリストは本質的にCoqで構築したものと同じです。
リストを分解するためにlcaseを使います。
これは「空リストのheadは何か？」というような問題を扱うことを避けるためです。
従って、例えば、数値リストの最初の2つの要素の和を計算する関数は次の通りです:
\x:List Nat.
lcase x of nil => 0
| a::x' => lcase x' of nil => a
| b::x'' => a+b
構文:
t ::= 項
| ...
| nil T
| cons t t
| lcase t of nil => t
| x::x => t
v ::= 値
| ...
| nil T nil値
| cons v v cons値
T ::= 型
| ...
| List T Tのリスト
簡約:
t1 --> t1'
-------------------------- (ST_Cons1)
cons t1 t2 --> cons t1' t2
t2 --> t2'
-------------------------- (ST_Cons2)
cons v1 t2 --> cons v1 t2'
t1 --> t1'
------------------------------------------- (ST_Lcase1)
(lcase t1 of nil => t2 | xh::xt => t3) -->
(lcase t1' of nil => t2 | xh::xt => t3)
----------------------------------------- (ST_LcaseNil)
(lcase nil T of nil => t2 | xh::xt => t3)
--> t2
------------------------------------------------ (ST_LcaseCons)
(lcase (cons vh vt) of nil => t2 | xh::xt => t3)
--> [xh:=vh,xt:=vt]t3
型付け:
------------------------- (T_Nil)
Gamma |- nil T \in List T
Gamma |- t1 \in T Gamma |- t2 \in List T
--------------------------------------------- (T_Cons)
Gamma |- cons t1 t2 \in List T
Gamma |- t1 \in List T1
Gamma |- t2 \in T
(h|->T1; t|->List T1; Gamma) |- t3 \in T
--------------------------------------------------- (T_Lcase)
Gamma |- (lcase t1 of nil => t2 | h::t => t3) \in T
（Coqを含む）ほとんどのプログラミング言語に現れるもう1つの機構が、再帰関数を定義する機能です。
例えば、階乗関数を次のように定義できるとよいと思うでしょう:
直接「再帰的定義」を形式化することも可能ですが、なかなかの作業が必要になります。
特にstep内で再帰関数定義の「環境(environment)」を持ち回る必要があるでしょう。
fact = \x:Nat.
test x=0 then 1 else x * (fact (pred x)))
この束縛子の中では、上で導入したletと異なり、右辺の変数factが束縛されることになります。
ここでは、冗長ではありますが、同じくらい強力で、直接の形式化が容易な形での再帰関数の定義方法を取ります。
再帰的定義を書く代わりに、fixという名前の「不動点演算子(fixed-point operator)」を定義します。
不動点演算子は、簡約の過程で必要に応じて再帰的定義の右辺に「展開」("unfold")するものです。
例えば、
fact = \x:Nat.
test x=0 then 1 else x * (fact (pred x)))
のように書く代わりに、次のように書きます。
fact =
fix
(\f:Nat->Nat.
\x:Nat.
test x=0 then 1 else x * (f (pred x)))
前者の書き方から、以下のようにして後者の書き方を得ます。
直観的にはfixに渡される高階関数fはfact関数の生成器(generator)です。
fが、factに求められる振る舞いをnまで「近似」する関数（つまり、n以下の入力に対しては正しい結果を返すがnより大きい入力に関してはどうでもいい関数）に適用されるとき、fはより良い近似、つまり、n+1まで正しい答えを返す関数、を返します。
fixをこの生成器に適用すると、生成器の「不動点(fixed point)」を返します。
この不動点は、すべての入力nについて求められる振る舞いをする関数です。
（ここでは不動点("fixed point")という用語を通常の数学と同じ意味で使っています。
通常の数学では、関数fの不動点とは、f(x) = x となる入力 x のことです。
ここでは、型 (Nat->Nat)->(Nat->Nat) を持つ関数Fの不動点は、Nat->Nat型の関数fのうち、F fがfと同じように振る舞うものです。）
構文:
t ::= 項
| ...
| fix t 不動点演算子
簡約:
t1 --> t1'
------------------ (ST_Fix1)
fix t1 --> fix t1'
-------------------------------------------- (ST_FixAbs)
fix (\xf:T1.t2) --> [xf:=fix (\xf:T1.t2)] t2
型付け:
Gamma |- t1 \in T1->T1
---------------------- (T_Fix)
Gamma |- fix t1 \in T1
fact 3 = fix F 3 の動きを追うことで、 ST_FixAbs がどのように動くのか見ます。
ここで、Fは以下の式とします。
F = (\f. \x. test x=0 then 1 else x * (f (pred x)))
（可読性のために型注釈は省略します。）
fix F 3
--> ST_FixAbs + ST_App1
(\x. test x=0 then 1 else x * (fix F (pred x))) 3
--> ST_AppAbs
test 3=0 then 1 else 3 * (fix F (pred 3))
--> ST_Test0_Nonzero
3 * (fix F (pred 3))
--> ST_FixAbs + ST_Mult2
3 * ((\x. test x=0 then 1 else x * (fix F (pred x))) (pred 3))
--> ST_PredNat + ST_Mult2 + ST_App2
3 * ((\x. test x=0 then 1 else x * (fix F (pred x))) 2)
--> ST_AppAbs + ST_Mult2
3 * (test 2=0 then 1 else 2 * (fix F (pred 2)))
--> ST_Test0_Nonzero + ST_Mult2
3 * (2 * (fix F (pred 2)))
--> ST_FixAbs + 2 x ST_Mult2
3 * (2 * ((\x. test x=0 then 1 else x * (fix F (pred x))) (pred 2)))
--> ST_PredNat + 2 x ST_Mult2 + ST_App2
3 * (2 * ((\x. test x=0 then 1 else x * (fix F (pred x))) 1))
--> ST_AppAbs + 2 x ST_Mult2
3 * (2 * (test 1=0 then 1 else 1 * (fix F (pred 1))))
--> ST_Test0_Nonzero + 2 x ST_Mult2
3 * (2 * (1 * (fix F (pred 1))))
--> ST_FixAbs + 3 x ST_Mult2
3 * (2 * (1 * ((\x. test x=0 then 1 else x * (fix F (pred x))) (pred 1))))
--> ST_PredNat + 3 x ST_Mult2 + ST_App2
3 * (2 * (1 * ((\x. test x=0 then 1 else x * (fix F (pred x))) 0)))
--> ST_AppAbs + 3 x ST_Mult2
3 * (2 * (1 * (test 0=0 then 1 else 0 * (fix F (pred 0)))))
--> ST_Test0Zero + 3 x ST_Mult2
3 * (2 * (1 * 1))
--> ST_MultNats + 2 x ST_Mult2
3 * (2 * 1)
--> ST_MultNats + ST_Mult2
3 * 2
--> ST_MultNats
6
重要な点として、CoqのFixpointと異なり、fixでの定義は発散するような関数も書けます。
練習問題: ★, standard, optional (halve_fix)
halve =
\x:Nat.
test x=0 then 0
else test (pred x)=0 then 0
else 1 + (halve (pred (pred x)))
Exercise: 1 star, standard, optional (fact_steps)
任意のTについて型 T->T の関数の不動点が記述できる形ができたことから、驚くようなことが起こります。
特に、すべての型が何らかの項に住まれている(inhabited)ということが導かれます。
これを確認するため、すべての型Tについて、項
fix (\x:T.x)
が定義できることを見てみましょう。
T_FixとT_Absから、この項は型Tを持ちます。
ST_FixAbsより、この項を簡約すると何度やっても自分自身になります。
したがって、この項はTの発散要素(diverging element)です。
より有用なこととして、次はfixを使って2引数の再帰関数を定義する例です:
fix (\x:T.x)
equal =
fix
(\eq:Nat->Nat->Bool.
\m:Nat. \n:Nat.
test m=0 then iszero n
else test n=0 then fls
else eq (pred m) (pred n))
そして最後に、次はfixを使って再帰関数の対を定義する例です（この例は、規則T_Fixの型T1は関数型ではなくてもよいことを示しています）:
evenodd =
fix
(\eo: (Nat->Bool * Nat->Bool).
let e = \n:Nat. test n=0 then tru else eo.snd (pred n) in
let o = \n:Nat. test n=0 then fls else eo.fst (pred n) in
(e,o))
even = evenodd.fst
odd = evenodd.snd
STLCの基本拡張の最後の例として、
レコード(records)とその型をどのように形式化するかをちょっと見てみましょう。
直観的には、レコードは組に二つの一般化をほどこすことで得られます。
（二つの代わりに）n-要素の組とすること、そして（位置の代わりに）「ラベル(label)」で要素へアクセスできることです。
構文:
t ::= 項
| ...
| {i1=t1, ..., in=tn} レコード
| t.i 射影
v ::= 値
| ...
| {i1=v1, ..., in=vn} レコード値
T ::= 型
| ...
| {i1:T1, ..., in:Tn} レコード型
直積からの一般化はかなり明確です。
しかし、ここで実際に記述したものは、以前の章で書いたものよりかなり非形式的であることは注意しておくべきです。
いろいろなところで、"..."を「これらを何個か」という意味で使っていますし、レコードに同じラベルが繰り返し出てきてはいけない、という通常の付加条件を明示的に述べることを省いています。
ti --> ti'
------------------------------------ (ST_Rcd)
{i1=v1, ..., im=vm, in=ti , ...}
--> {i1=v1, ..., im=vm, in=ti', ...}
t1 --> t1'
-------------- (ST_Proj1)
t1.i --> t1'.i
------------------------- (ST_ProjRcd)
{..., i=vi, ...}.i --> vi
これらの規則も、やはりちょっと非形式的です。
例えば、最初の規則は「tiが値でないフィールドのうち最も左のもので、tiはti'にステップで進むならば、レコード全体のステップは...」と読まれることを意図しています。
最後の規則では、i と呼ばれるフィールドは1つだけで、他のすべてのフィールドは値を持っていることを意図しています。
Gamma |- t1 \in T1 ... Gamma |- tn \in Tn
---------------------------------------------------- (T_Rcd)
Gamma |- {i1=t1, ..., in=tn} \in {i1:T1, ..., in:Tn}
Gamma |- t \in {..., i:Ti, ...}
------------------------------- (T_Proj)
Gamma |- t.i \in Ti
上述の定義を精密にする方法はいくつもあります。
- 構文の形と推論規則を、上記の形になるべく近いまま直接形式化するという方法があります。
これは概念的に「直球」で、もし本当のコンパイラを作るならば、おそらくいちばん合っているでしょう。
特に、形式化の中にエラーメッセージのプリントを含めることができるので、プログラマが理解するのが容易になるでしょう。
しかし、規則の形式化版はまったくきれいにはなりませんし、扱いも難しいものになります。
というのも、...で省略した部分を全て明示的に定量化し、理解しなければならないからです。
このため、レコードによる拡張は本章の追加課題にも入れていません。
（それでもここで非形式的に議論しておくのは、Sub章における部分型付けのモチベーションになるからです。）
- 別の方法として、レコードを表現する、よりスムーズな方法を探すことができます。
例えば、1つのコンストラクタでレコード全体を一度に作るのではなく、空レコードに対応する1つのコンストラクタと、存在するレコードに1つのフィールドを追加する別のコンストラクタの2つで表現するという方法があります。
この方法は、レコードについての計算のメタ理論に一番の興味がある場合には正しい方法です。
なぜなら、この方法をとると、きれいで優雅な定義と証明が得られるからです。
Records章では、この方法がどのように行えるかを示しています。
- 最後に、望むならば、レコードを形式化することを完全に避けることができます。 このためには、レコード記法は、対と直積型を含むより複雑な式の単なる非形式的な略記法である、と規定します。 次節では、このアプローチの概略を与えます。
では、レコードをunitと対で表現する方法を見ていきましょう。
（この素晴らしい表現は、Luca Cardelliによる提案です。
この表現により部分型付けを追加することもできます。）
最初に、任意のサイズの「組(tuple)」が対とunit値のネストでエンコードできることを確認します。
対の記法 (t1,t2) を混用するのを避けるため、組を書き下すためにはラベルを持たない中カッコ({..})を使います。
つまり、{}は0個組、{5}は一つ組、{5,6}は二つ組（事実上対と同じ）、{5,6,7}は三つ組、等です。
次に、レコードラベルに何らかの全順序があり、そのため各ラベルに一意に自然数が関連づけられると仮定します。
この数をラベルの「ポジション(position)」と呼びます。
例えば、以下のようにポジションが定められるとします:
レコードの型についてもまったくおなじことをします:
{} ----> unit
{t1, t2, ..., tn} ----> (t1, trest)
ただし {t2, ..., tn} ----> trest
同様に、組の型を直積型のネストでエンコードすることができます。
{} ----> Unit
{T1, T2, ..., Tn} ----> T1 * TRest
ただし {T2, ..., Tn} ----> TRest
組のフィールドの射影演算は、第2射影の列に続く第1射影としてエンコードできます:
t.0 ----> t.fst
t.(n+1) ----> (t.snd).n
LABEL POSITION
a 0
b 1
c 2
... ...
bar 1395
... ...
foo 4460
... ...
このポジションを、レコード値を組(つまりネストされた対)でエンコードするために使います。
つまり、フィールドをそのポジションでソートします。
例えば:
{a=5, b=6} ----> {5,6}
{a=5, c=7} ----> {5,unit,7}
{c=7, a=5} ----> {5,unit,7}
{c=5, b=3} ----> {unit,3,5}
{f=8,c=5,a=7} ----> {7,unit,5,unit,unit,8}
{f=8,c=5} ----> {unit,unit,5,unit,unit,8}
以下のことに注意します。
各フィールドはそのラベルに関連づけられたポジションに現れます。
また、組の大きさは、最大のポジションを持つラベルによって決定されます。
そして、使われていないポジションはunitで埋められます。
{a:Nat, b:Nat} ----> {Nat,Nat}
{c:Nat, a:Nat} ----> {Nat,Unit,Nat}
{f:Nat, c:Nat ----> {Unit,Unit,Nat,Unit,Unit,Nat}
最後に、レコードの射影は適切なポジションについての組の射影でエンコードされます:
t.l ----> t.(position of l)
レコードのオリジナルの「直接の」表現に対するすべての型付け規則が、このエンコードで正しいことをチェックするのは難しいことではありません。
（簡約規則は正しさを「ほぼ」確認できます。完全に、ではありません。
なぜなら、フィールドの並べ直しによってフィールドの簡約順序が変わりうるためです。）
もちろん、ラベルfooを持つレコードをたまたま使ったときには、このエンコードはあまり効率的ではありません。
しかしこの問題は見た目ほど深刻ではありません。
もし、コンパイラがプログラム全体を同時に見ることができると仮定するなら、ラベルの番号づけをうまく選んで、一番よく使われるラベルに小さいポジションを与えることができます。
実際、商用のコンパイラで本質的にこれをやっているものもあります!
直積がレコードに一般化できたのと同様、直和は n-個のラベルを持った型「バリアント」(variants)に一般化できます。
T1+T2 の代わりに <l1:T1,l2:T2,...ln:Tn> のように書くことができます。
ここでl1、l2、... はフィールドラベルで、インスタンスの構成と、case のラベルの両方に使われます。
n-個のバリアントは、リストや木構造のような任意の帰納的データ型をゼロから構築するのに必要なメカニズムのほとんどを与えます。
唯一足りないのは、型定義の再帰です。ここではこの話題は扱いません。
ただ、詳細な扱いはいろいろなテキストブックに書かれています。
例えば "Types and Programming Languages" Pierce 2002 （Bib.v内）です。
練習問題: ★★★, standard (STLCE_definitions)
- 数値
- 直和
- リスト
- Unit型
- 直積
- let (束縛を含む)
- fix
Inductive ty : Type :=
| Arrow : ty -> ty -> ty
| Nat : ty
| Sum : ty -> ty -> ty
| List : ty -> ty
| Unit : ty
| Prod : ty -> ty -> ty.
Inductive tm : Type :=
| var : string -> tm
| app : tm -> tm -> tm
| abs : string -> ty -> tm -> tm
| const : nat -> tm
| scc : tm -> tm
| prd : tm -> tm
| mlt : tm -> tm -> tm
| test0 : tm -> tm -> tm -> tm
| tinl : ty -> tm -> tm
| tinr : ty -> tm -> tm
| tcase : tm -> string -> tm -> string -> tm -> tm
| tnil : ty -> tm
| tcons : tm -> tm -> tm
| tlcase : tm -> tm -> string -> string -> tm -> tm
| unit : tm
| pair : tm -> tm -> tm
| fst : tm -> tm
| snd : tm -> tm
| tlet : string -> tm -> tm -> tm
| tfix : tm -> tm.
なお、簡潔にするため、ブール値をなくし、その代わりゼロテストと条件分岐を組み合わせた test0 構文を提供しています。
つまり、
test x = 0 then ... else ...
と書く代わりに、次のように書きます:
test0 x then ... else ...
Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
match t with
| var y =>
if eqb_string x y then s else t
| abs y T t1 =>
abs y T (if eqb_string x y then t1 else (subst x s t1))
| app t1 t2 =>
app (subst x s t1) (subst x s t2)
| const n =>
const n
| scc t1 =>
scc (subst x s t1)
| prd t1 =>
prd (subst x s t1)
| mlt t1 t2 =>
mlt (subst x s t1) (subst x s t2)
| test0 t1 t2 t3 =>
test0 (subst x s t1) (subst x s t2) (subst x s t3)
| tinl T t1 =>
tinl T (subst x s t1)
| tinr T t1 =>
tinr T (subst x s t1)
| tcase t0 y1 t1 y2 t2 =>
tcase (subst x s t0)
y1 (if eqb_string x y1 then t1 else (subst x s t1))
y2 (if eqb_string x y2 then t2 else (subst x s t2))
| tnil T =>
tnil T
| tcons t1 t2 =>
tcons (subst x s t1) (subst x s t2)
| tlcase t1 t2 y1 y2 t3 =>
tlcase (subst x s t1) (subst x s t2) y1 y2
(if eqb_string x y1 then
t3
else if eqb_string x y2 then t3
else (subst x s t3))
| unit => unit
| _ => t
end.
Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).
次にこの言語の値を定義します。
Inductive value : tm -> Prop :=
| v_abs : forall x T11 t12,
value (abs x T11 t12)
| v_nat : forall n1,
value (const n1)
| v_inl : forall v T,
value v ->
value (tinl T v)
| v_inr : forall v T,
value v ->
value (tinr T v)
| v_lnil : forall T, value (tnil T)
| v_lcons : forall v1 vl,
value v1 ->
value vl ->
value (tcons v1 vl)
| v_unit : value unit
| v_pair : forall v1 v2,
value v1 ->
value v2 ->
value (pair v1 v2).
Hint Constructors value.
Reserved Notation "t1 '-->' t2" (at level 40).
Inductive step : tm -> tm -> Prop :=
| ST_AppAbs : forall x T11 t12 v2,
value v2 ->
(app (abs x T11 t12) v2) --> [x:=v2]t12
| ST_App1 : forall t1 t1' t2,
t1 --> t1' ->
(app t1 t2) --> (app t1' t2)
| ST_App2 : forall v1 t2 t2',
value v1 ->
t2 --> t2' ->
(app v1 t2) --> (app v1 t2')
| ST_Succ1 : forall t1 t1',
t1 --> t1' ->
(scc t1) --> (scc t1')
| ST_SuccNat : forall n1,
(scc (const n1)) --> (const (S n1))
| ST_Pred : forall t1 t1',
t1 --> t1' ->
(prd t1) --> (prd t1')
| ST_PredNat : forall n1,
(prd (const n1)) --> (const (pred n1))
| ST_Mult1 : forall t1 t1' t2,
t1 --> t1' ->
(mlt t1 t2) --> (mlt t1' t2)
| ST_Mult2 : forall v1 t2 t2',
value v1 ->
t2 --> t2' ->
(mlt v1 t2) --> (mlt v1 t2')
| ST_Mulconsts : forall n1 n2,
(mlt (const n1) (const n2)) --> (const (mult n1 n2))
| ST_Test01 : forall t1 t1' t2 t3,
t1 --> t1' ->
(test0 t1 t2 t3) --> (test0 t1' t2 t3)
| ST_Test0Zero : forall t2 t3,
(test0 (const 0) t2 t3) --> t2
| ST_Test0Nonzero : forall n t2 t3,
(test0 (const (S n)) t2 t3) --> t3
| ST_Inl : forall t1 t1' T,
t1 --> t1' ->
(tinl T t1) --> (tinl T t1')
| ST_Inr : forall t1 t1' T,
t1 --> t1' ->
(tinr T t1) --> (tinr T t1')
| ST_Case : forall t0 t0' x1 t1 x2 t2,
t0 --> t0' ->
(tcase t0 x1 t1 x2 t2) --> (tcase t0' x1 t1 x2 t2)
| ST_CaseInl : forall v0 x1 t1 x2 t2 T,
value v0 ->
(tcase (tinl T v0) x1 t1 x2 t2) --> [x1:=v0]t1
| ST_CaseInr : forall v0 x1 t1 x2 t2 T,
value v0 ->
(tcase (tinr T v0) x1 t1 x2 t2) --> [x2:=v0]t2
| ST_Cons1 : forall t1 t1' t2,
t1 --> t1' ->
(tcons t1 t2) --> (tcons t1' t2)
| ST_Cons2 : forall v1 t2 t2',
value v1 ->
t2 --> t2' ->
(tcons v1 t2) --> (tcons v1 t2')
| ST_Lcase1 : forall t1 t1' t2 x1 x2 t3,
t1 --> t1' ->
(tlcase t1 t2 x1 x2 t3) --> (tlcase t1' t2 x1 x2 t3)
| ST_LcaseNil : forall T t2 x1 x2 t3,
(tlcase (tnil T) t2 x1 x2 t3) --> t2
| ST_LcaseCons : forall v1 vl t2 x1 x2 t3,
value v1 ->
value vl ->
(tlcase (tcons v1 vl) t2 x1 x2 t3)
--> (subst x2 vl (subst x1 v1 t3))
where "t1 '-->' t2" := (step t1 t2).
Notation multistep := (multi step).
Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40).
Hint Constructors step.
次に型付け規則を定義します。
上述の推論規則のほとんど直接の転写です。
Reserved Notation "Gamma '|-' t '\in' T" (at level 40).
Inductive has_type : context -> tm -> ty -> Prop :=
| T_Var : forall Gamma x T,
Gamma x = Some T ->
Gamma |- (var x) \in T
| T_Abs : forall Gamma x T11 T12 t12,
(update Gamma x T11) |- t12 \in T12 ->
Gamma |- (abs x T11 t12) \in (Arrow T11 T12)
| T_App : forall T1 T2 Gamma t1 t2,
Gamma |- t1 \in (Arrow T1 T2) ->
Gamma |- t2 \in T1 ->
Gamma |- (app t1 t2) \in T2
| T_Nat : forall Gamma n1,
Gamma |- (const n1) \in Nat
| T_Succ : forall Gamma t1,
Gamma |- t1 \in Nat ->
Gamma |- (scc t1) \in Nat
| T_Pred : forall Gamma t1,
Gamma |- t1 \in Nat ->
Gamma |- (prd t1) \in Nat
| T_Mult : forall Gamma t1 t2,
Gamma |- t1 \in Nat ->
Gamma |- t2 \in Nat ->
Gamma |- (mlt t1 t2) \in Nat
| T_Test0 : forall Gamma t1 t2 t3 T1,
Gamma |- t1 \in Nat ->
Gamma |- t2 \in T1 ->
Gamma |- t3 \in T1 ->
Gamma |- (test0 t1 t2 t3) \in T1
| T_Inl : forall Gamma t1 T1 T2,
Gamma |- t1 \in T1 ->
Gamma |- (tinl T2 t1) \in (Sum T1 T2)
| T_Inr : forall Gamma t2 T1 T2,
Gamma |- t2 \in T2 ->
Gamma |- (tinr T1 t2) \in (Sum T1 T2)
| T_Case : forall Gamma t0 x1 T1 t1 x2 T2 t2 T,
Gamma |- t0 \in (Sum T1 T2) ->
(update Gamma x1 T1) |- t1 \in T ->
(update Gamma x2 T2) |- t2 \in T ->
Gamma |- (tcase t0 x1 t1 x2 t2) \in T
| T_Nil : forall Gamma T,
Gamma |- (tnil T) \in (List T)
| T_Cons : forall Gamma t1 t2 T1,
Gamma |- t1 \in T1 ->
Gamma |- t2 \in (List T1) ->
Gamma |- (tcons t1 t2) \in (List T1)
| T_Lcase : forall Gamma t1 T1 t2 x1 x2 t3 T2,
Gamma |- t1 \in (List T1) ->
Gamma |- t2 \in T2 ->
(update (update Gamma x2 (List T1)) x1 T1) |- t3 \in T2 ->
Gamma |- (tlcase t1 t2 x1 x2 t3) \in T2
| T_Unit : forall Gamma,
Gamma |- unit \in Unit
where "Gamma '|-' t '\in' T" := (has_type Gamma t T).
Hint Constructors has_type.
Definition manual_grade_for_extensions_definition : option (nat*string) := None.
☐
練習問題: ★★★, standard (STLCE_examples)
最初に、いくつか変数名を定義しましょう:
Open Scope string_scope.
Notation x := "x".
Notation y := "y".
Notation a := "a".
Notation f := "f".
Notation g := "g".
Notation l := "l".
Notation k := "k".
Notation i1 := "i1".
Notation i2 := "i2".
Notation processSum := "processSum".
Notation n := "n".
Notation eq := "eq".
Notation m := "m".
Notation evenodd := "evenodd".
Notation even := "even".
Notation odd := "odd".
Notation eo := "eo".
次に、Coq にちょっと手を入れて、型の導出の検索を自動化します。
詳細を理解する必要はまったくありません。
ざっと眺めておけば、もしautoに独自の拡張をしなければならなくなったとき、何を調べれば良いかがわかるでしょう。
以下のHint宣言は、次のように言っています:
autoが (Gamma |- (app e1 e1) \in T) という形のゴールに到達したときは常に、 eapply T_App を考えなさい。
この結果、中間的な型 T1 の存在変数が残ります。
lcaseについても同様です。
その存在変数は、e1とe2の型導出の探索の仮定で具体化されます。
またヒントに、等号による比較の形のゴールを解く場合に「より困難なことを試しなさい」ということも追加します。
これは、T_Var（これは事前条件に等号による比較を含みます）を自動的に使用するのに便利です。
Hint Extern 2 (has_type _ (app _ _) _) =>
eapply T_App; auto.
Hint Extern 2 (has_type _ (tlcase _ _ _ _ _) _) =>
eapply T_Lcase; auto.
Hint Extern 2 (_ = _) => compute; reflexivity.
Module Numtest.
Definition test :=
test0
(prd
(scc
(prd
(mlt
(const 2)
(const 0)))))
(const 5)
(const 6).
Example typechecks :
empty |- test \in Nat.
Proof.
unfold test.
auto 10.
Admitted.
Example numtest_reduces :
test -->* const 5.
Proof.
Admitted.
End Numtest.
Module Prodtest.
Definition test :=
snd
(fst
(pair
(pair
(const 5)
(const 6))
(const 7))).
Example typechecks :
empty |- test \in Nat.
Proof. unfold test. eauto 15. Admitted.
Example reduces :
test -->* const 6.
Proof.
Admitted.
End Prodtest.
Module LetTest.
Definition test :=
tlet
x
(prd (const 6))
(scc (var x)).
Example typechecks :
empty |- test \in Nat.
Proof. unfold test. eauto 15. Admitted.
Example reduces :
test -->* const 6.
Proof.
Admitted.
End LetTest.
Module Sumtest1.
Definition test :=
tcase (tinl Nat (const 5))
x (var x)
y (var y).
Example typechecks :
empty |- test \in Nat.
Proof. unfold test. eauto 15. Admitted.
Example reduces :
test -->* (const 5).
Proof.
Admitted.
End Sumtest1.
Module Sumtest2.
Definition test :=
tlet
processSum
(abs x (Sum Nat Nat)
(tcase (var x)
n (var n)
n (test0 (var n) (const 1) (const 0))))
(pair
(app (var processSum) (tinl Nat (const 5)))
(app (var processSum) (tinr Nat (const 5)))).
Example typechecks :
empty |- test \in (Prod Nat Nat).
Proof. unfold test. eauto 15. Admitted.
Example reduces :
test -->* (pair (const 5) (const 0)).
Proof.
Admitted.
End Sumtest2.
Module ListTest.
Definition test :=
tlet l
(tcons (const 5) (tcons (const 6) (tnil Nat)))
(tlcase (var l)
(const 0)
x y (mlt (var x) (var x))).
Example typechecks :
empty |- test \in Nat.
Proof. unfold test. eauto 20. Admitted.
Example reduces :
test -->* (const 25).
Proof.
Admitted.
End ListTest.
Module FixTest1.
Definition fact :=
tfix
(abs f (Arrow Nat Nat)
(abs a Nat
(test0
(var a)
(const 1)
(mlt
(var a)
(app (var f) (prd (var a))))))).
（警告: いくつかの規則が間違っていてもfactの型チェックが通るかもしれません。）
Example typechecks :
empty |- fact \in (Arrow Nat Nat).
Proof. unfold fact. auto 10. Admitted.
Example reduces :
(app fact (const 4)) -->* (const 24).
Proof.
Admitted.
End FixTest1.
Module FixTest2.
Definition map :=
abs g (Arrow Nat Nat)
(tfix
(abs f (Arrow (List Nat) (List Nat))
(abs l (List Nat)
(tlcase (var l)
(tnil Nat)
a l (tcons (app (var g) (var a))
(app (var f) (var l))))))).
Example typechecks :
empty |- map \in
(Arrow (Arrow Nat Nat)
(Arrow (List Nat)
(List Nat))).
Proof. unfold map. auto 10. Admitted.
Example reduces :
app (app map (abs a Nat (scc (var a))))
(tcons (const 1) (tcons (const 2) (tnil Nat)))
-->* (tcons (const 2) (tcons (const 3) (tnil Nat))).
Proof.
Admitted.
End FixTest2.
Module FixTest3.
Definition equal :=
tfix
(abs eq (Arrow Nat (Arrow Nat Nat))
(abs m Nat
(abs n Nat
(test0 (var m)
(test0 (var n) (const 1) (const 0))
(test0 (var n)
(const 0)
(app (app (var eq)
(prd (var m)))
(prd (var n)))))))).
Example typechecks :
empty |- equal \in (Arrow Nat (Arrow Nat Nat)).
Proof. unfold equal. auto 10. Admitted.
Example reduces :
(app (app equal (const 4)) (const 4)) -->* (const 1).
Proof.
Admitted.
Example reduces2 :
(app (app equal (const 4)) (const 5)) -->* (const 0).
Proof.
Admitted.
End FixTest3.
Module FixTest4.
Definition eotest :=
tlet evenodd
(tfix
(abs eo (Prod (Arrow Nat Nat) (Arrow Nat Nat))
(pair
(abs n Nat
(test0 (var n)
(const 1)
(app (snd (var eo)) (prd (var n)))))
(abs n Nat
(test0 (var n)
(const 0)
(app (fst (var eo)) (prd (var n))))))))
(tlet even (fst (var evenodd))
(tlet odd (snd (var evenodd))
(pair
(app (var even) (const 3))
(app (var even) (const 4))))).
Example typechecks :
empty |- eotest \in (Prod Nat Nat).
Proof. unfold eotest. eauto 30. Admitted.
Example reduces :
eotest -->* (pair (const 0) (const 1)).
Proof.
Admitted.
End FixTest4.
End Examples.
☐
拡張したシステムの進行と保存の証明は、純粋な単純型付きラムダ計算のものと本質的に同じです（もちろん長くはなりますが）。
練習問題: ★★★, standard (STLCE_progress)
Theorem progress : forall t T,
empty |- t \in T ->
value t \/ exists t', t --> t'.
Proof with eauto.
intros t T Ht.
remember empty as Gamma.
generalize dependent HeqGamma.
induction Ht; intros HeqGamma; subst.
-
inversion H.
-
left...
-
right.
destruct IHHt1; subst...
+
destruct IHHt2; subst...
*
inversion H; subst; try solve_by_invert.
exists (subst x t2 t12)...
*
inversion H0 as [t2' Hstp]. exists (app t1 t2')...
+
inversion H as [t1' Hstp]. exists (app t1' t2)...
-
left...
-
right.
destruct IHHt...
+
inversion H; subst; try solve_by_invert.
exists (const (S n1))...
+
inversion H as [t1' Hstp].
exists (scc t1')...
-
right.
destruct IHHt...
+
inversion H; subst; try solve_by_invert.
exists (const (pred n1))...
+
inversion H as [t1' Hstp].
exists (prd t1')...
-
right.
destruct IHHt1...
+
destruct IHHt2...
*
inversion H; subst; try solve_by_invert.
inversion H0; subst; try solve_by_invert.
exists (const (mult n1 n0))...
*
inversion H0 as [t2' Hstp].
exists (mlt t1 t2')...
+
inversion H as [t1' Hstp].
exists (mlt t1' t2)...
-
right.
destruct IHHt1...
+
inversion H; subst; try solve_by_invert.
destruct n1 as [|n1'].
*
exists t2...
*
exists t3...
+
inversion H as [t1' H0].
exists (test0 t1' t2 t3)...
-
destruct IHHt...
+
right. inversion H as [t1' Hstp]...
-
destruct IHHt...
+
right. inversion H as [t1' Hstp]...
-
right.
destruct IHHt1...
+
inversion H; subst; try solve_by_invert.
*
exists ([x1:=v]t1)...
*
exists ([x2:=v]t2)...
+
inversion H as [t0' Hstp].
exists (tcase t0' x1 t1 x2 t2)...
-
left...
-
destruct IHHt1...
+
destruct IHHt2...
*
right. inversion H0 as [t2' Hstp].
exists (tcons t1 t2')...
+
right. inversion H as [t1' Hstp].
exists (tcons t1' t2)...
-
right.
destruct IHHt1...
+
inversion H; subst; try solve_by_invert.
*
exists t2...
*
exists ([x2:=vl]([x1:=v1]t3))...
+
inversion H as [t1' Hstp].
exists (tlcase t1' t2 x1 x2 t3)...
-
left...
Admitted.
Definition manual_grade_for_progress : option (nat*string) := None.
☐
練習問題: ★★★, standard (STLCE_context_invariance)
Inductive appears_free_in : string -> tm -> Prop :=
| afi_var : forall x,
appears_free_in x (var x)
| afi_app1 : forall x t1 t2,
appears_free_in x t1 -> appears_free_in x (app t1 t2)
| afi_app2 : forall x t1 t2,
appears_free_in x t2 -> appears_free_in x (app t1 t2)
| afi_abs : forall x y T11 t12,
y <> x ->
appears_free_in x t12 ->
appears_free_in x (abs y T11 t12)
| afi_succ : forall x t,
appears_free_in x t ->
appears_free_in x (scc t)
| afi_pred : forall x t,
appears_free_in x t ->
appears_free_in x (prd t)
| afi_mult1 : forall x t1 t2,
appears_free_in x t1 ->
appears_free_in x (mlt t1 t2)
| afi_mult2 : forall x t1 t2,
appears_free_in x t2 ->
appears_free_in x (mlt t1 t2)
| afi_test01 : forall x t1 t2 t3,
appears_free_in x t1 ->
appears_free_in x (test0 t1 t2 t3)
| afi_test02 : forall x t1 t2 t3,
appears_free_in x t2 ->
appears_free_in x (test0 t1 t2 t3)
| afi_test03 : forall x t1 t2 t3,
appears_free_in x t3 ->
appears_free_in x (test0 t1 t2 t3)
| afi_inl : forall x t T,
appears_free_in x t ->
appears_free_in x (tinl T t)
| afi_inr : forall x t T,
appears_free_in x t ->
appears_free_in x (tinr T t)
| afi_case0 : forall x t0 x1 t1 x2 t2,
appears_free_in x t0 ->
appears_free_in x (tcase t0 x1 t1 x2 t2)
| afi_case1 : forall x t0 x1 t1 x2 t2,
x1 <> x ->
appears_free_in x t1 ->
appears_free_in x (tcase t0 x1 t1 x2 t2)
| afi_case2 : forall x t0 x1 t1 x2 t2,
x2 <> x ->
appears_free_in x t2 ->
appears_free_in x (tcase t0 x1 t1 x2 t2)
| afi_cons1 : forall x t1 t2,
appears_free_in x t1 ->
appears_free_in x (tcons t1 t2)
| afi_cons2 : forall x t1 t2,
appears_free_in x t2 ->
appears_free_in x (tcons t1 t2)
| afi_lcase1 : forall x t1 t2 y1 y2 t3,
appears_free_in x t1 ->
appears_free_in x (tlcase t1 t2 y1 y2 t3)
| afi_lcase2 : forall x t1 t2 y1 y2 t3,
appears_free_in x t2 ->
appears_free_in x (tlcase t1 t2 y1 y2 t3)
| afi_lcase3 : forall x t1 t2 y1 y2 t3,
y1 <> x ->
y2 <> x ->
appears_free_in x t3 ->
appears_free_in x (tlcase t1 t2 y1 y2 t3)
.
Hint Constructors appears_free_in.
Lemma context_invariance : forall Gamma Gamma' t S,
Gamma |- t \in S ->
(forall x, appears_free_in x t -> Gamma x = Gamma' x) ->
Gamma' |- t \in S.
Proof with eauto 30.
intros. generalize dependent Gamma'.
induction H;
intros Gamma' Heqv...
-
apply T_Var... rewrite <- Heqv...
-
apply T_Abs... apply IHhas_type. intros y Hafi.
unfold update, t_update.
destruct (eqb_stringP x y)...
-
eapply T_Case...
+ apply IHhas_type2. intros y Hafi.
unfold update, t_update.
destruct (eqb_stringP x1 y)...
+ apply IHhas_type3. intros y Hafi.
unfold update, t_update.
destruct (eqb_stringP x2 y)...
-
eapply T_Lcase... apply IHhas_type3. intros y Hafi.
unfold update, t_update.
destruct (eqb_stringP x1 y)...
destruct (eqb_stringP x2 y)...
Admitted.
Lemma free_in_context : forall x t T Gamma,
appears_free_in x t ->
Gamma |- t \in T ->
exists T', Gamma x = Some T'.
Proof with eauto.
intros x t T Gamma Hafi Htyp.
induction Htyp; inversion Hafi; subst...
-
destruct IHHtyp as [T' Hctx]... exists T'.
unfold update, t_update in Hctx.
rewrite false_eqb_string in Hctx...
-
destruct IHHtyp2 as [T' Hctx]... exists T'.
unfold update, t_update in Hctx.
rewrite false_eqb_string in Hctx...
-
destruct IHHtyp3 as [T' Hctx]... exists T'.
unfold update, t_update in Hctx.
rewrite false_eqb_string in Hctx...
-
clear Htyp1 IHHtyp1 Htyp2 IHHtyp2.
destruct IHHtyp3 as [T' Hctx]... exists T'.
unfold update, t_update in Hctx.
rewrite false_eqb_string in Hctx...
rewrite false_eqb_string in Hctx...
Admitted.
Definition manual_grade_for_context_invariance : option (nat*string) := None.
☐
Lemma substitution_preserves_typing : forall Gamma x U v t S,
(update Gamma x U) |- t \in S ->
empty |- v \in U ->
Gamma |- ([x:=v]t) \in S.
Proof with eauto.
intros Gamma x U v t S Htypt Htypv.
generalize dependent Gamma. generalize dependent S.
induction t;
intros S Gamma Htypt; simpl; inversion Htypt; subst...
-
simpl. rename s into y.
unfold update, t_update in H1.
destruct (eqb_stringP x y).
+
subst.
inversion H1; subst. clear H1.
eapply context_invariance...
intros x Hcontra.
destruct (free_in_context _ _ S empty Hcontra)
as [T' HT']...
inversion HT'.
+
apply T_Var...
-
rename s into y. rename t into T11.
apply T_Abs...
destruct (eqb_stringP x y) as [Hxy|Hxy].
+
eapply context_invariance...
subst.
intros x Hafi. unfold update, t_update.
destruct (eqb_string y x)...
+
apply IHt. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (eqb_stringP y z) as [Hyz|Hyz]...
subst.
rewrite false_eqb_string...
-
rename s into x1. rename s0 into x2.
eapply T_Case...
+
destruct (eqb_stringP x x1) as [Hxx1|Hxx1].
*
eapply context_invariance...
subst.
intros z Hafi. unfold update, t_update.
destruct (eqb_string x1 z)...
*
apply IHt2. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (eqb_stringP x1 z) as [Hx1z|Hx1z]...
subst. rewrite false_eqb_string...
+
destruct (eqb_stringP x x2) as [Hxx2|Hxx2].
*
eapply context_invariance...
subst.
intros z Hafi. unfold update, t_update.
destruct (eqb_string x2 z)...
*
apply IHt3. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (eqb_stringP x2 z)...
subst. rewrite false_eqb_string...
-
rename s into y1. rename s0 into y2.
eapply T_Lcase...
destruct (eqb_stringP x y1).
+
simpl.
eapply context_invariance...
subst.
intros z Hafi. unfold update, t_update.
destruct (eqb_stringP y1 z)...
+
destruct (eqb_stringP x y2).
*
eapply context_invariance...
subst.
intros z Hafi. unfold update, t_update.
destruct (eqb_stringP y2 z)...
*
apply IHt3. eapply context_invariance...
intros z Hafi. unfold update, t_update.
destruct (eqb_stringP y1 z)...
subst. rewrite false_eqb_string...
destruct (eqb_stringP y2 z)...
subst. rewrite false_eqb_string...
Admitted.
Definition manual_grade_for_substitution_preserves_typing : option (nat*string) := None.
☐
Theorem preservation : forall t t' T,
empty |- t \in T ->
t --> t' ->
empty |- t' \in T.
Proof with eauto.
intros t t' T HT.
remember empty as Gamma. generalize dependent HeqGamma.
generalize dependent t'.
induction HT;
intros t' HeqGamma HE; subst; inversion HE; subst...
-
inversion HE; subst...
+
apply substitution_preserves_typing with T1...
inversion HT1...
-
inversion HT1; subst.
eapply substitution_preserves_typing...
-
inversion HT1; subst.
eapply substitution_preserves_typing...
-
+
inversion HT1; subst.
apply substitution_preserves_typing with (List T1)...
apply substitution_preserves_typing with T1...
Admitted.
Definition manual_grade_for_preservation : option (nat*string) := None.
☐