CS611 Lecture 31 Logical relations: strong normalization November 12, 2001Scribe: Andrew Chung, Bill McCloskey Lecturer: Andrew Myers1 Strong NormalizationRecall from before that λ→is a typed version of the lambda calculus with lambda terms of the formλx:τ. eA language has the property of strong normalization if every expression can be normalized, or evaluated toa value. The language λ→has this property. Such languages are not as expressive as languages without strongnormalization, since the halting problem is solvable. But they are useful for more restricted applicationswhere termination is desirable, such as modelling the properties of other languages.There are two ways to show that a language exhibits strong normalization. The first is to show thatthe operational semantics agrees with the denotational semantics. The other is to show directly that everyexpression can be normalized.2 Agreement between SOS and Denotational SemanticsUsually, to show the two semantics agree, it is sufficient to show that e ⇑ ⇐⇒ C[[` e : B]]ρ =⊥. Any otherdifference between the SOS and denotational semantics can be transformed into expressions that diverge inonly one of the semantics.The argument for equivalence can be formalized in two statements.• Soundness: e 7−→∗v ⇒ C[[` e : τ]]ρ = C[[` v : τ]]ρ• Adequacy: e 7−→∗b ⇐ C[[` e : B]]ρ = C[[` b : B]]ρb:B is a base value. Notice that the meanings are actually equal, and not merely equivalent, as has b een thecase before. The first condition states that if e evaluates to a value in the operational semantics, then themeaning of e is equal to the meaning of the value. The second condition only needs to be proved for basevalues. If there is a difference in an expression that has a non-base type, base values can be extracted fromthe term, the equivalence can be proved, and the based values can be wrapped back into the expression.3 Proof of Strong Normalization3.1 Logical RelationsHowever, a more direct statement will be proved in this lecture. It will be shown that ` e : τ ⇒ ∃v. e 7−→∗v.This statement will be proved using logical relations. A logical relation is a relation defined on terms andindexed by types. e Rτe0is a relation on expressions e and e0of type τ . Logical relations can be used toprove properties of terms using induction over typing derivations.In this case, a unary relation Rτwill be used. Rτessentially behaves like a set, so that Rτe ⇐⇒ e ∈ Rτ.Rτwill be defined as the set of terms of type τ which terminate and which preserve termination behavior.Formally,e ∈ RB⇐⇒ ` e : B ∧ ∃v. e 7−→∗ve ∈ Rτ →τ0⇐⇒ ` e : τ → τ0∧ ∃v. e 7−→∗v ∧ ∀e0∈ Rτ. ( e e0) ∈ Rτ0B is any of the three base types: 1, bool, or int. Note that although e may have type B, it is not necessarilya base value, syntactically. For example, the term (λx : 1. 2) #u ∈ Rint, but it is not a base value. Also,notice the last clause of the second condition. It states that when the function is applied to a term thatterminates, the result of the application must terminate. This clause captures the essence of the logicalrelations approach.13.2 A Substitution OperatorNow the goal is to prove ` e : τ ⇒ e ∈ Rτ. If this were true, it would imply ∃v. e 7−→∗v by the definition ofRτ. Unfortunately, it is not possible to directly prove this goal. The hypothesis is too weak, since it is onlyvalid in an empty typing context. But to prove the statement in a typing context Γ, a special substitutionoperator will be needed to ensure that the term remains in Rτeven after substitution.The substitution operator γ ∈ Var * Expr will be defined. In some sense, γ must agree with the typingcontext Γ. Any substitution made for a variable x must have type Γ(x) and must be in RΓ(x). Define γ |= Γto be true when the domains of γ and Γ are equal and when ∀x ∈ dom(γ). γ(x) ∈ RΓ(x). Then define anoperator ˆγ ∈ Expr → Expr that applies the substition γ on an entire expression. Formally this operatorˆ·is defined on an arbitrary γ as follows, by structural induction:ˆγ(x) =nγ(x) if x ∈ dom(γ)x otherwiseˆγ(b) = bˆγ(e0e1) = ˆγ(e0) ˆγ(e1)ˆγ(λx:τ. e) = λx:τ. ˆγx(e)γx=½γ if x 6∈ dom(γ)γ − hx, γ(x)i otherwiseNow the new goal, using the substitution operator, is Γ ` e : τ ∧ γ |= Γ ⇒ ˆγ(e) ∈ Rτ. This goal isa generalization of the previous goal, with γ = Γ = ∅. The proof of this statement will use a substitutionlemma Γ ` e : τ ∧ γ |= Γ ⇒ ` ˆγ(e) : τ . The proof of this lemma is similar to the proof of other substitutionlemmas, and will be omitted. The substitution lemma is needed to ensure that ` ˆγ(e) : τ (note the lack ofa typing context), which is required by the definition of Rτ.Another lemma is also used in the proof below. It states that Γ ` e : τ ∧ e 7−→∗e0∧ e0∈ Rτ⇒ e ∈ Rτ.If e steps to e0, and e0terminates, then e also terminates, and types are preserved across the step. The proofof this lemma is left as an exercise.3.3 Proof of Strong NormalizationRecall the syntax of λ→. It will be useful during the proof.e ::= b | x | e0e1| λx:τ. eCase 1. Assume e = b, a base value. Clearly ` e : B. It is necessary to show that Γ ` b : B ∧ γ |= Γ ⇒ˆγ(b) ∈ RB. Since b is a base value, it is a value, so b 7−→∗v = b. Therefore b = ˆγ(b) ∈ RB.Case 2. Assume e = x, a variable. It is necessary to show that Γ ` x : τ ∧ γ |= Γ ⇒ ˆγ(x) ∈ Rτ.Now since x is a variable, τ = Γ(x), and so x ∈ dom(Γ). Therefore, because γ |= Γ, γ(x) ∈ Rτanddom(γ) = dom(Γ). And finally, since ˆγ(x) = γ(x), ˆγ(x) ∈ Rτ.Case 3. Assume e = e0e1. It is necessary to show that Γ ` e0e1: τ ∧ γ |= Γ ⇒ ˆγ(e0e1) ∈ Rτ. Atyping derivation exists for Γ ` e0e1: τ, and it must have the formΓ ` e0: τ0→ τ Γ ` e1: τ0Γ ` e0e1: τTherefore, there are derivations for the two typing judgments in the antecedent of the inference rule. So,by the induction hypothesis, ˆγ(e0) ∈ Rτ0→τand ˆγ(e1) ∈ Rτ0. By the definition of Rτ0→τ, ˆγ(e0e1) =ˆγ(e0) ˆγ(e1) ∈ Rτ, since ˆγ(e1) ∈ Rτ0.Case 4. Assume e = λx:τ. e0. It is necessary to show thatΓ ` (λx:τ. e0) : τ → τ0∧ γ |= Γ ⇒ ˆγ(λx : τ. e0) ∈ Rτ →τ0By the definition of ˆγ, ˆγ(λx : τ. e0) = λx:τ. ˆγx(e0), which is a value. Using the assumptions, the