type safety

Posted on In Views:

There are two kinds of semantics for a programming language.

  • dynamic semantic, which is opeartional semantic
  • static semantic, which is type system

Type safety

  • progress if ∅ Γ e:A then either e:value, or e ↦ e'
  • preservation if Γ ⊢ e:A, e ↦ e' then Γ ⊢ e':A

"well typed expr can not go wrong"

e:A e:value e ↦ e' e':A

Prove of type preservation

If Γ ⊢ e:C and e ↦ e', then Γ ⊢ e':C If e ↦ e', then Γ ⊢ e:C implies Γ ⊢ e':C Proof By rule induction on e ↦ e'

case)

case)

...

case) λx:A.e v ↦ [v|x]e Γ ⊢ (λx:A.e)v:C Γ ⊢ [v|x]e:C

We consider the most challenge case to prove. 

1
2
3
4
5
Γ, x:A ⊢ e:C
----------------
Γ ⊢ λx:A.e:A→C  Γ ⊢ v:A
--------------------
      Γ ⊢ (λx:A.e)v:C

Γ ⊢[v|x]e:C - NTS

recursive to prove: If e ↦ e', then Γ ⊢ e:C implies Γ ⊢ e':C

so we introduce substitution lemma

If Γ ⊢ e:A and Γ,x:A ⊢ e':C, then Γ ⊢ [e|x]e':C Proof By rule induction on Γ, x:A ⊢ e':C By Curry-Howard isomorphism, it's equal to prove If Γ,x:A ⊢ e':C then (Γ ⊢ e:A implies Γ ⊢ [e|x]e':C)

case 

1
2
3
4
5
6
7
8
9
10
--------------------Var  e'=x, C=A
Γ, x:A ⊢ e':C

Γ ⊢ e:A                        assumption

Γ ⊢ [e|x]e':C
  = [e|x]x
  = e:C


case 

1
2
3
4
5
6
7
8
9
10
11
    y:C ∈ Γ
--------------------Var  e'=y≠x
Γ, x:A ⊢ e':C
         y:C
Γ ⊢ e:A                        assumption



Γ ⊢ [e|x]e':C
  = [e|x]y:C
  = y:C

If Γ,x:A ⊢ e':C then (Γ ⊢ e:A implies Γ ⊢ [e|x]e':C)

case 

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

Γ, x:A, y:C₁ ⊢ e'':C₂
-------------------- → I where C=C₁→C₂
Γ, x:A ⊢ e':C
         λy:C₁.e'':C


Γ ⊢ e:A                        assumption
Γ, y:C₁ ⊢ e:A                  by weakening
Γ, y:C₁ ⊢ [e|x]e'':C₂          by IH on the premise


Γ, λy:C₁ ⊢ [e|x]e'':C₂     <- NTS
Γ ⊢ λy:C₁[e|x]e'':C₁→C₂     <- NTS
Γ ⊢ [e|x]λy:C₁.e'':C        <- NTS
Γ ⊢ [e|x]e':C                <- NTS