Compiler Theory

Type Safety Proof

Prerequisites

A type safety proof for our languages requires

• principle of implication
  • If P implies Q and P then Q
• principle of induction
  • Let J be some inductively defined judgment, defined by R₁, R₂, …, Rₙ.
  • To prove some property for J, i.e. P(J), it suffices to prove
    1. If P(sub-derivations of R₀) then P(R₀)
    2. If P(sub-derivations of R₁) then P(R₁)
    3. and so on, up to Rₙ.

Examples

We first have to define some equivalence relation a ≡ b**, in order to talk about some results ofeval being equivalent.

v ≡ᵥ v Value equivalence

————————
 n ≡ᵥ n

————————
 b ≡ᵥ b

 v₁ ≡ᵥ v₁'     v₂ ≡ᵥ v₂'
—————————————————————————
 (v₁, v₂) ≡ᵥ (v₁', v₂')

a ≡ b Equivalence

 a ≡ᵥ b
————————
 a ≡ b

 a ≡ b     b ≡ c
—————————————————
      a ≡ c

Theorems

Theorem: for all n, m : Nat, eval(n + add1 m) ≡ eval(add1 n + m).

Proof (by induction on n):

Case 0: eval(0 + add1 m) ≡ eval(add1 0 + m)

• Since 0 + add1 m → add1 m and add1 0 + m → 0 + add1 m → add1 m, eval(0 + add1 m) ≡ eval(add1 0 + m), as desired.

Case add1 n': eval(add1 n' + add1 m) ≡ eval(add1 (add1 n') + m).

• Since add1 n' + add1 m → n' + add1 (add1 m) and add1 (add1 n') + m → add1 n' + add1 m → n' + add1 (add1 m), eval(add1 n' + add1 m) ≡ eval(add1 (add1 n') + m), as desired.

QED.

Theorem: for all n, m : Nat, eval(add1 n + m) ≡ eval(add1 (n + m)).

Proof (by induction on n):

Case 0: eval(add1 0 + m) ≡ eval(add1 (0 + m))

• Since add1 0 + m → 0 + add1 m → add1 m and add1 (0 + m) → add1 m, eval(add1 0 + m) ≡ eval(add1 (0 + m)), as desired.

Case add1 n': eval(add1 (add1 n') + m) ≡ eval(add1 (add1 n' + m))

• Our induction hypothesis is eval(add1 n' + m) ≡ eval(add1 (n' + m))

• Since add1 (add1 n') + m → add1 n' + add1 m and eval(add1 n' + add1 m) ≡ eval(add1 (n' + add1 m)) (by our induction hypothesis), eval(add1 (add1 n') + m) ≡ eval(add1 (n' + add1 m)).

• Also, since add1 (add1 n' + m) → add1 (n' + add1 m), eval(add1 (add1 n' + m)) ≡ eval(add1 (n' + add1 m)).

• Thus, eval(add1 (add1 n') + m) ≡ eval(add1 (add1 n' + m)), as desired.

QED.

Theorem: for all n : Nat, eval(n + 0) ≡ eval(n).

Proof (by induction on n):

Case 0: eval(0 + 0) ≡ eval(0)

• Since 0 + 0 → 0, eval(0 + 0) ≡ eval(0), as desired.

Case add1 m: eval(add1 m + 0) ≡ eval(add1 m)

• Our induction hypothesis is eval(m + 0) ≡ eval(m).

• Since eval(add1 m + 0) ≡ eval(add1 (m + 0)) and eval(m + 0) ≡ eval(m) (by our induction hypothesis), eval(add1 m + 0) ≡ eval(add1 m), as desired.

QED.

Theorem: for all n, m : Nat, eval(n + m) ≡ eval(m + n).

Proof (by induction on n):

Case 0: eval(0 + m) ≡ eval(m + 0)

• Since 0 + m → m, eval(0 + m) ≡ eval(m).

• Since eval(m + 0) ≡ eval(m), eval(m + 0) ≡ eval(0 + m), as desired.

Case add1 n': eval(add1 n' + m) ≡ eval(m + add1 n')

• Our induction hypothesis is eval(n' + m) ≡ eval(m + n'). Hence, eval(add1 (n' + m)) ≡ eval(add1 (m + n')).

• Since eval(add1 n' + m) ≡ eval(add1 (n' + m)), eval(m + add1 n') ≡ eval(add1 m + n'), eval(add1 m + n') ≡ eval(add1 (m + n')), and eval(add1 (n' + m)) ≡ eval(add1 (m + n')), we have eval(add1 n' + m) ≡ eval(m + add1 n'), as desired.

QED.

Type safety proof

Proof (by induction on • ⊢ e : A):

Case Nat: if • ⊢ n : Nat, then eval(n) = n.

• By definition of eval:

     ————————
      n →* n
  —————————————
   eval(n) = n

  as desired.

Case Bool: elided for brevity

Case If: If • ⊢ e : Bool implies eval(e) = v, • ⊢ e₁ : A implies eval(e₁) = v₁, • ⊢ e₂ : A implies eval(e₂) = v₂, then • ⊢ if e then e₁ else e2 implies eval(if e then e₁ else e₂) = v₃.

• This requires proof of canonical form.
  • If Γ ⊢ v : Bool, then v = true or v = false.

Case λ: If x : A ⊢ e : B implies then • ⊢ λx:A.e : A → B implies eval(λx:A.e) = v.

• We are stuck in this case.

A way out

In order to prove type safety, we need to strengthen the theorem: we have to prove progress and preservation instead. In addition, for convenience, we define irreducibles and call values observables.

i ::= x | v | λx:A.`e

Lemma (progress): if • ⊢ e : A then either e is irreducible or e → e’.

Lemma (preservation): if Γ ⊢ e : A and e → e’ then Γ ⊢ e’ : A.

Furthermore, we define valid top level programs ⊢ e in order to rule out evaluating λs at the top level.

⊢ e Valid top level programs

 • ⊢ e : Nat
—————————————
     ⊢ e

 • ⊢ e : Bool
——————————————
      ⊢ e

Type safety, redefined

Theorem (type safety): if ⊢ e then eval(e) = v or eval(e`)** = Ω.

Proof: By progress, since • ⊢ e : A, either e is irreducible or e → e’.

Case e is irreducible: by canonical form, eval(e) = v, either e = n or e = b.

Case e → e’: we must show that either e’ is a value or by progress, e’ can continue computing, i.e. eval(e) = Ω.

Proof of progress

In order to prove progress, we have to change our model to include congruence closure.

We also change syntax for reduction relation to e ⊳ e.

The older syntax e → e is now reserved for congruence closure has all congruence rules (hence the name).

Conversion rules e →* e now only contain reflexivity and transitivity rules.

Also, congruence closure has a new rule.

 e ⊳ e'
————————
 e → e'

Proof (for progress):

Case Var: impossible

Case Add:

 • ⊢ e₁ : Nat     • ⊢ e₂ : Nat
———————————————————————————————
      • ⊢ e₁ + e₂ : Nat

• By the induction hypothesis, e₁ is either irreducible or e₁ → e₁’
• Case e₁ → e₁’: we have e₁ + e₂ → e₁’ + e₂, as desired.
• Case e₁ is irreducible:
  • Case e₂ → e₂’: By Congruence-Add1 rule, i + e₂ → i + e₂’.
  • Case e₂ is irreducible: by canonical form, i₁ + i₂ must step to their sum.

And so on.

Note

Progress and preservation is a particular proof technique to prove type safety.