CS611 Lecture 29 Soundness of Typing Rules 7 November 2001Scribe: Stephen Chong and Prakash Linga Lecturer: Andrew Myers1 Recapitulation of Static Semantics of λ→ e : τ means “e is a well-formed program with type τ”Γ  e : τ means “e is a well-formed program with type τ in typing context Γ” e : τdef⇐⇒ ∅  e : τ1.1 Recasting the Typing Context ΓIn the last lecture, we regarded Γ as being a partial function from Va r to Type:Γ∈ Var Type.This time, we will regard Γ as a syntactic object, defined by the formation rules:Γ ::= ∅|Γ,x:τor, alternatively, as being defined by the following axiom and inference rule:∅ Γ Γ,x:τwhere  Γ means “Γ is a well-formed context.” For notational convenience, a typing context ∅,x1:τ1,...,xn:τncan be written as x1:τ1,...,xn:τn.Order within a typing context Γ is not important since we want them to be isomorphic to partialfunctions. We formalize the unimportance of order by using an equivalence relation ≈ on typing contexts,and the following inference rule that allows us to substitute equivalent contexts when constructing a typingderivation:Γ  e : τ  Γ ≈ ΓΓ e:τ[ctxt-subst]The equivalence relation ≈ on typing contexts is defined by the following rules, plus the usual rules thatensure the relation is reflexive, symmetric, and transitive: Γ,x:τ,x :τ≈ Γ,x:τ[update] Γ,x:τ,x:τ≈ Γ,x:τ,x:τ(x = x) [exchange] Γ ≈ Γ Γ,x:τ ≈ Γ,x:τ[extend]Treating the typing context as a syntactic object, instead of as a partial function, gives us more flexibilityin defining language semantics. For example, we could ensure that no variable could be declared in the scopeof another variable with the same name. Making Γ purely syntactic also makes our proofs a little moremechanical, which is good.11.2 Static SemanticsUsing the typing contexts just defined, we can express the static semantics similarly to the previous lecture;but with explicit well formedness requirements on the typing context. ΓΓ,x:τ  x : τ[var]Γ  e0: τ → τΓ  e1: τ  ΓΓ  e0e1:τ[app]Γ,x:τ  e : τ ΓΓ  (λx:τ.e):τ → τ[abs]2 Denotational SemanticsT [[ 1]] = UT [[ int]] = ZT [[ bool]] = BT [[ τ0→ τ1]] = T [[ τ0]] →T[[ τ1]]C[[ Γ  e : τ]] ρ ∈T[[ τ]] i f ρ |=Γwhereρ |=Γdef⇐⇒ ∀ x, τ . Γ  x : τ ⇒ ρ(x) ∈T[[ τ]]The denotational semantics are defined by induction on typing derivations:C[[ Γ  #u : 1]] ρ = uC[[ Γ  #f : bool]] ρ = trueC[[ Γ  #t : bool]] ρ = falseC[[ Γ  n : int]] ρ = nC[[ Γ  x : τ ]] ρ = ρ(x)C[[ Γ  e0e1: τ]] ρ =(C[[ Γ  e0: τ → τ]] ρ)(C[[ Γ  e1: τ]] ρ)C[[ Γ  (λx:τ.e):τ → τ]] ρ = λv ∈T[[ τ]] . C[[ Γ ,x:τ  e : τ]] ρ[x → v]It is necessary to show that ρ |=Γ⇒ ρ[x → v] |=Γ,x:τ for the last rule to be correct. This is left as anexercise for the reader.2.1 Example of denotational semanticsx:int  x : int∅(λx : int.x):int → intC[[ ∅(λx:int.x):int → int]] ∅ = λv ∈T[[ int]] . C[[ x:int  x : int]] {x → v}= λv ∈ Z.v22.2 A Type for λx. (xx) ?Suppose that x is of type τ , and the term itself is of type τ → τ. Consider the derivation tree for this term:x:τ  x : τ→ τx:τ  x : τx:τ  (xx):τ∅(λx:τ. (xx)) : τ → τFrom this derivation, we can see that τmust be equal to τ. That is, we need a τ such that τ ≡ τ → τ.However, this is not possible, so we cannot assign a type to this term.We have lost some expressive power, although later in the course we will see constructions that allow usto assign a type to this expression.3 Soundness from the Operational PerspectiveWe will now look at the soundness of the typing rules in the operational perspective. What this means is,Typing rules are sound ⇐⇒ no well formed program gets stuck.Note that we use well-formed and well-typed equivalently for this language. To be more precise, e : τ ∧ e −→∗e⇒ (e∈ Value ∨∃e.e−→ e)To show this we will use a 2-step approach. We will show the following two lemmas:• Preservation: As we evaluate a program its type is preserved at each step. e : τ ∧ e −→ e⇒e: τ• Progress: Every program is either a value or can be stepped into another program (and using preser-vation lemma this will be of the same type!) e : τ ⇒ e = v ∈ Value ∨∃e.e −→ eNote that with these two lemmas soundness easily follows. We use induction on the number of steps takenin e −→∗eto show that emusthavethesametypease;theprogress lemma can then be applied to e!Wewill now set out to prove these lemmas.3.1 Proof of Preservation lemmaAssuming e : τ ∧ e −→ ewe need to show that  e: τ.We will do this by well-founded induction on typing derivations. (Note that the typing derivations arefinite and therefore the relation of subderivation is well-founded.) The property we are trying to show ontyping derivations is:P ( e : τ) ⇐⇒ ∀ e.e −→ e⇒ e: τWe define the following for convenience:e0≡ (λx :τ. e1) ve0≡ e1{v/x}Then we have e ≡ C[e0]ande≡ C[e0]. Note that because the typing context is ∅, the [ctxt-subst] rulecannot be useful in proving  e : τ. So we can assume that the proof uses one of the other rules.Now consider the possible forms of e. There are three cases to consider-3• Case 1: C = Ce2.Then e = C[e0]=C[e0] e2.Usingβ-reduction C[e0] −→ C[e0]. Using the rule for application, forsome τ2, C[e0]:τ2→ τ  e2: τ2 C[e0]:τNow  C[e0]:τ2→ τ has a smaller derivation than  e : τ and therefore using the induction hypothesisimplies  C[e0]:τ2→ τ.Sowecanuse: C[e0]:τ2→ τ  e2: τ2 C[e0]:τTherefore P ( e : τ) holds in this case.• Case 2: C = vCSimilar to Case 1.• Case 3: C =[]Now e ≡ e0and e≡ e0. The typing derivation of  e : τ must look like this:x:τ e2: τ (λx:τ.e2):τ→ τ  v : τ (λx:τ.e2) v : τWe need to show that  e2{v/x} : τ using x : τ e2: τ and  v : τ. This follows as a special case ofthe Substitution lemma which we will prove below.3.2 Substitution lemmaΓ,x:τ e : τ