ch:partial-evaluation: ch:partial-evaluation

Rule PE-Dynamic gives $x ⇓ res (x)$ . Rule PE-Op-S gives $2 + 3 ⇓ known (5)$ . The derivations $y ⇓ res (y)$ and $1 ⇓ known (1)$ , followed by PE-Op-D, give $y \cdot 1 ⇓ res (y \cdot 1)$ . Therefore PE-If-D returns $r = if 0 x then 5 else y \cdot 1.$ At $(x, y) = (0, 7)$ , source and residual select the first branch and return $5$ . At $(1, 7)$ , both select the second branch and return $7$ . These are the two branch instances of theorem 127.4.

At budget zero, PE-Fuel emits $g (0; x)$ . At budget one, the new pattern $(g, 0)$ is allocated and unfolded once; its body reaches $(g, 1)$ at exhausted budget and emits $g (1; x)$ . At budget two, the patterns $(g, 0)$ and $(g, 1)$ are allocated, and the frontier emits $g (2; x)$ . The retained equations therefore describe $g_{0} (x) = g_{1} (x), g_{1} (x) = g (2; x)$ up to the number of allocated residual names. The source has no finite evaluation derivation returning a numeral. Replacing the frontier call by zero gives the mutated residual program a finite derivation returning zero. At $n = 0$ , the two sides of the finite-return equivalence in theorem 127.9 are therefore false and true, respectively. This is a counterexample to the theorem’s stated finite-return conclusion for the mutation; it does not invoke a divergence-preservation theorem.

The only rule for a static conditional is BT-If-S, whose first premise would be $τ ⊢ x : S$ . But BT-Var gives $τ ⊢ x : D$ , so the derivation fails at that premise. The least well-annotated repair changes the conditional annotation and inserts the two forced embeddings: ${if}_{d} (x, lift (0), lift (1)) .$ Rule BT-Lift gives all three premises binding time $D$ , and Off-Lift followed by Off-If-D gives $P^{b}; (\emptyset; [x \mapsto x]) ⊢_{off} {if}_{d} (x, lift (0), lift (1)) ⇓ code (if x quote (0) quote (1)) .$

The monovariant division assigns $power (D, D) : D$ , so even a call at exponent four residualizes the test, decrement, recursive call, and multiplication. Splitting gives ${power}_{d} (D, D) : D$ and ${power}_{s} (S; D) : D$ . The known-exponent call selects the second copy; its recursive static argument decreases through $4, 3, 2, 1, 0$ , and specialization returns $x \cdot (x \cdot (x \cdot (x \cdot 1))) .$ Both copied definitions erase to the original two equations for power. By induction on $k$ , the zero calls all return $1$ , and the successor calls all return $x$ times the equal recursive result. Thus replacing a call by the copy selected at its call site preserves every erased call.

Use quoted lists as the exact Scheme0 data representation: $\begin{aligned} ⌜ Num (n) ⌝ & = (num, n), \\ ⌜ Var (x) ⌝ & = (var, x), \\ ⌜ Add (q_{1}, q_{2}) ⌝ & = (add, ⌜ q_{1} ⌝, ⌜ q_{2} ⌝) . \end{aligned}$ The tags and variable names are quoted symbols; the tuples are quoted-list values built with $cons$ . In Scheme0 notation, the interpreter definition is the first-order equation $\begin{aligned} {int}_{+} (q, d) = if & (car (q) = quote (num)) car (cdr (q)) \\ else if & (car (q) = quote (var)) lookup (car (cdr (q)), d) \\ else & {int}_{+} (car (cdr (q)), d) + {int}_{+} (car (cdr (cdr (q))), d), \end{aligned}$ The environment is a quoted list of pairs. Its Scheme0 lookup definition is $lookup (x, d) = if (x = car (car (d)), car (cdr (car (d))), lookup (x, cdr (d))) .$ The represented program is evaluated only under environments containing each of its free variable names, so the undefined empty-list primitive case is not reached. The final interpreter branch is reached only for the $add$ tag, because the represented language has exactly the three forms listed in the exercise. Represent the object program by $q = Add (Add (Var (x), Num (2)), Num (3)) .$ The interpreter ${int}_{+}$ dispatches on $Num$ , $Var$ , and $Add$ , recursively interpreting the two children of an addition. Assume at this point that the call $mix ({int}_{+}^{a}, ⌜ q ⌝)$ terminates and returns $r$ . The mix equation then gives, for every input environment $d$ , $eval (r, d) = v ⟺ eval (q, d) = v .$ The displayed interpreter has no reassociation rule, so specializing its three dispatches leaves exactly the residual arithmetic $(x + 2) + 3$ . The termination assumption is used exactly to obtain the returned residual program $r$ ; the implication in (127.2) has no conclusion when mix does not return.

Let $| - |$ count syntax nodes. Residualizing the dynamic test duplicates its two branches, so $| E_{n + 1} | = 2 | E_{n} | + 2$ , with $| E_{0} | = 1$ . Hence $| E_{n} | = 3 \cdot 2^{n} - 2$ . Instead bind the residual for $E_{n}$ once: $let z_{n} = E_{n} in if 0 y_{n} then z_{n} else z_{n}$ . Each level adds one test, one let, and two variable edges to the dag, so its number of distinct nodes is linear in $n$ . At every level the already constructed residual $E_{n}$ terminates under the exercise’s total arithmetic environment; proposition 127.11 therefore preserves each finite-return observation. Induction on $n$ composes these equivalences.

The polyvariant key produces distinct entries ${power}_{2} (x) = x \cdot (x \cdot 1)$ and ${power}_{3} (y) = y \cdot (y \cdot (y \cdot 1))$ , with the displayed association inherited from the source. A monovariant key $power$ cannot reuse one specialized equation for both static exponents without losing correctness; it must merge the exponent to a dynamic parameter and retain the test, decrement, and recursive call in the residual program $\begin{aligned} {power}_{m} (k, z) & = if 0 k then 1 else z \cdot {power}_{m} (k - 1, z), \\ main (x, y) & = ({power}_{m} (2, x), {power}_{m} (3, y)) . \end{aligned}$ The corresponding polyvariant main expression is $main (x, y) = ({power}_{2} (x), {power}_{3} (y)) .$ Thus the monovariant program loses the distinction between two and three but remains sound. In the polyvariant program, each new-call case unfolds the equation at its exact static tuple. The new-pattern and recursive-hit cases of theorem 127.9 therefore prove preservation of that residual program.

The monovariant policy is a different algorithm. For its direct proof, let $z$ be a natural and induct on the promoted exponent $k$ . At zero, both the source call and ${power}_{m} (0, z)$ select the first branch and return $1$ . At $k + 1$ , both select the second branch, multiply by $z$ , and make their respective call at $k$ ; the induction hypothesis identifies the returned recursive values. Hence ${power}_{m} (k, z)$ and $power (k, z)$ have the same finite return for every natural $k, z$ . Instantiating this result at $(2, x)$ and $(3, y)$ , then applying the pair constructor congruence, proves preservation of the displayed monovariant main expression. No case of theorem 127.9 is used for the promoted-parameter table.

Put $compiler = run (mix, [{mix}^{a}, {int}^{a}]) : Prog$ . Assuming this specialization terminates, (127.2) gives, for every represented $q$ , $run (compiler, ⌜ q ⌝) = run (mix, [{int}^{a}, ⌜ q ⌝]) = compile (q) : Prog .$ For the third projection, put $cogen = run (mix, [{mix}^{a}, {mix}^{a}]) : Prog$ . Assuming that self-specialization terminates, instantiate its dynamic input with ${int}^{a} : StaticTuple$ to obtain $run (cogen, {int}^{a}) = compiler : Prog .$ The inclusions $AnnProg \subseteq StaticTuple \subseteq Data$ type both displayed static tuples. No equation is asserted without the named termination assumption.