ch:evaluation-strategy-translations: ch:evaluation-strategy-translations

Name reduction may contract the outer redex first: $$(\lambda x.fxx)R⟼fRR⟼faR⟼faa.$$ The first arrow creates the two copies of the unreduced argument. Value reduction must first use $$R=(\lambda u.u)a⟼a.$$ Compatibility then gives $$(\lambda x.fxx)R⟼(\lambda x.fxx)a⟼faa.$$ Only the second arrow substitutes twice, and it copies the value $a$, not the redex $R$.

Put $F=\lambda x.fxx$. The application clause gives $$(FR{)}^{\mathsf{n}}=(\lambda y.\mathsf{let}!x=y\mathsf{in}{f}^{\mathsf{n}}xx)!R^{\mathsf{n}}.$$ The principal trace is $${⟶}_{\mathrm{L}\mathrm{i}\mathrm{n}-\mathrm{B}\mathrm{e}\mathrm{t}\mathrm{a}}\mathsf{let}!x=!R^{\mathsf{n}}\mathsf{in}{f}^{\mathsf{n}}xx{⟶}_{\mathrm{L}\mathrm{i}\mathrm{n}-\mathrm{B}\mathrm{a}\mathrm{n}\mathrm{g}}{f}^{\mathsf{n}}{R}^{\mathsf{n}}{R}^{\mathsf{n}}.$$ The single promotion $!R^{\mathsf{n}}$ licenses exponential elimination; the resulting exponential assumption for $x$ licenses both occurrences. No other box is introduced around the argument.

Expansion and the first two administrative target contractions give $$((\lambda x.M)N{)}^{\mathsf{v}}{⟼}_{\mathsf{lin}}^{\ast }\mathsf{let}!x=N^{\mathsf{v}}\mathsf{in}{M}^{\mathsf{v}}.$$ For an arbitrary $N$, the right-hand side need not expose a bang, so Lin-Bang need not apply. If $N=V$, then $V^{\mathsf{v}}=!V^{+}$, and the trace continues to $M^{\mathsf{v}}[x:=V^{+}]$. Replacing the application argument by $!N^{\mathsf{v}}$ would expose a bang even when $N$ is an application; the target could then enter the body before the source value-beta premise was satisfied.

The translation is $$\mathsf{let}!x=R^{\mathsf{v}}\mathsf{in}!a.$$ Because $x$ is absent from the body, Aff-Weak reduces it to $!a$. Suppose $R^{\mathsf{v}}$ uses a linear assumption $r:C$. The redex is typed in context $r:C$, but the reduct $!a$ uses no $r$. The linear target has no weakening rule for $r:C$, so the same-context subject-reduction conclusion is unavailable. Affine weakening derives it, which is why the call-by-need target is not $\mathsf{lin}$.

For name erasure, a Lin-Beta/Lin-Bang principal pair maps to one source beta step. A Lin-App or Lin-Assoc step maps to zero source steps: erasure performs the same substitution on both sides. Under call-by-let erasure, Lin-Beta, Lin-Bang, Lin-App, and Lin-Assoc correspond respectively to the source families Let-I, Let-V, Let-C, and Let-A, allowing a short nonempty sequence when the target exposes two principal rules at once. The last two source rules are required because the target can commute an exponential let through application or another let before a value is exposed.

Use the grammar in the proof of theorem 37.6. Variables have themselves as erasure; translated abstractions erase to source abstractions; $(S!T{)}^{\mathrm{♭}}=S^{\mathrm{♭}}{T}^{\mathrm{♭}}$; and $$(\mathsf{let}!x=!S\mathsf{in}T{)}^{\mathrm{♭}}=T^{\mathrm{♭}}[x:=S^{\mathrm{♭}}].$$ Structural induction proves $(M^{\mathsf{n}}{)}^{\mathrm{♭}}=M$. For closure, Lin-Beta creates the fourth grammar form, Lin-Bang removes it, and the two commuting rules only reassociate the third and fourth forms. Case analysis gives one source beta step for the principal pair and reflexivity for each commuting image. Induction on target sequence length yields reflection.

Rule Let-I exposes the operator box with Lin-Bang, contracts the linear application with Lin-Beta, and leaves the translated source let. Rule Let-V is Lin-Bang. Rule Let-C is Lin-Assoc followed by Lin-App; Let-A is Lin-Assoc. Fresh binders are chosen before every trace.

The reachable-value erasure maps a boxed value image to a source value, the administrative operator let to its source application, and a general exponential let to source let. Thus each target rule maps to zero or more call-by-let steps and the erasure is a right inverse. This proves exactness for $\mathsf{let}$. Proposition 5.4 of [MOTW99] is used only after both endpoints are let-free; it converts that call-by-let reduction to call-by-value reduction.