简单类型Lambda演算(2)

2019-08-05 本文已影响0人卷毛宿敌大小姐

在前一部分中，我们简单的学习了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 x₀,并且引入Gamma x₀= Some x₀,此时有goal为
```
 (∀x, appears_free_in x (var x0) → Gamma x = Gamma' x)  →
 Gamma' ⊢ (var x0) ∈ T.
```
此时根据T_Var可以轻松得到。

当T_App时， t = t1 t2, T = T12,并引入

Gamma ⊢ t1 ∈ Arrow T11 T12 
Gamma ⊢ t2 ∈ T11

代入，得新goal为

(∀x, appears_free_in x (app t1 t2) → Gamma x = Gamma' x) →
Gamma' ⊢ (app t1 t2) ∈ T12.

此时直接根据T_App可得

当T_Abs时，t = abs x0 T11 t12, T = Arrow T11 T12, 引入条件
```
(x0 ⊢> T11 ; Gamma) ⊢ t12 ∈ T12
```
此时goal为
```
(∀x, appears_free_in x (abs x0 T11 t12) → Gamma x = Gamma' x) →
Gamma' ⊢ (abs x0 T11 t12) ∈ Arrow T11 T12
```
IH为
```
 ∀Gamma', (∀x, appears_free_in x t12 → (x0 ⊢> T11 ; Gamma) x = Gamma' x) →
 Gamma' ⊢ t12 ∈ T12
```
若要想在此使用T_Abs来完成证明，需要
```
(x0 ⊢> T11 ; Gamma') ⊢ t12 ∈ T12
```
这里我们明显需要给IH构造一个Gamma',这样应用IH就可以完成证明；
取Gamma' = x0 ⊢> T11 ; Gamma',应用IH，可以得到新goal为
```
∀x, appears_free_in x t12 →  (x0 ⊢> T11 ; Gamma) x = (x0 ⊢> T11 ;Gamma') x
```
此时分情况讨论x0 =? x,
- 如果相等，没什么好说的肯定成立， T11 = T11
- 如果不相等x0 x，那么相当于需要证明Gamma x = Gamma ' x ，此时应用条件
```
 (∀x, appears_free_in x (abs x0 T11 t12) → Gamma x = Gamma' x) 
```
  可以不难发现满足afi_abs的情况，命题成立

综上，归纳得原命题成立
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可容易改写为
```
Gamma ⊢ v ∈ T
```
  此时，由(v ⊢> U ; Gamma) ⊢ v ∈ T 不难得出 T = U, 故替换后goal为
```
empty ⊢ v ∈ U → Gamma  ⊢ v ∈ U
```
  根据之前证明过的context_invariance可以发现，只要证
```
∀x, appears_free_in x t → empty x = Gamma x
```
  这一点其实很明显，因为empty肯定是封闭的，故成立。
- 如果 x $\neq$ v那么，展开偏射更新操作后不难得到，类型不变。
abs时，t = abs x' T1 t1。有归纳假设 IH：
```
∀ T Gramma, (x ⊢> U ; Gamma) ⊢ t1 ∈ T → 
Gamma ⊢ [x:=v]t1 ∈ T
```
当x v相等时，和上面相似，替换后的新goal为：
```
Gamma ⊢ abs v T1 t1 ∈ T
```
此时根据类型的定义T_Abs可以看出，T = Arrow T11 T12 , 要证
```
(v ⊢> T11 ; Gamma) ⊢ t1 ∈ T12
```
此时反演条件(v⊢> U ; Gamma) ⊢ abs v T1 t1 ∈ Arrow T11 T12可以得到，
```
(v  ⊢> T11 ; v ⊢> U ; Gamma) ⊢ t1 ∈ T12
```
显然和goal相同。
当 x v时:
根据T_Abs不难看出，goal为
```
(v ⊢> T11 ; Gamma) ⊢ [x:=v] t1 ∈ T12
```
此时应用归纳假设,goal变为
```
(x ⊢> U ; v ⊢> T11 ; Gamma) ⊢ t1 ∈ T12 
```
加上之反演过的条件(v⊢> U ; Gamma) ⊢ abs v T1 t1 ∈ Arrow T11 T12
，又可以应用context_invariance了,goal变为
```
 ∀x, appears_free_in x t →  (x ⊢> U ; v ⊢> T11 ; Gamma) x = ( v ⊢> T11 ; x ⊢> U ;Gamma)  x
```
因为x v并不相等，所以上面的式子成立

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相同那么两个类型就相同。