在前一部分中， 我们简单的学习了Lambda calculus的定义。既然是给lambda演算添加了类型，那么我们自然是希望这个类型系统真的能够减少出现不能归约的错误类型，是一个真正可靠的系统。最直接的方式就是使用定理证明器来证明一下我们在类型系统中学习过的性质。
0X00 经典形式(Canonical Forms)
之前在介绍类型系统的时候我们证明过， 有的形式的值可以被看作是经典形式，如果看到这种形式，我们立马可以推测出是哪种值。STLC的两种值类型， bool类型和箭头类型，自然也有对应的经典形式。
形式化的有：
Lemma canonical_forms_bool : ∀t,
empty ⊢ t ∈ Bool →
value t →
(t = tru) ∨ (t = fls).
Lemma canonical_forms_fun : ∀t T1 T2,
empty ⊢ t ∈ (Arrow T1 T2) →
value t →
∃x u, t = abs x T1 u.
0X01 Progress
定义良好的类型关系的重要性质就是， 一个封闭的类型良好的项是不会阻塞的。
Theorem progress : ∀ t T,
empty ⊢ t ∈ T →
value t ∨ ∃t', t --> t'.
接下来，针对STLC， 证明这条性质。
Proof
对empty ⊢ t ∈ T进行归纳证明：
-
对于T_Fls, T_Tru， T_Abs，的情况tru,fls, lambda满足值的定义。
-
当上式取T_Var时，需要有empty x = T成立,但是我们之前说过，自由变量在我们定义定义的语言中是不能单独存在的，其必须有类型上下文，（No free occurrance） .这种情况排除。
-
当T_App时， t= t11 t12, T = T12,此时goal变为
value t11 t12 ∨ ∃t', t11 t12 --> t'有归纳假设IH
IH1: value t1 ∨ ∃t', t1 --> t'. IH2: value t2 ∨ ∃t', t2 --> t'.对IH分情况讨论，
- 如果t1是值 t2 -->t'，那么符合ST_App2的情况， 可以继续归约；
- 如果t2 也是值，根据函数体的经典形式一定可以写为abs x T1 u，根据ST_Abs,可以继续归约；
- 如果t1可以继续归约， 那么符合ST_App1的情况，可以继续归约。
所以在T_App情况下命题成立。
-
当T_Test时。这种情况其实和命令式语言类似，此时goal 为：
value test t1 then t2 else t3 ∨ ∃t', test t1 then t2 else t3 --> t'IH为：
IH1: value t1 ∨ ∃t', t1 --> t'. IH2: value t2 ∨ ∃t', t2 --> t'. IH3: value t3 ∨ ∃t', t3 --> t'.对IH分情况讨论
- 如t1 是值，那么，根据t1的正负性表达式可以使用ST_TestTru, ST_TestFls分别进行归约；
- 如t1可以归约，那么可以根据ST_Test进行归约。
所以在T_Test时命题成立
综上，之前定义的STLC具备progress性质
Q.E.D.
0X02 自由变量
之前说过了，我们的替换操作只能对 自由出现(free occurance)进行替换， 所以首先来定义一下什么样子的上下文能满足自由替换。
Definition
如果满足以下几种不同情况之一，那么我们称变量x自由出现在满足上下文Gamma的项目t中
- t是变量x
- t是一个参数和不包含x的函数，并且t自由出现在函数体中
- t是函数作用，而在作用或被作用的项目中t都自由出现
- t是判断语句，而在组成判断语句的各个组成部分中有t自由出现
形式化的有
Inductive appears_free_in : string → tm → Prop :=
| afi_var : ∀x,
appears_free_in x (var x)
| afi_app1 : ∀x t1 t2,
appears_free_in x t1 →
appears_free_in x (app t1 t2)
| afi_app2 : ∀x t1 t2,
appears_free_in x t2 →
appears_free_in x (app t1 t2)
| afi_abs : ∀x y T11 t12,
y ≠ x →
appears_free_in x t12 →
appears_free_in x (abs y T11 t12)
| afi_test1 : ∀x t1 t2 t3,
appears_free_in x t1 →
appears_free_in x (test t1 t2 t3)
| afi_test2 : ∀x t1 t2 t3,
appears_free_in x t2 →
appears_free_in x (test t1 t2 t3)
| afi_test3 : ∀x t1 t2 t3,
appears_free_in x t3 →
appears_free_in x (test t1 t2 t3).
如在一个项中没有自由变量，那么我们称该项封闭(closed).
形式化的有
Definition closed (t:tm) :=
∀x, ¬appears_free_in x t.
0X03 替换(substitution)
在证明替换都是安全的之前，我们需要先证明一个引理
Lemma
如果x在项t中自由出现，且项t类型良好(well-typed)，那么上下文Gamma中必然存在一个x的偏射。
形式化的有
Lemma free_in_context : ∀x t T Gamma,
appears_free_in x t →
Gamma ⊢ t ∈ T →
∃T', Gamma x = Some T'.
这个引理其实是比较显然的，也比较好证明，归纳自由出现的关系就行了，根据归纳假设就可证明.
有一个比较显然的推论：
Corollary
如果一个项在空上下文中类型良好，那么这个项是封闭的。
在证明安全替换不改变类型之前，首先我们先证明一下上下问在替换中满足的性质。
Lemma
在安全替换的过程中，我们的上下文可能会发生改变，但是上下文的这种改变应该不能改变原本项目的类型。
形式化的有
Lemma context_invariance : ∀Gamma Gamma' t T,
Gamma ⊢ t ∈ T →
(∀x, appears_free_in x t → Gamma x = Gamma' x) →
Gamma' ⊢ t ∈ T.
Proof
首先因为我们并不知道变化后的Gamma‘会是什么，这个和具体的变化有关，所以在这里，我们范化Gamma'，对类型关系 Gamma ⊢ t ∈ T进行归纳。
- 当关系最后一步为T_Fls, T_Tru时，结论显然成立。
- 当T_Var时， t = var x0,并且引入Gamma x0= Some x0,此时有goal为
此时根据T_Var可以轻松得到。(∀x, appears_free_in x (var x0) → Gamma x = Gamma' x) → Gamma' ⊢ (var x0) ∈ T. - 当T_App时， t = t1 t2, T = T12,并引入
代入，得新goal为Gamma ⊢ t1 ∈ Arrow T11 T12 Gamma ⊢ t2 ∈ T11
此时直接根据T_App可得(∀x, appears_free_in x (app t1 t2) → Gamma x = Gamma' x) → Gamma' ⊢ (app t1 t2) ∈ T12. - 当T_Abs时，t = abs x0 T11 t12, T = Arrow T11 T12, 引入条件
此时goal为(x0 ⊢> T11 ; Gamma) ⊢ t12 ∈ T12
IH为(∀x, appears_free_in x (abs x0 T11 t12) → Gamma x = Gamma' x) → Gamma' ⊢ (abs x0 T11 t12) ∈ Arrow T11 T12
若要想在此使用T_Abs来完成证明，需要∀Gamma', (∀x, appears_free_in x t12 → (x0 ⊢> T11 ; Gamma) x = Gamma' x) → Gamma' ⊢ t12 ∈ T12
这里我们明显需要给IH构造一个Gamma',这样应用IH就可以完成证明；(x0 ⊢> T11 ; Gamma') ⊢ t12 ∈ T12
取Gamma' = x0 ⊢> T11 ; Gamma',应用IH，可以得到新goal为
此时分情况讨论x0 =? x,∀x, appears_free_in x t12 → (x0 ⊢> T11 ; Gamma) x = (x0 ⊢> T11 ;Gamma') x- 如果相等，没什么好说的肯定成立， T11 = T11
- 如果不相等x0
x，那么相当于需要证明Gamma x = Gamma ' x ，此时应用条件
可以不难发现满足afi_abs的情况，命题成立(∀x, appears_free_in x (abs x0 T11 t12) → Gamma x = Gamma' x)
综上，归纳得原命题成立
Q.E.D.
然后我们就可以证明安全替换不会改变类型了！！
形式化的有
Lemma
Lemma substitution_preserves_typing : ∀Gamma x U t v T,
(x ⊢> U ; Gamma) ⊢ t ∈ T →
empty ⊢ v ∈ U →
Gamma ⊢ [x:=v]t ∈ T.
Proof
泛化Gamma T, 对t进行归纳证明
- Fls和Tru,替换并不改变任何东西。显然成立
- 对于if， abs, app的情况,归纳以后，根据归纳假设都正好符合替换的定义
- var时，有两种情况
- 如果x = v, 那么相当于不发生替换,此时goal可容易改写为
此时，由(v ⊢> U ; Gamma) ⊢ v ∈ T 不难得出 T = U, 故替换后goal为Gamma ⊢ v ∈ T
根据之前证明过的context_invariance可以发现，只要证empty ⊢ v ∈ U → Gamma ⊢ v ∈ U
这一点其实很明显，因为empty肯定是封闭的，故成立。∀x, appears_free_in x t → empty x = Gamma x - 如果 x
- 如果x = v, 那么相当于不发生替换,此时goal可容易改写为
- abs时，t = abs x' T1 t1。有归纳假设 IH：
当x v相等时，和上面相似，替换后的新goal为：∀ T Gramma, (x ⊢> U ; Gamma) ⊢ t1 ∈ T → Gamma ⊢ [x:=v]t1 ∈ T
此时根据类型的定义T_Abs可以看出，T = Arrow T11 T12 , 要证Gamma ⊢ abs v T1 t1 ∈ T
此时反演条件(v⊢> U ; Gamma) ⊢ abs v T1 t1 ∈ Arrow T11 T12可以得到，(v ⊢> T11 ; Gamma) ⊢ t1 ∈ T12
显然和goal相同。(v ⊢> T11 ; v ⊢> U ; Gamma) ⊢ t1 ∈ T12
当 x
根据T_Abs不难看出，goal为
此时应用归纳假设,goal变为(v ⊢> T11 ; Gamma) ⊢ [x:=v] t1 ∈ T12
加上之反演过的条件(v⊢> U ; Gamma) ⊢ abs v T1 t1 ∈ Arrow T11 T12(x ⊢> U ; v ⊢> T11 ; Gamma) ⊢ t1 ∈ T12
，又可以应用context_invariance了,goal变为
因为x v并不相等，所以上面的式子成立∀x, appears_free_in x t → (x ⊢> U ; v ⊢> T11 ; Gamma) x = ( v ⊢> T11 ; x ⊢> U ;Gamma) x
Q.E.D.
0X04 Preservation
有了上面的结论我们终于可以证明类型关系在归约过程中不会发生改变了
Theorem preservation : ∀t t' T,
empty ⊢ t ∈ T →
t --> t' →
empty ⊢ t' ∈ T.
其实这里已经满简单了，毕竟除了App之外的case都是平凡的。
Proof
对类型关系empty ⊢ t ∈ T进行归纳证明：
- T_Fls, T_Tru, T_Abs都没有什么好说，这些case都不能向下归约了。
- T_Test时， 直接反演empty ⊢ test t1 t2 t3 ∈ T,三种步进最后的类型其实都一样都是T，再加上归纳假设就可以证明。
- T_App1和T_App2其实都是比较平凡的情况，都是可以根据归纳假设和反演得到的
T_AppAbs的情况，根据我们之前证明的替换并不改变类型也可以很简单的证明。
Q.E.D.
这里我写的很简略，主要是其实这里唯一和以前证明的区别就在于出现了替换，我们主要保证，这个替换也没有改变类型那么必然是可以保证类型没有改变的～～
0X05 类型可靠(Type Soundness)
这是 Progress和Preservation的一个推论，在这里就不证明了，和之前类型系统中的基本上一样
0X06 类型唯一性(type uniqueness)
Theorem
一个item只能有一个类型，如果两个item相同那么两个类型就相同。
形式化的有
Theorem unique_types : ∀Gamma e T T',
Gamma ⊢ e ∈ T →
Gamma ⊢ e ∈ T' →
T = T'.
Proof
这个证明真的很没意思。。。。。所有的case基本就是泛化T',然后对Gamma ⊢ e ∈ T 归纳，再反演Gamma ⊢ e ∈ T'，加上归纳假设和替换就可以证出来。。。。。真的不是我懒....唯一技术在于怎么用Coq写的短大概，懒得折腾了。
die
网友评论