Optimal sharing, readback, and cost

The imported signature has finite untyped lambda terms, ordered buses, root/void/croissant/bracket/fan nodes, the six Figure 2 bus-rule schemes without optional garbage rules, the diagrammatic §4.1 translation $\mathcal{G}$, and the access-path readback $\mathcal{R}$. Full graph reduction is ${⟶}_{\mathrm{GAL}}$; $\underset{\mathrm{GAL}:(u,v)}{\overset{a}{\to }}$ names only a labeled rightmost-fan subcase. A graph is in the theorem’s domain when it is reachable from $\mathcal{G}(M)$.

Gonthier–Abadi–Lévy Theorem 3 gives initial readback, multi-step readback simulation, and graph-normal-to-beta-normal reflection. Theorem 4 gives uniqueness of rightmost-fan redex labels and therefore nonduplication of Lévy-family work. Both have proof sketches in the local author copy at printed pp. 11–12, and §4.1 calls the translation informal because it relies on left/right bus structure. A general reduction may still perform work in a subterm later found useless; a normal-order strategy avoids that work. No wall-clock, memory, or scheduler theorem is inherited.

Asperti–Mairson use explicitly typed closed simply typed lambda terms, their type-sensitive size, one complete Lévy-family contraction per parallel beta step, first-class machines up to polynomial simulation slowdown, and $K_0(n)=n$, $K_{j+1}(n)=2^{K_j(n)}$.

Theorem 5.3 gives the nonelementary machine-time lower bound despite linearly many parallel steps. Corollary 5.4 transfers the bound to local interactions of Lamping’s graph-reduction algorithm, including croissant/bracket bookkeeping. Corollary 5.6 separates ordinary and parallel beta counts. These statements do not transfer to an arbitrary reducer without a simulation and cost relation.

The Kappa companion implements only the opening one-node let-graph and a finite certificate-syntax checker. It validates endpoint tags, beta paths, and label uniqueness supplied as data. It does not construct $\mathcal{G}(M)$, recognize GAL incidence, prove label propagation, or establish either imported theorem family.

GAL §§3.3–4.1, 5.2–5.3, and 6.1 plus Theorems 3–4 fix the graph interface and qualification. Asperti–Mairson Definition 3.1, Theorem 5.3, and Corollaries 5.4 and 5.6 fix the typed cost interface and lower bounds.