CS611 Lecture 24 Soundness of the Typing Rules 25 October 2006Lecturer: Dexter Kozen1 Soundness from the Operational PerspectiveWe will now look at the soundness of the λ→typing rules from the operational perspective. This means:The typing rules are sound ⇐⇒ no well-formed program gets stuck.For this language, well-formed and well-typed are synonymous. To be more precise, let us call e irreducibleand write Irred(e) if there is no reduction possible on e. All values of λ→are irreducible. If e is irreduciblebut is not a value, then e is said to be stuck. We wish to showTheorem 1 (Operational Soundness) ` e:τ ∧ e∗→ e0∧ Irred(e0) ⇒ e0∈ Val ∧ ` e0:τ.We will prove this in two steps using the following two lemmas:Lemma 2 (Type Preservation) Γ ` e:τ ∧ e → e0⇒ Γ ` e0:τ.Lemma 3 (Progress) ` e :τ ∧ Irred(e) ⇒ e ∈ Val.The type preservation lemma says that as we evaluate a program, its type is preserved at each step. Theprogress lemma says that every program is either a value or can be stepped to another program (and by thepreservation lemma, this will be of the same type).Operational soundness follows easily from these two lemmas. Type preservation says every step preservesthe type, so we use induction on the number of steps taken in e∗→ e0to show that e0must have the sametype as e. Then progress can be applied to e0to show that the evaluation isn’t stuck there. We will now setout to prove these two lemmas.2 Proof of the Type Preservation LemmaAssuming that Γ ` e : τ and e → e0, we wish to show that Γ ` e0: τ. We will do this by induction on thewe ll-founded subterm relation.If e → e0, there are three cases corresp onding to the three evaluation rules:e0→ e00e0e1→ e00e1(L)e → e0v e → v e0(R)(λx:σ. e) v → e{v/x}(β)• Case (L): e0e1→ e00e1.Because we have a typing derivation for e0e1, we know that there are typing derivations for e0ande1too. We must have Γ ` e0: σ → τ and Γ ` e1: σ for some type σ. By the induction hypothesis, thereduction e0→ e00also preserves type, so Γ ` e00:σ → τ . Applying the typing rule for applications, wehave that Γ ` e00e1:τ.• Case (R): v e → v e0.This case is symmetrical to case (L). In this case it is the right-hand subexpression making the step.• Case (β): (λx:σ. e) v → e{v/x}.The typing derivation of Γ ` (λx:σ. e) v : τ must look like this:Γ, x:σ ` e:τΓ ` (λx :σ. e):σ → τ Γ ` v : σΓ ` (λx :σ. e) v :τWe want to show that Γ ` e{v/x} :τ using the facts Γ, x:σ ` e:τ and ` v :σ. Our induction hypothesisdoesn’t help us here; we need to prove this separately. It follows as a special case of the substitutionlemma below, which captures the type preservation of β-reduction.13 The Substitution LemmaLemma 4 (Substitution Lemma) ` v :σ ⇒ (Γ, x:σ ` e:τ ⇔ Γ ` e{v/x}:τ).We will prove this by structural induction on e.• Case 1: x /∈ FV(e).This case covers the base cases e ∈ {n, true, false, null} and e = y 6= x and λ-abstractions λx : ρ. e thatbind x. In this case the substitution has no effect and any binding of x in the type environment Γ isirrelevant, thus the lemma reduces to the trivial statement` v :σ ⇒ (Γ ` e : τ ⇔ Γ ` e :τ).• Case 2: e = x.In this case the lemma reduces to` v :σ ⇒ (Γ, x:σ ` x:τ ⇔ Γ ` v :τ),since x{v/x} = v. Since v is closed, the type environment Γ is irrelevant, so the statement furtherreduces to` v :σ ⇒ (x:σ ` x:τ ⇔ ` v :τ).Since types are unique, both sides of the double implication say that σ = τ, so again the lemma reducesto a tautology.• Case 3: e = e0e1.Supp ose ` v :σ.Γ, x:σ ` e0e1:τ ⇔ ∃σ Γ, x:σ ` e0:σ → τ ∧ Γ, x:σ ` e1:σ typing rule for applications⇔ ∃σ Γ ` e0{v/x}:σ → τ ∧ Γ ` e1{v/x}:σ induction hypothesis⇔ Γ ` e0{v/x} e1{v/x}:τ typing rule for applications⇔ Γ ` (e0e1){v/x} : τ definition of substitution.• Case 4: e = λy :ρ. e0, where y 6= x (the case y = x was covered in Case 1).Supp ose ` v : σ. The type of λy : ρ. e0, if it exists, must be ρ → τ for some τ . Similarly, the type of(λy :ρ. e0){v/x} = λy :ρ. (e0{v/x}), if it exists, must be ρ → τ0for some τ0.Γ, x:σ ` (λy :ρ. e0):ρ → τ ⇔ Γ, x:σ, y : ρ ` e0:τ typing rule for abstractions⇔ Γ, y :ρ, x:σ ` e0:τ exchange⇔ Γ, y :ρ ` e0{v/x}:τ induction hypothesis⇔ Γ ` λy : ρ. (e0{v/x}):ρ → τ typing rule for abstractions⇔ Γ ` (λy : ρ. e0){v/x} : ρ → τ definition of substitution.4 Proof of the Progress LemmaTo finish the proof of soundness, it remains to prove the progress lemma. Recall that this lemma states` e:τ ∧ Irred(e) ⇒ e ∈ Val,or equivalently,` e:τ ∧ e /∈ Val ⇒ ∃e0e → e0.2In other words, we cannot get s tuck when evaluating a well-typed expression.We prove the progress lemma using structural induction on e. Recall the definition of a term in λ→:e ::= b | x | λx:τ. e | e0e1,where b denotes a constant. This gives four c ases :• Case e = b.Since b ∈ Val, we are done.• Case e = x.This case is impossible, because we cannot assign a type to x if the type environment is empty.• Case e = λx:σ. e0.Since e ∈ Val, we are done.• Case e = e0e1.We know that there is a type derivation of Γ ` e0e1:τ, and the last step of this derivation must havethe formΓ ` e0:σ → τ Γ ` e1:σΓ ` e0e1:τfor some type σ. By the induction hypothesis, either e0∈ Val or ∃e00e0→ e00, and either e1∈ Val or∃e01e1→ e01. This gives three possibilities:– Both e0and e1are values. Since e0is a value with an arrow type σ → τ, it has to be anabstraction, say e0= λx:σ. e00, and e1is some value v of type σ. Thene = (λx:σ. e00) v → e00{v/x},so e can b e further reduced.– e0is not a value. Then ∃e00e0→ e00, and we havee0→ e00e0e1→ e00e1,so e = e0e1can be further reduced.– e0is some value v, but e1is not a value. Then ∃e01e1→ e01, and we havee1→ e01v e1→ v e01,so e = v e1can be further reduced.This completes the pro