CS611 Lecture 9 Semantics via Translation 18 September 2006Lecturer: Dexter Kozen1 OverviewOur goal is to study basic programming language features using the semantic techniques we know:• small-step operational semantics;• big-step op e rational semantics;• translation.We will mostly use small-step semantics and translation.2 TranslationFor translation, we map well-formed programs in the original language into items in a meaning space. Theseitems may be• programs in an another language (definitional translation);• mathematical objects (denotational semantics); an example is taking λx : int. x to {(0, 0), (1, 1), . . . }.Because they define the meaning of a program, thes e translations are also known as meaning functionsor semantic functions. We usually denote the semantic function under consideration by [[·]]. An object e inthe original language is mapped to an object [[e]] in the meaning space under the semantic function. We mayoccasionally add an annotation to distinguish between different semantic functions, as for example [[e]]cbnorC[[e]].3 Translating CBN λ-Calculus into CBV λ-CalculusThe call-by-name (lazy) λ-calculus was defined with the following reduction rule and evaluation contexts:(λx. e1) e2→ e1{e2/x} E ::= [•] | E e.The call-by-value (eager) λ-calculus was similarly defined with(λx. e) v → e{v/x} E ::= [•] | E e | v E.To translate from the CBN λ-calculus to the CBV λ-calculus, we define the semantic function [[·]] byinduction on the syntactic structure:[[x]]4= x · ID[[λx. e]]4= λx. [[e]][[e1e2]]4= [[e1]] (λz. [[e2]]), where z /∈ FV([[e2]]).The idea is to wrap the parameters to functions inside λ-abstractions to delay their evaluation, then tofinally pass in a dummy parameter to expand them out.For an example, recall that we defined:true4= λxy. xfalse4= λxy. yif4= λxyz. xyz.1The problem with this construction in the CBV λ-calculus is that if b e1e2evaluates both e1and e2,regardless of the truth value of b. Perhaps the conversion above can be used to fix these to evaluate themlazily.[[true ]] = [[λxy. x]]= λxy. [[x]]= λxy. x ID[[false ]] = λxy. y ID[[if ]] = [[λxyz. xyz ]]= λxyz. [[(xy)z ]]= λxyz. [[xy ]] (λd. [[z ]])= λxyz. [[x]] (λd. [[y ]]) (λd. [[z ]])= λxyz. (x ID) (λd . y ID) (λd. z ID).This is not a complete solution, as the conversion does not work for all expressions, but only fully convertedones. But if use d as intended, it has the desired effect. For example, e valuating under the CBV rules,[[if true e1e2]] = [[if ]] (λd. [[true ]]) (λd. [[e1]]) (λd. [[e2]])= (λxyz. (x ID) (λd. y ID) (λd. z ID)) (λd. [[true ]]) (λd. [[e1]]) (λd. [[e2]])→ ((λd. [[true ]]) ID) (λd. (λd. [[e1]]) ID) (λd. (λd. [[e2]]) ID)→ [[true ]] (λd. [[e1]]) (λd. [[e2]])= (λxy. x ID) (λd. [[e1]]) (λd. [[e2]])→ (λd. [[e1]]) ID→ [[e1]],and e2was never evaluated.4 AdequacyBoth the CBV and CBN λ-calculus are deterministic systems in the sense that there is at most one reductionthat can be p erformed on any term. When an expression e in a language is evaluated in a deterministicsystem, one of three things can happen:1. The computation can converge to a value: e ⇓ v.2. The computation can converge to a non-value. When this happens, we say the computation is stuck.3. The computation can diverge: e ⇑.A semantic translation is adequate if these three behaviors in the s ource system are accurately reflectedin the target system, and vice versa. One aspect of this relationship is captured in the following diagram:[[e]]ev0v[[v ]]6?6?--@@@@R∗∗≈If an expression e converges to a value v in zero or more steps in the source language, then [[e]] mustconverge to some value v0that is equivalent (e.g. β-equivalent) to [[v ]], and vice-versa. This is formallystated as two properties, soundness and completeness. For our CBN-to-CBV translation, these propertiestake the following form:24.1 Soundness[[e]]∗−→cbvv0⇒ ∃v e∗−→cbnv ∧ v0≈ [[v ]]In other words, any computation in the CBV domain starting from the image [[e]] of a CBN program e mustaccurately reflect the com putation in the CBN domain.4.2 Completenesse∗−→cbnv ⇒ ∃v0[[e]]∗−→cbvv0∧ v0≈ [[v ]]In other words, any computation in the CBN domain starting from e must be accurately reflected by thecomputation in the CBV domain starting from the image [[e]].4.3 NonterminationIt must also be the case that the source and target agree on nonterminating executions. We write e ⇑ andsay that e diverges if there exists an infinite sequence of expressions e1, e2, . . . such that e → e1→ e2→ . . . .The additional condition for adequacy ise ⇑cbn⇔ [[e]] ⇑cbv.The direction ⇐ of this implication can be considered part of the requirement for soundness, and the direction⇒ can be considered part of the requirement for completeness. Adequacy is the combination of soundnessand c ompletenes s.5 Untyped ML (uML)Let’s construct an example by augmenting the λ-calculus with some more conventional programming con-structs and defining its translation to the CBV λ-calculus. We call this language uML since it resemblesML, with the “u” standing for “untyped”.5.1 Expressionse ::= λx1. . . xn. e | e0· · · en| x | n | true | false| (e1, . . . , en) | #n e | if e0then e1else e2| let x = e1in e2| letrec f1= λx1. e1and . . . and fn= λxn. enin e5.2 Valuesv ::= λx1. . . xn. e | n | true | false | (v1, . . . , vn)5.3 Evaluation ContextsE ::= [•] | v0· · · vmE em+2· · · en| #n E| if E then e1else e2| let x = E in e| (v1, . . . , vm, E, em+2, . . . , en)35.4 Reductions(λx1. . . xn. e) v1· · · vn→ e{v1/x1}{v2/x2} · · · {vn/xn}#n (v1, . . . , vm) → vn, where 1 ≤ n ≤ mif true then e1else e2→ e1if false then e1else e2→ e2let x = v in e → e{v/x}letrec . . . → to be continuedWe can already see that types will be important for establishing soundness. For example, what happenswith the expression if 3 then 1 else 0? The evaluation is stuck, because there is no reduction rule thatapplies to this term.5.5 Translating uML to the CBV λ-CalculusWe define some of the translation rules:[[λx1. . . xn. e]]4= λx1. . . xn. [[e]][[e0· · · en]]4= [[e0]] [[e1]] [[e2]] · · · [[en]][[x]]4= x[[n]]4= λfx. fnx[[true ]]4= λxy. x ID[[false ]]4= λxy. y ID[[if e0then e1else e2]]4= [[e0]] (λz. [[e1]]) (λz. [[e2]]).Revisiting our earlier example if 3 then 1 else 0, we see that the translation to CBV is not sound,because its