ch:partial-evaluation: fuelled numeric specialization

Problem, result, and invariant. Build an online specializer that folds static arithmetic, residualizes dynamic tests, and cannot unfold a recursive call after its budget is exhausted. The result of specialization is either a known natural number or printed residual syntax. Maintain three invariants: every free variable in the residual occurs free in the input outside the static environment; two visits to the same function-and-static-argument state reuse the same residual name; and every frontier call is backed either by a completed residual equation or by a call-reachability-closed retained source equation.

Representation tradeoff. The companion uses constructors for numerals, the variables $x$ and $y$, addition, multiplication, and zero tests. It represents residual expressions by strings, but represents residual calls and equations by separate ResidualCall and Equation constructors. Consequently the closure oracle is computed by traversing equation targets and retained source names; it is not a printed Boolean fixture. Strings keep the residual arithmetic examples small, but the host cannot subsequently typecheck or traverse those expressions. A single residual abstract-syntax tree would support both operations and alpha-aware memoization; it would also require a pretty-printer and a separate equality decision. The mixed representation is adequate only because Scheme0 here has fixed variable names and no binder.

First complete version. Begin with Num, X, Y, and Add. Constants produce Known; variables produce Residual. Specializing addition specializes both operands, returns Known (a + b) when both are known, and otherwise prints the two residual operands with a plus sign. This version already computes a useful end-to-end result: specialization of 2 + 3 returns five, whereas specialization of x + 3 returns (x + 3).

Remaining cases. Add multiplication by the same known/residual split. Add a structurally recursive specializePower; the power-3 fixture must invoke this function rather than supply an already-unrolled term. Add zero tests next: select a branch only when the scrutinee is known, and otherwise residualize the test after specializing both branches. Add calls last, because they combine both control mechanisms. At fuel zero return the call and the reachable retained equation. At positive fuel consult the memo list; a hit returns the installed residual name, and a miss installs the state before recursively constructing its completed equation at predecessor fuel. The same fixture revisits one installed state; loop changes its static argument and reaches the fuel boundary. The call case is the proof-emphasized case of theorem 127.9: every recursive premise consumes one fuel unit, and a memo hit performs no unfolding.

Observable result. The accepted program prints the specialized third power, a dynamic conditional whose static branch is five, the retained closure at fuel zero, two completed loop equations followed by a retained equation, a genuinely reached self-recursive memo hit, and closure-check: computed closed. It ends with All 6 Chapter 127 corpus cases passed.

A failing version. Change the static addition result from Known (a + b) to Known a. The program still typechecks, and residual-only examples can hide the defect. The dynamic conditional exposes it because its static then-branch changes from five to two. The stdout oracle therefore rejects the mutant. A second mutant removes the retained loop definition from the structured residual program. It still checks, but the computed closure line becomes computed open; this mutation distinguishes graph closure from a literal success string.

Acceptance test. Apply the four-command procedure in subappendix E.6. Require one passing inline test, the exact accepted transcript, and an empty audit. Replay both recorded mutations, require the stdout test to fail on the dynamic-conditional and computed-closure lines respectively, restore the accepted source, and rerun all four commands.

The historical self-application checks are separate native paths. First run scheme0-self-application.sh with Gambit Scheme. It loads the unchanged Chapter 5 source, annotates the distributed power program and specializer, specializes the specializer to each, installs the resulting compiler-generator, and requires the regenerated power generator and compiler-generator to be structurally equal to their originals. This is the direct Scheme0 witness required by the chapter.

Then run native-self-application.sh with SWI-Prolog. This second script specializes the archived flow-chart mix.fc with mixmix.in, executes the distributed cogen.fc with self.in, and executes the regenerated compiler-generator on the same input. Acceptance requires a nonempty first result and byte-for-byte equality between the latter two generated programs. Keep both native oracles separate from the Kappa stdout oracle: the native runs check acquired historical transformers, whereas the Kappa run checks the book’s bounded numeric specializer. Run agda MixCore.agda after both executable paths. Inspect mix-sound: the companion’s Spec type pairs each residual with its evaluation equation. Its specializer folds literal arithmetic, specializes both branches of a dynamic zero test, and constructs the equation compositionally. The file deliberately stops before calls, memoization, fuel control, and self-application.

Mathematical boundary. The finite corpus illustrates the static operator case of theorem 127.4 and the residual-call case of theorem 127.9; it does not prove either theorem. Its observer records finite returns only. It supplies no divergence preservation, binding-time analysis, or Futamura projection. The separate Scheme0 and flow-chart fixed-point replays supply implementation evidence for historical self-application; they do not prove those semantic equations.