类型系统

不得不说我对type的理解是非常浅薄的， 记得老头在去年的时候推荐了little typer给我，（ 说起来这本书的读书笔记也是一直没有整理好）。也是这本书上面type和相关证明的东西激发了我的兴趣吧。。。。

type is a expression which express another expression.

0X00 问题引入

验证一个只有加法和数字的语言显然不是我们的目标我们希望有更加复杂的语言，比如加入数字和布尔值，判断结构等。定义如下

t ::= tru
    | fls
    | test t then t else t
    | zro
    | scc t
    | prd t
    | iszro t

这里我懒得写latex了，直接给出对应的单步操作语义的形式化定义吧

Reserved Notation "t1 '-->' t2" (at level 40).
Inductive step : tm → tm → Prop :=
  | ST_TestTru : ∀t1 t2,
      (test tru t1 t2) --> t1
  | ST_TestFls : ∀t1 t2,
      (test fls t1 t2) --> t2
  | ST_Test : ∀t1 t1' t2 t3,
      t1 --> t1' →
      (test t1 t2 t3) --> (test t1' t2 t3)
  | ST_Scc : ∀t1 t1',
      t1 --> t1' →
      (scc t1) --> (scc t1')
  | ST_PrdZro :
      (prd zro) --> zro
  | ST_PrdScc : ∀t1,
      nvalue t1 →
      (prd (scc t1)) --> t1
  | ST_Prd : ∀t1 t1',
      t1 --> t1' →
      (prd t1) --> (prd t1')
  | ST_IszroZro :
      (iszro zro) --> tru
  | ST_IszroScc : ∀t1,
       nvalue t1 →
      (iszro (scc t1)) --> fls
  | ST_Iszro : ∀t1 t1',
      t1 --> t1' →
      (iszro t1) --> (iszro t1')

where "t1 '-->' t2" := (step t1 t2).

在这种情况下，很明显，值要么是布尔值，要不就是数字。如果仔细观察上述的语义我们会发现， 这里就很容易出现一些表达式是正规式(normal form)但是不是值(value).
Example:
prd true
这就是一个正规式但是明显不是值，因为根据定义prd后面跟的应该是一个数字。那是因为我们的操作语义只能保证步进这个过程但是我们不能保证步进出来的东西一定是有意义的。

而排除这些无意义正规式的方法就是引入类型(type)。通过定义类型关系(typing relation),我们可以保证我们语言中的item都是良类型(well-type)而不是劣类型(ill-type)。

0X01 类型的表示法

通常的我们使用和 来表示类型关系，例如：⊢ tru ∈ Bool,读作“tru有类型Bool”

ok接下来，给我们之前定义里的所有表达式都加上类型吧！

Reserved Notation "'⊢' t '∈' T" (at level 40).
Inductive has_type : tm → ty → Prop :=
  | T_Tru :
       ⊢ tru ∈ Bool
  | T_Fls :
       ⊢ fls ∈ Bool
  | T_Test : ∀t1 t2 t3 T,
       ⊢ t1 ∈ Bool →
       ⊢ t2 ∈ T →
       ⊢ t3 ∈ T →
       ⊢ test t1 t2 t3 ∈ T
  | T_Zro :
       ⊢ zro ∈ Nat
  | T_Scc : ∀t1,
       ⊢ t1 ∈ Nat →
       ⊢ scc t1 ∈ Nat
  | T_Prd : ∀t1,
       ⊢ t1 ∈ Nat →
       ⊢ prd t1 ∈ Nat
  | T_Iszro : ∀t1,
       ⊢ t1 ∈ Nat →
       ⊢ iszro t1 ∈ Bool

where "'⊢' t '∈' T" := (has_type t T).

需要主要的是，类型系统是一种保守(conservative)或者说静态(static)的近似方式。类型和项是如何被规约的完全没有关系，特别的，不需要通过一个表达式的normal form来确定类型！
换句话说，别把类型和有没有化简扯上关系。。。

经典形式(Canonical Form)

Lemma bool_canonical : ∀t, ⊢ t ∈ Bool → value t → bvalue t.

Lemma nat_canonical : ∀t, ⊢ t ∈ Nat → value t → nvalue t.

如果我们讨论值(value)的类型，就不难得出以上的结论，两种值分别是两种类型的典型代表～～

0X02 类型的性质

Progress

由于下一条性质我实在是不知道应该如何让翻译=。=，所以都用英文了。
Theorem:
在类型关系系统中, 类型良好的项是一个值或者可以被规约到下一步。
形式化的有：

Theorem progress : ∀ t T,
  ⊢ t ∈ T -> 
  value t ∨ ∃t', t --> t'.

接下来尝试对刚才定义的有bool类型和数字类型的语言证明这条性质

Proof:
对 ⊢ t ∈ T进行归纳证明：

• 由值定义可以知，对于类型规则中的T_Tru， T_Fls, T_Zro直接符合，是平凡的case。
• 当类型关系满足T_Test时有t=test t1 t2 t3,新的goal为

  value (test t1 t2 t3) \/ (∃ t' : tm, test t1 t2 t3 --> t')
  

  有三个较小的命题作为IH

  IHHT1 : value t1 \/ (∃ t' : tm, t1 --> t')
  IHHT2 : value t2 \/ (∃ t' : tm, t2 --> t')
  IHHT3 : value t3 \/ (∃ t' : tm, t3 --> t')
  

  反演IHHT1，
  • 如果value t1时，此时通过T_Test可知t1是一个布尔类型，根据经典形式,t1是一个布尔值(bool value).如果真那么可以步进到t2,假那么步进到t3,故此种情况满足可以向下步进,goal成立.
  • 如果 ∃ t' : tm, t1 --> t',根据ST_Test的步进规则, test t1 t2 t3存在步进, goal成立.
    所以 T_Test时候成立.
• 当类型关系满足T_Scc时有t=scc t1, 此时goal为:

  value (scc t1) \/ (∃ t' : tm, value t1 --> t')
  

  IH为

  IHHT1 : value t1 \/ (∃ t' : tm, t1 --> t')
  

  反演IHHT1,
  • 如果 value t1,此时根据数字的经典形式可以推出, t1 是数字值,1是那么scc t1根据数字值的定义显然也是
  • 如果 ∃ t' : tm, t1 --> t', 这个时候时候符合规则ST_Scc,可以步进.

剩下的其他集中可能性,均与上述证明非常类似.
综上, 我们定义的这种语言具有progress性质.

Q.E.D.

Preservation

这条重要的性质是说
Theorem
在类型关系系统中,如果一个item是类型良好的(well-typed),那么如果它步进规约下去依然是类型良好的.

这条性质也被称为主语规约(subjective reduction),因为类型系统对于语言来说其实非常类似一个谓词逻辑(predicated logic),相当于用一个类型范化了一堆东西的行为,自然是可以被称为谓词,而item在这里就是主语.

形式化的有

Theorem preservation : ∀ t t' T,
  ⊢ t ∈ T →
    t --> t' →
  ⊢ t' ∈ T

对于之前定义的语言,尝试证明上述性质.
Proof
从命题可以看出, 我们希望证明一个类型为T的item在被规约后能够得到一个对应的t'而,t'也有T类型.直觉告诉我们,不同的t对应的t'应该是不同的,所以首先generalize t'.之后对⊢ t ∈ T进行归纳证明:

• 对于T_Fls, T_tru, T_zro之类的Base case, 此时t步进都为自身,当然类型还是T.
• 当T_Test时, 有t=test t1 t2 t3, t1是bool, t2 t3是T类型,代入得到新goal

  test t1 t2 t3 --> t' -> ⊢ t' ∈ T
  

  此时有IH:

   IH1 : ∀ t' : tm, t1 --> t' -> ⊢ t' ∈ Bool 
   IH2 : ∀ t' : tm, t2 --> t' -> ⊢ t' ∈ T
   IH3 : ∀ t' : tm, t3 --> t' -> ⊢ t' ∈ T
  

  此时反演test t1 t2 t3 --> t',根据ST_Test有此时有t'=test t1' t2 t3,并且有t1 --> t1', ,代入后的goal为

  ⊢ test t1' t2 t3 ∈ T
  

  此时由l类型关系的定义T_Test可以指导如果t1'是bool类型,t2 t3是T类型,那么goal成立,对与t2 t3条件中已经成立;根据IH1加上t1是bool不难证明t'也是Bool.
  如果反演时,服从ST_TestTru,ST_TestFls,那么直接根据IH2,IH3可以证明.
• 当T_Scc时, t=scc t1,并且有t1是Nat数字类型. T = Nat

   scc t1 --> t' -> ⊢ t' ∈ Nat
  

  IH为:

  ∀ t' : tm, t1 --> t' -> ⊢ t' ∈ Nat
  

  此时反演scc t1 --> t',可以得出t'=scc t1',且有t1 --> t1',应用IH可以证明
• 当T_isZro时,此时证明与T_Scc类似
• 当T_Prd时, 此时有t = prd t1 T = Nat,t1为Nat类型,代入后goal为

  prd t1 --> t' -> ⊢ t' ∈ Nat
  

  IH:

  ∀ t' : tm, t1 --> t' -> ⊢ t' ∈ Nat
  

  此时反演prd t1 --> t',有两种情况
  • 满足ST_PrdZro时, t1 = zro = t', 自然是Nat类型
  • 满足ST_PrdScc时, nvalue t1,并且t1 = scc t1', t' = t1', 替换可知,scc t1'是Nat,而由此可知,t1'是Nat类型,命题成立.

Q.E.D.

Soundness可靠性

我们之前说了类型系统的出现是为了解决语义中出现有的normal form不是值但是无法再向下规约的情况.所以类型系统自然应该有可靠性的性质.

Corrollary
一个类型良好(well-typed)的item不会遇到阻塞(stuck)的情况.
形式化的有

Corollary soundness : ∀t t' T,
  ⊢ t ∈ T →
  t -->* t' →
  ~(stuck t').

这一点没什么好说的,根据stuck的定义和步进闭包的性质展开后不难看出,这是我们上面证明的两条性质的一个推论.为了练习,还是在这里累赘的证明一下.....毕竟考试万一考呢.....

Proof:
对多步规约t -->* t'进行归纳

• 0次step时, t' = t就是这时候因为t有类型,根据progress性质,t要么是值,要么可以规约到下step.显然不会stuck
• 当遇到中间情况, x 单步到一个中间状态y,并且y能多步到z,goal为 ~(stuck z),归纳假设为t=y时,此时有⊢ y ∈ T -> ~(stuck z) ,根据preservation如果x->y那么x,y同类型,根据归纳假设,命题成立.

Q.E.D.

至此所有重要性质证明完毕.