Evaluation-Strategy Translations

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Put $$R=(\lambda u.u)a,D=(\lambda x.fxx)R.$$ One call-by-name step copies the unreduced term $R$. Call by value first reduces $R$ to the value $a$, then substitutes. Call by need instead retains one binding for $R$ and lets both uses of $x$ refer to it. If the calculus records neither suspension nor sharing, the three descriptions have the same ordinary beta normal form and the operational distinction has disappeared.

Linear syntax records it. A term under (!) may be copied; an unboxed term must be used once. The call-by-name translation boxes every argument, the call-by-value translation boxes only values, and the call-by-need translation adds global weakening without adding global contraction. The last change is affinity, not a slogan about lazy evaluation.

One source grammar, two beta disciplines

Fix base types $Z$. The common type and term grammar is $$A,B::=Z\mid A\to B.$$ $$M,N::=x\mid \lambda x.M\mid MN,V::=x\mid \lambda x.M.$$ Contexts are finite maps and admit weakening, contraction, and exchange. The typing rules are the simply typed rules for variables, abstraction, and application. Capture-avoiding substitution is written $M[x:=N]$.

The final sentence matters. Compatible closure may reduce under a lambda or inside either side of an application. Calling the second rule “call by value” describes its beta restriction; it does not select a unique next redex. Deterministic machines require a separate context grammar.

On the opening term, name beta gives $$D⟼fRR,$$ whereas value beta cannot contract the outer redex until $R$ has become a value. The example exhibits duplication, but not an exact cost theorem: compatible reduction can still choose different redex orders.

The linear target makes suspension explicit

The target calculus $\mathsf{lin}$ has $$A,B::=Z\mid !A\mid A⊸B$$ and $$L,M,N::=x\mid !M\mid \mathsf{let}!x=M\mathsf{in}N\mid \lambda x.M\mid MN.$$ An assumption $x:A$ is linear. An exponential assumption $!x:!A$ may be weakened or contracted. Linear abstraction consumes exactly one $x:A$; application splits the context. Promotion derives $!M:!A$ only when every assumption is already exponential. Exponential elimination binds the duplicable assumption $!x:!A$. The complete sheet is in subappendix A.51.

The first two rules remove an introduction followed by its elimination. The last two are administrative: they expose a redex without claiming that a source beta step occurred. Completeness below would be false if these administrative steps were silently quotiented away or added on the source side without a corresponding source rule.

Proof of Lemma 37.3 — Target substitution

Proof. Induct on the typing derivation of $M$. The variable case either returns the derivation of $N$ or rebuilds the unrelated variable. Abstraction renames its binder before applying the induction hypothesis. Application uses the unique premise whose split contains $x$; the other premise is unchanged. For exponential elimination, apply the induction hypothesis in the premise containing $x$ and rebuild the let. Promotion cannot contain a linear $x$; in the exponential case its premise contains only exponential assumptions, so copying the promoted substitution preserves the promotion side condition. Weakening and contraction are rebuilt on exponential assumptions only. ◻

Proof of Theorem 37.4 — Subject reduction for the linear target

Proof. For Lin-Beta and Lin-Bang, invert the typing of the redex and apply lemma 37.3. For Lin-App, the application split and the exponential-elimination split reassociate the same pairwise-disjoint contexts. Rule Lin-Assoc uses the associativity of those splits and alpha-renaming of the inner binder. Compatible positions follow by induction on the surrounding term. ◻

Call by name: box every argument

Define the translation $(-{)}^{\mathsf{n}}$ by $$Z^{\mathsf{n}}=Z,(A\to B{)}^{\mathsf{n}}=!A^{\mathsf{n}}⊸B^{\mathsf{n}},$$ where $y$ is fresh. The exclamation before each argument is the operational choice: the function may discard or duplicate the suspended computation.

Proof of Lemma 37.5 — Name substitution and typing

Proof. The substitution equality is structural induction on $M$, choosing the fresh binder in the abstraction clause away from both substitutions. For typing, induct forward on the source derivation. Source weakening and contraction become the target rules for exponential assumptions; application uses promotion on the translated argument. In the reverse direction, invert the syntax-directed last rule forced by each translated term shape. In particular, a translated application contains exactly one promoted argument, and a translated abstraction contains exactly the displayed exponential let; their inversions recover the source application and abstraction rules. ◻

Proof of Theorem 37.6 — Exact call-by-name translation

Proof. For preservation, a source beta step translates as $$K:=\lambda y.\mathsf{let}!x=y\mathsf{in}{M}^{\mathsf{n}}.$$ Then $$K!N^{\mathsf{n}}{⟶}_{\mathrm{L}\mathrm{i}\mathrm{n}-\mathrm{B}\mathrm{e}\mathrm{t}\mathrm{a}}\mathsf{let}!x=!N^{\mathsf{n}}\mathsf{in}{M}^{\mathsf{n}}{⟶}_{\mathrm{L}\mathrm{i}\mathrm{n}-\mathrm{B}\mathrm{a}\mathrm{n}\mathrm{g}}{M}^{\mathsf{n}}[x:=N^{\mathsf{n}}],$$ which is $(M[x:=N]{)}^{\mathsf{n}}$ by lemma 37.5. Compatible contexts translate compositionally, and induction handles a sequence.

For reflection, consider the target terms reachable from a translation: $$S,T::=x\mid \lambda y.\mathsf{let}!x=y\mathsf{in}S\mid S!T\mid \mathsf{let}!x=!S\mathsf{in}T.$$ Define erasure $S^{\mathrm{♭}}$ by the inverse clauses for variables, abstractions, and applications, and by $$(\mathsf{let}!x=!S\mathsf{in}T{)}^{\mathrm{♭}}=T^{\mathrm{♭}}[x:=S^{\mathrm{♭}}].$$ Induction gives $(M^{\mathsf{n}}{)}^{\mathrm{♭}}=M$. A case analysis on the four target rules shows $S{⟼}_{\mathsf{lin}}T$ implies $S^{\mathrm{♭}}{⟼}^{\ast }{T}^{\mathrm{♭}}$: the two administrative rules erase to rearrangements of the same substitution, while the principal pair erases to beta. Apply this fact along the target sequence and then the right-inverse equation. ◻

Call by value: box only values

Define mutually $A^{\mathsf{v}}$, the unboxed value type $A^{+}$, term translation $M^{\mathsf{v}}$, and value translation $V^{+}$: $$A^{\mathsf{v}}=!A^{+},Z^{+}=Z,(A\to B{)}^{+}=A^{\mathsf{v}}⊸B^{\mathsf{v}},$$ For a source context, put $$(x_1:A_1,\dots ,x_k:A_k{)}^{\mathsf{v}}=!x_1:A_1^{\mathsf{v}},\dots ,!x_k:A_k^{\mathsf{v}}.$$ Every translated term returns a boxed value. An arbitrary argument is not newly boxed at the application site. The outer let therefore waits until the operator exposes a box, and the function’s exponential let waits until the argument does likewise.

For an arbitrary $N$, the outer source redex translates only as far as $$((\lambda x.M)N{)}^{\mathsf{v}}{⟼}_{\mathsf{lin}}^{\ast }\mathsf{let}!x=N^{\mathsf{v}}\mathsf{in}{M}^{\mathsf{v}}.$$ If $N=V$, then $V^{\mathsf{v}}=!V^{+}$, so Lin-Bang continues to $M^{\mathsf{v}}[x:=V^{+}]$. This is the value restriction in target syntax.

Reflection needs the administrative source calculus that the target exposes.

Proof of Lemma 37.8 — Conservative administrative completion

Proof. A value-beta step factors as Let-I followed by Let-V. The reverse implication is Proposition 5.4 of [MOTW99]. Its standard-reduction argument permutes Let-C and Let-A administrative steps until each Let-V exposes one value-beta contraction; between let-free endpoints the introduced lets then occur in Let-I/Let-V pairs. The proposition is imported only for these four compatible rules and the displayed value grammar. It is not a conservativity claim for arbitrary extensions of either language. ◻

Proof of Theorem 37.9 — Exact call-by-value translation

Proof. Structural induction proves $(M[x:=V]{)}^{\mathsf{v}}=M^{\mathsf{v}}[x:=V^{+}]$ and the two mutually stated typing properties. Each of Let-I, Let-V, Let-C, and Let-A translates respectively to a nonempty sequence using the displayed linear beta, bang, application-commuting, and let-association rules. This proves preservation for call by let.

For reflection, the reachable-image grammar distinguishes boxed value images, applications headed by an administrative exponential let, and nested lets. Erase those shapes back to $\mathsf{let}$. The erasure is a right inverse and maps every target step to zero or more call-by-let steps, by inspection of the four target rules. Hence target reduction reflects call-by-let reduction. Finally apply lemma 37.8 at the let-free endpoints. ◻

Call by need: weaken globally, contract only boxes

Call by need keeps the call-by-let syntax and adds garbage collection.

Proof of Corollary 37.11 — Affine target subject reduction

Proof. The four linear rules use theorem 37.4; their typing derivations remain valid because affine weakening only adds derivations. Rule Aff-Weak deletes an unused binding. The reduct omits the bound term’s assumptions, and affine weakening restores them in the conclusion context. Compatible positions follow by induction on the surrounding term. ◻

The call-by-need translation is exactly $(-{)}^{\mathsf{v}}$, now read from $\mathsf{need}$ into $\mathsf{aff}$. Rule Need-G maps to Aff-Weak. This single correspondence explains why the target is affine: an unused suspended computation may disappear before it produces a box, while an unboxed computation still may not be duplicated.

Proof of Theorem 37.12 — Exact call-by-need translation

Proof. The call-by-let cases are those of theorem 37.9. The new source rule translates to $$\mathsf{let}!x=M^{\mathsf{v}}\mathsf{in}{N}^{\mathsf{v}}{⟶}_{\mathrm{A}\mathrm{f}\mathrm{f}-\mathrm{W}\mathrm{e}\mathrm{a}\mathrm{k}}{N}^{\mathsf{v}},$$ because translation preserves free-variable absence. Conversely, extend the reachable-image erasure used for call by value by mapping Aff-Weak to Need-G. Every old affine reduction has the old call-by-let image; the new reduction has exactly the displayed garbage-collection image. The same right-inverse argument reflects a target sequence. ◻

The theorem relates reductions of the two displayed calculi. It does not say that every graph reducer, lazy language, or heap machine implements this relation. In particular, the compatible source relation does not count heap updates. Sharing is represented by the retained let binding and the absence of contraction on its unboxed right-hand side; an exact update-once cost claim would need a heap semantics and a costed simulation.

For the paper’s common extension by constants and primitive delta rules, $\mathsf{need}$ and $\mathsf{name}$ are observationally equivalent: they reduce a closed source term to the same constants. This imported result does not identify their reduction graphs; the discarded and shared work is precisely what can differ.

Three translations, one diagnostic table

The table predicts three useful failures. Boxing every value-translation argument would permit call-by-value functions to consume an unevaluated computation. Removing the call-by-name box would make a nonlinear source function ill typed. Giving $\mathsf{need}$ global contraction would license duplication of an unforced right-hand side and erase the sharing discipline.

Proof of Proposition 37.13 — Opening obstruction

Proof. Put $F=\lambda x.fxx$ and expand the three application clauses. The name clause is $D^{\mathsf{n}}=F^{\mathsf{n}}!R^{\mathsf{n}}$. The other two are $(\mathsf{let}!z=F^{\mathsf{v}}\mathsf{in}z)R^{\mathsf{v}}$. The structural claims then follow from the linear and affine context rules: both restrict contraction to $!x:!A$, while only the affine system admits weakening on an arbitrary $x:A$. ◻

Frozen boundary and practical inspection

The completed results concern simply typed function space, explicit exponentials, compatible reduction, and the displayed let and affine extensions. Products and primitive constants can be added by the source’s stated clauses. Sums, recursion, effects, polymorphism, dependent types, and deterministic machines require new translation and simulation cases. Nothing here transfers an exact cost or full-abstraction theorem to those extensions.

Suggested first pass.

Begin with exercise 37.1, exercise 37.2 and continue with exercise 37.3, exercise 37.4. The practical project is an optional second pass.

None of these problems is a prerequisite for a later chapter.

Exercise 37.6¶

★★★ Complete the call-by-name reachable-image proof: show closure under all four target reductions, define every erasure clause, and prove both the right-inverse and one-step reflection lemmas.

Referenced from 3 locations

• Evaluation-Strategy Translations
• ch:evaluation-strategy-translations: ch:evaluation-strategy-translations

Exercise 37.7¶

★★★ For each rule of $\mathsf{let}$, give its complete nonempty target trace. Then give the erasure image of each target administrative rule and identify where conservativity over let-free value terms is used.

Referenced from 3 locations

• Evaluation-Strategy Translations
• ch:evaluation-strategy-translations: ch:evaluation-strategy-translations

Exercise 37.8¶

★★★ Practical project.evaluation-translation-inspector Use Kappa to implement the three translations on finite named syntax and a classifier for the principal target traces. Maintain this invariant: every reported target step is either the image of the named source step or is explicitly tagged administrative. The corpus must observe the two-step name beta image, reject a value beta whose argument is not a value, accept the same redex after replacing the argument by a value, map source garbage collection to affine weakening, and distinguish boxing every name argument from boxing only value images. Mutate the name application clause by deleting its box; the inline oracle must fail. Explain why these executions do not prove theorem 37.6, theorem 37.9, theorem 37.12. Appendix E records the acceptance commands, and appendix F gives the construction stages.

Referenced from 4 locations

• Evaluation-Strategy Translations
• Object calculus checker and evaluator
• ch:evaluation-strategy-translations: ch:evaluation-strategy-translations

Sources.

The calculi, translations, and exact reduction results are the function-only systems of Maraist, Odersky, Turner, and Wadler [MOTW99]. Their Propositions 2.1–6.7 own subject reduction, confluence, translation exactness, the conservative call-by-let bridge, and the stated observational equivalences. The chapter reconstructs the translation and reflection arguments needed above but does not import the paper’s sketched extensions as if they belonged to the frozen signature. The separate call-by-need calculus of Maraist, Odersky, and Wadler [MOW98] supplies broader operational background; it does not replace the selected translation calculus.