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

Problem, result, and invariant. Implement the name and value translations on finite syntax and classify the principal name, value, and need steps. The result is an inspectable five-case trace. Maintain one invariant: every reported target step is either the image of the source redex named by the case or carries an explicit administrative tag. The program must never report an administrative commute as source beta.

Representation. Use one Source datatype with variables, lambdas, applications, and source lets. Use a separate Target datatype with variables, lambdas, applications, bang, and exponential let. Represent variable names by natural numbers. Separate datatypes prevent a source let from being confused with an exponential target let.

Named syntax keeps the printed clauses recognizable. A de Bruijn representation would simplify alpha-equivalence, but it would add shifting machinery unrelated to this corpus. The inspector performs no substitution, so natural-number names are enough for the selected observations.

First complete version. Implement translateName by structural recursion. Its application clause constructs TApp. Set its function field to translateName applied to the source function. Set its argument field to TBang around translateName of the source argument. Then recognize a source application headed by a lambda and return the two principal tags Lin-Beta and Lin-Bang. Test the translated identity application before adding the other strategies.

Remaining cases. Define translateValue mutually with the unboxed translateValuePlus; only source variables and lambdas count as values. The application clause introduces an operator TLetBang but no new argument bang. Add a free-occurrence predicate that respects lambda and let binders. A need-garbage candidate is accepted only when its binder is absent from the body, in which case its target tag is Aff-Weak.

A failing version. Delete TBang from the name application clause. The translator still typechecks as Kappa data and audits cleanly, but the nonvalue boxing comparison fails. As a second mutation, make isValue return true on applications; the value classifier then accepts the deliberately blocked redex. These mutations distinguish Kappa type safety from correctness of the encoded translation.

Acceptance test. Run the four commands in appendix E. Require these five outcomes:

• name beta has the two-principal-step image;

• value beta rejects the nonvalue argument;

• value beta accepts the corresponding lambda argument;

• need garbage collection maps to affine weakening; and

• name boxes a nonvalue argument while value does not.

The final summary must report five passing cases, and the audit must print [].

Mathematical boundary. The artifact computes two syntax translations and five finite classifications. It does not implement capture-avoiding substitution or arbitrary reduction closure and therefore proves no typing theorem, simulation, reflection, conservativity, observational equivalence, confluence, or cost bound. Those claims belong to the chapter’s mathematical development.