ch:optimal-sharing: ch:optimal-sharing

Represent lambda terms by Var, Lam, and App. Represent the opening labeled term graph by Shared, carrying its node name, family label, stored definition, and body. Implement capture-avoiding named substitution with binder freshening, alpha-equivalence, graph readback, and the shared-beta clause before any certificate code. Check that contracting the opening graph preserves node 10 and label 17, changes its readback from the duplicated residual term to $zz$, and that the complete two-step beta path is valid. Add the crossed-binder redex $(\lambda 1.\lambda 2.1)2$ and accept a freshened result modulo alpha.

Represent one richer contraction certificate as a TraceEntry containing two FanEndpoints, a natural-number family label, and a ReadbackWitness. Implement alpha-equivalence and isBetaStep, which checks a root contraction or one congruence step below a constructor. Then make readbackWitnessValid check every adjacent pair of a path containing at least two terms. Implement rightmostPairValid for distinct endpoint identifiers with opposite left/right-rightmost tags and labelMember for claimed-family-label uniqueness. These are checks on the certificate syntax, not reconstructions of general graph incidence or label propagation. Maintain the invariant that every accepted entry has distinct endpoints with opposite rightmost tags, a nonempty verified beta path, and a label absent from the accepted prefix. The accepted two-entry case conjoins the opening graph checks with the two-entry trace audit.

Build six named checks. The empty trace checks the base case, the accepted two-entry trace uses labels 17 and 29, and the crossed-binder redex checks freshening and alpha-equivalence. Isolate three negative traces: one has an auxiliary fan port, one jumps directly over two beta contractions, and one repeats label 17. Print exactly

PASS empty trace accepted
PASS valid two-entry trace accepted
PASS capture-avoiding beta accepted modulo alpha
PASS malformed rightmost-fan pair rejected
PASS non-beta readback step rejected
PASS repeated family label rejected
All 6 Chapter 42 corpus cases passed.

Run the four commands recorded in appendix E and require the audit result []. Then apply each independent mutation from artifacts/ch42-optimal-sharing/MUTATIONS.md. Re-run check and audit to confirm that every mutant still belongs to the portable language profile, and require the frozen test oracle to fail at exactly the graph-label, pair, beta-step, or repeat case whose validation was removed or corrupted.

Finally compare the certificate fields with the two cited Gonthier–Abadi–Lévy theorems: record the finite untyped source calculus, translation $\mathcal{G}$, labeled graph relation ${⟶}_{\mathrm{GAL}}$, rightmost-fan pair, claimed label, readback $\mathcal{R}$, and distinct-label premise. The implementation constructs the displayed one-node graph, validates supplied finite certificate data, and checks the supplied beta path. It neither synthesizes that path nor proves the richer fields’ graph-semantic origin.

Representation comparison. A flat list of TraceEntry records keeps every supplied endpoint, label, and readback path visible to the oracle and makes duplicate-label checking a finite list traversal. A direct adjacency graph with typed port maps could make malformed incidence harder to express, but implementing it would require the imported fan grammar and propagation rules that this capsule does not reconstruct. Use the flat certificate representation here so the executable boundary agrees with the chapter’s finite auditor.

Theorem boundary. The run illustrates the sharing and readback mechanism that motivates the imported Gonthier–Abadi–Lévy readback and Lévy optimality theorem; the one-node fragment is not itself an instance of their full graph calculus. It does not prove that the supplied endpoints are facing fans, that their labels arose by graph propagation, or that no Lévy family is contracted twice in an arbitrary reduction. Those claims remain the mathematical content of theorem 42.6.