CS611 Lecture 10 Definitional Translation September 21, 2001Scribe: Andrew Chung and Alexa Sharp Lecturer: Andrew Myers1 Evaluation ContextsIn call-by-name (CBN) lambda calculus we had the following evaluation rules:(λx e0) e1→ e0{e1/x}e0→ e0(e0e1) → (e0e1)We can restate the operational semantics in a different way using evaluation contexts. A context isa program with a hole in it. An evaluation context is a context where the hole is a place we can plugin a reducible expression, or redex.WewriteC ˆtomeananevaluationcontextandC[e]todenotethecontext applied to an expression e (which fills the hole in C). We redefine the call-by-name and call-by-valueevaluation rules in terms of these contexts:For call-by-name:C ::= [ · ] |Ce1C[(λxe0) e1] → C[e0{e1/x}]For call-by-value:C ::= [ · ] |Ce1| v CC[(λx e) v] → C[e{v/x}]where v = λxe2 A Translation FunctionAnother way to understand a language (say, CBN λ-calculus) is to construct a definitional interpreter,aninterpreter for the CBN λ-calculus written in another, better understood language. A related approach isto define a definitional translation, which translates CBN λ-calculus into another language.The call-by-value calculus is a good language to translate other languages to, because it is simple andcorresponds fairly well to what is easy to compile. To show this, we will demonstrate how to translate CBNλ-calculus into CBV λ-calculus by producing a desugaring function D[[ e]] = e,wheree is a CBN term andeis a CBV term that simulates e in some sense.The key problem in translating the lazy CBN calculus to the eager CBN calculus is that we need a wayto “pickle” a (possibly divergent) expression e so that we do not evaluate it right away (eagerly). This isnecessary in our CBN to CBV translation in order to simulate lazy evaluation. We pickle an expression eby wrapping it into a lambda-term:e → (λze) z ∈ FV[[ e]]The right-hand term is called a thunk (The past participle of “think”). The argument z is a dummyvariable, so it doesn’t matter what we apply this function to. We’ll apply it to the simplest closed term,I ≡ λx x.Now let us inductively define D, our translation function:D[[ x]] = ( xI)1D[[ e0e1]] = D[[ e0]] ( λzD[[ e1]] )D[[ λxe]] = ( λxD[[ e]] )We will check this definition by trying it on the test case FA L S E Ω. Recall that FA L SE ≡ λxλy y,Ω ≡ (λx (xx))(λx (xx)). We would (ideally) like to have FA L S E Ω →∗I, as this is how call-by-namewould evaluate the expression. Note that this same expression diverges in the call-by-value calculus. Webegin withD[[ ( λx(λyy)) ((λx(xx)) (λx(xx)))]]= D[[ ( λx(λyy))]] (λzD[[ Ω ]] )=(λx(λy(yI))) (λzD[[ Ω ]] )=(λy(yI))= D[[ λyy]]This evaluation satisfies the following commutation diagram, which seems like a reasonable way to capturethe soundness of the translation:eCBN∗−→ vD↓ D↓D[[ e]]CBV ∗−→ D[[ v]]But we have a problem with this notion of soundness, which is illustrated in the following example.Consider(λy (λx y)) (λw w) → λx (λw w)We’d like to have D[[ λx (λx y)(λw w)]] →∗D[[ λxλw w]] = λxλw (wI). However, our definition above resultsin the following evaluation:D[[ ( λy(λxy)) (λww)]] = λy(λx(yI)) (λz(λw(wI))) →∗(λx(λz(λw(wI))) I) = λxλw (wI)What has happened is that the two right-hand-sides are not exact translations; instead we have an extraλ-term and application introduced by the D function. Thus our commutation diagram needs to look morelike this:eCBN−→ e↓↓D[[ e]]CBV ∗−→ D[[ e]] ≈ eBut the two terms are really equivalent in that if we were allowed to make a β reduction in the middleof the term, then the two will be exactly the same. What we would like to say is that if eCBN−→ e⇒∃ e. D[[ e]]CBV ∗−→ e∧ e≈D[[ e]]3 Equivalence Axioms a nd RulesWe define an equational proof system that allows us to show that two expressions are equivalent. Note thatwe might consider expressions to be equivalent extensionally even though the proof system cannot show it;that’s okay because we only want to be able to show that certain expressions produced by D are equivalent.e ≈ e(reflexive)e≈ ee ≈ e(symmetric)e1≈ e2e2≈ e3e1≈ e3(transitive)e0≈ e0e1≈ e1e0e1≈ e0e1e ≈ eλxe≈ λxe(λxe0) e1≈ e0{e1/x}2These top three rules hold for any equational proof system: they capture the idea that ≈ is an equivalencerelation. The next two rules tell us that substituting equivalent terms results in equivalent terms; a relationwith this property is called a congruence. The final rule says that β-reduction preserves equivalence. For thistranslation, we could in place of the β rule define a more restrictive equivalence rule that captures preciselythe way in which terms can fails to be syntactically equal:z ∈ FV(e0)(λz e0)I ≈ e0With these axioms and rules, we can attempt to prove the soundess prop erty, i.e. eCBN−→ e⇒∃ e. D[[ e]]CBV ∗−→ e∧ e≈D[[ e]]. Equivalently, if we can show that eCBV−→ e⇒D[[ e]] ≈D[[ e]] ,then we can prove the soundness property by induction on the number of evaluation steps.Consider all the steps e → eyou could take with CBN semantics:C ::= [ · ] |Ce1C[(λxe0) e1] → C[e0{e1/x}]We will prove eCBN−→ e⇒D[[ e]] ≈D[[ e]] by induction on the structure of the context CN.ConsiderCN[(λxe0) e1] → CN[e0{e1/x}], where CN=[ · ]orCN= CNe,whereCNis a smaller context than CN(ie,induction hypothesis).If CN=[ · ], then we would like to show that D[[ ( λxe0) e1]] ≈D[[ e0{e1/x}]]. Continuing the evaluation,we have⇒D[[ ( λxe0)]] (λzD[[ e1]] ) ≈D[[ e0{e1/x}]]⇒ (λxD[[ e0]] ) ( λzD [[ e1]] ) ≈D[[ e0{e1/x}]]⇒D[[ e0]] {(λzD[[ e1]] ) /x}≈D[[ e0{e1/x}]]This is an example of a Substitution Lemma. The proof (including the CN= CNe) will be continuednext