Partial Evaluation, Binding-Time Analysis, and the Futamura Projections

Prerequisites. Direct starred prerequisites: Chapter 17. No later core chapter depends on this route.

An interpreter for a fixed source program performs the same dispatch whenever its dynamic input changes. Evaluation cannot perform that dispatch before the input is known. A specializer must evaluate the source-determined work, emit the input-dependent work, and preserve divergence as well as returned values.

A residual term is the missing result

The shared source language is Jones–Gomard–Sestoft’s exact first-order Scheme0 card.

Fix natural numbers with total addition and multiplication. For a natural exponent $k$, define At $k=3$, the tests and decrements depend only on $3$. The three multiplications depend on $x$. Performing the former and retaining the latter gives $x\cdot (x\cdot (x\cdot 1))$.

There is a direct translation into Scheme0: translate $n$ to the numeral constant, $e_1+e_2$ and $e_1\cdot e_2$ to primitive applications, and $\mathsf{if}\mathsf{0}{e}_0\mathsf{then}{e}_1\mathsf{else}{e}_2$ to $\mathsf{if}(=e_{0}0)e_1{e}_2$. Thus this is a numeric projection of Scheme0, not a second presentation of its grammar. It omits quoted lists and calls until section 127.2; the historical self-applicability theorem is never inferred from this smaller definition.

Let ${\rho }_s$ contain the variables known during specialization. The judgment ${\rho }_s{⊢}_{\mathsf{pe}}e\Downarrow q$ is generated by these rules.

${\rho }_s{⊢}_{\mathsf{pe}}n\Downarrow \mathsf{known}(n)$

${\rho }_s(x)=n$

${\rho }_s{⊢}_{\mathsf{pe}}x\Downarrow \mathsf{known}(n)$

$x\notin \mathrm{dom}({\rho }_s)$

${\rho }_s{⊢}_{\mathsf{pe}}x\Downarrow \mathsf{res}(x)$

For $\odot \in \{+,\cdot \}$, arithmetic has two clauses.

${\rho }_s{⊢}_{\mathsf{pe}}{e}_1\Downarrow \mathsf{known}(n_1)$${\rho }_s{⊢}_{\mathsf{pe}}{e}_2\Downarrow \mathsf{known}(n_2)$

${\rho }_s{⊢}_{\mathsf{pe}}{e}_1\odot e_2\Downarrow \mathsf{known}(n_1\odot n_2)$

${\rho }_s{⊢}_{\mathsf{pe}}{e}_1\Downarrow q_1$${\rho }_s{⊢}_{\mathsf{pe}}{e}_2\Downarrow q_2$$(\mathrm{\exists }{r}_1.q_1=\mathsf{res}(r_1))\vee (\mathrm{\exists }{r}_2.q_2=\mathsf{res}(r_2))$

${\rho }_s{⊢}_{\mathsf{pe}}{e}_1\odot e_2\Downarrow \mathsf{res}(\mathsf{lift}(q_1)\odot \mathsf{lift}(q_2))$

${\rho }_s{⊢}_{\mathsf{pe}}{e}_0\Downarrow \mathsf{known}(0)$${\rho }_s{⊢}_{\mathsf{pe}}{e}_1\Downarrow q$

${\rho }_s{⊢}_{\mathsf{pe}}\mathsf{if}\mathsf{0}{e}_0\mathsf{then}{e}_1\mathsf{else}{e}_2\Downarrow q$

${\rho }_s{⊢}_{\mathsf{pe}}{e}_0\Downarrow \mathsf{known}(n+1)$${\rho }_s{⊢}_{\mathsf{pe}}{e}_2\Downarrow q$

${\rho }_s{⊢}_{\mathsf{pe}}\mathsf{if}\mathsf{0}{e}_0\mathsf{then}{e}_1\mathsf{else}{e}_2\Downarrow q$

${\rho }_s{⊢}_{\mathsf{pe}}{e}_0\Downarrow \mathsf{res}(r_0)$${\rho }_s{⊢}_{\mathsf{pe}}{e}_1\Downarrow q_1$${\rho }_s{⊢}_{\mathsf{pe}}{e}_2\Downarrow q_2$

${\rho }_s{⊢}_{\mathsf{pe}}\mathsf{if}\mathsf{0}{e}_0\mathsf{then}{e}_1\mathsf{else}{e}_2\Downarrow \mathsf{res}(\mathsf{if}\mathsf{0}{r}_0\mathsf{then}\mathsf{lift}(q_1)\mathsf{else}\mathsf{lift}(q_2))$

On $\mathsf{if}\mathsf{0}x\mathsf{then}0\mathsf{else}1$, choosing either branch changes the answer for one of $x=0$ and $x=1$. Rule PE-If-D must retain both branches.

Proof of Lemma 127.3 — Residual variables

Proof. Induct on the specialization derivation. Rules PE-Num and PE-Static leave no variable. Rule PE-Dynamic retains its one variable, whose side condition puts it outside the static domain. Each operator conclusion takes the union of the free variables in its premises. The two known-test rules retain only the selected branch. Rule PE-If-D takes the union of the test and both branches. These are all rules. ◻

Proof of Theorem 127.4 — Online specialization equation

Proof. Induct on the specialization derivation. The numeral and variable cases follow by lookup. In PE-Op-S, both operands evaluate to the recorded numerals. In PE-Op-D, apply the two induction hypotheses in left-to-right order and rebuild the operator evaluation.

For PE-If-Z, the test induction hypothesis gives zero in the combined environment. Both evaluations enter the first branch, where the branch induction hypothesis gives the equivalence. Rule PE-If-N uses the second branch and the recorded nonzero value. In PE-If-D, the residual test and source test have the same value by the induction hypothesis. They select the same branch, whose induction hypothesis gives the result. ◻

Recursion forces memoization and a budget

For the recursion argument, extend definition 127.2 with calls. A numeric call program is a finite list of equations $f({\overrightarrow{x}}_s;{\overrightarrow{x}}_d)=e_f$, separating static and dynamic parameters. Its source evaluation extends $\mathsf{eval}$ with

$P;\rho ⊢{\overrightarrow{e}}_s\Downarrow \overrightarrow{n}$$P;\rho ⊢{\overrightarrow{e}}_d\Downarrow \overrightarrow{v}$$P(f)=({\overrightarrow{x}}_s;{\overrightarrow{x}}_d;e_f)$$P;[{\overrightarrow{x}}_s\mapsto \overrightarrow{n},{\overrightarrow{x}}_d\mapsto \overrightarrow{v}]⊢e_f\Downarrow v$

$P;\rho ⊢\mathsf{call}f({\overrightarrow{e}}_s;{\overrightarrow{e}}_d)\Downarrow v$

The numeral, variable, operation, and conditional rules are the big-step counterparts of $\mathsf{eval}$ in definition 127.2; vector evaluation is left to right. This card translates into Scheme0 by merging the two formal-parameter lists and applying the translation above. A static call pattern is a pair $(f,\overrightarrow{n})$. A memo table maps such a pattern to one residual function name and, after the recursive call returns, its equation. Revisiting a pattern emits a call to that name; encountering a new pattern first allocates a fresh name and then specializes its body. Different static tuples are distinct patterns, so this policy is polyvariant.

The call $g(n;x)=g(n+1;x)$ generates the infinite pattern sequence $(g,0),(g,1),\dots$. Memoization alone does not terminate.

The two entry states are not merely an implementation detail. A proof that uses a recursive hit must relate the hit to the equation that will exist after the allocating call finishes.

Proof of Lemma 127.7 — Memo completion and finite simulation

Proof. Use strong induction on $k$, simultaneously for every table entry and for the expression at every specialization subderivation. Inside the height induction, induct on that fixed specialization derivation. Numerals, variables, primitives, and conditionals use the corresponding argument or selected-branch induction hypotheses.

For PE-Call-Hit, memo-table lookup fixes the name in the conclusion. If its entry is pending, condition 1 identifies the unique enclosing allocator and the equation that the final table supplies; if it is completed, that equation belongs to the completed entry and condition 2 applies. In either case, inversion of a finite N-Call derivation exposes an evaluation of the equation body whose height is strictly below the height of the call. Apply the outer induction hypothesis to that body and rebuild the call on the other side. This argument works in both directions and is the step that justifies a recursive back edge.

For PE-Call-New, allocation preserves all older names, the body premise supplies the new equation, and completion changes only the state of that entry. Apply the inner induction hypotheses to the argument derivations and the outer induction hypothesis to each strictly shorter finite body evaluation. Table extensions are harmless by the same evaluation-derivation argument later recorded as residual-program monotonicity: allocation uses fresh names, completion preserves old equations, and retained closure only grows. For PE-Fuel, both sides invoke the same retained source equation; condition 3 supplies every later callee. These are the three call rules. Freshness gives unique names, $\mathsf{complete}$ gives one final equation per allocation, and the construction of $F_{\mathrm{\infty }}$ gives condition 3. Hence the simultaneous claims hold at $k+1$, and induction establishes them for every $k$. ◻

Proof of Lemma 127.8 — Residual-program monotonicity

Proof. Induct on the finite evaluation derivation. Numeral, variable, operator, and conditional rules do not inspect the program. In the call case, the equation used by the premise is either a completed residual equation or a retained source equation. Extension preserves completed entries, uses globally fresh names for new entries, and only enlarges the call-reachable retained set. Therefore $P_{{\mu }_2}$ retains the equation used by the premise; apply the induction hypotheses to the argument and body derivations and rebuild N-Call. ◻

Proof of Theorem 127.9 — Safe-fuel search termination and preservation

Proof. Implement proof search by the ordered, pairwise-disjoint rule alternatives. Order its recursive calls lexicographically by budget and expression size. A syntax-directed rule searches strict subexpressions. Unfolding a new call pattern decreases the budget. A repeated pattern and PE-Fuel emit syntax and make no recursive call on a function body. The order is well founded, so search returns either the unique derivation selected by the rules or a finite static-failure result. This first conclusion does not assert that every input has a derivation.

For preservation, the successful search from the empty table has a final completed table: every allocation is completed while its enclosing PE-Call-New returns. Apply lemma 127.7 at a height strictly larger than the finite evaluation derivation in the implication under consideration. The lemma’s expression clause gives that implication, and applying it from the other side gives the converse. Quantifying over all finite heights proves the displayed equivalence. This argument does not turn absence of a finite derivation into a divergence theorem. ◻

Fuel controls transformation time, not residual size. A dynamic conditional can duplicate a large continuation. For size control, extend residual syntax with $\mathsf{let}z=r\mathsf{in}{r}^{\prime }$ and the single source rule

$P;\rho ⊢r\Downarrow v$$P;\rho [z\mapsto v]⊢r^{\prime }\Downarrow n$

$P;\rho ⊢\mathsf{let}z=r\mathsf{in}{r}^{\prime }\Downarrow n$

Proof of Lemma 127.10 — Evaluation decomposition for substitution

Proof. Induct structurally on $r^{\prime }$, with a subsidiary induction on the displayed finite evaluation derivation for each direction. At the variable $z$, the left side is the assumed derivation of $r$, while the right side is lookup of $v$. A different variable uses the same lookup on both sides. Primitive and conditional cases apply the induction hypotheses in evaluation order; determinism of $P;\rho ⊢r\Downarrow v$ ensures that multiple substituted occurrences yield the same $v$. In a call, apply the induction hypotheses to every actual argument, then use the identical source equation and environment for the body. Alpha-renaming handles a binder in an extended residual language. These are every expression constructor, so both implications follow. This reverse implication is an anti-substitution lemma; it is not obtained by reading the ordinary substitution lemma backward. ◻

Proof of Proposition 127.11 — Let-insertion preservation

Proof. Invert or introduce N-Let, then apply lemma 127.10 in the required direction. The termination hypothesis is necessary under call by value: when $z\notin \mathrm{fv}(r^{\prime })$, insertion evaluates $r$ even though substitution does not. ◻

This preservation theorem does not bound the number of distinct static call patterns.

Offline annotations and the three projections

The second card is the two-level Scheme0 syntax of Jones–Gomard–Sestoft. For $b\in \{S,D\}$, a division $\tau$ maps variables to binding times. The annotated constructs are The two argument lists at a call are the callee’s static and dynamic parameters. The subscript on a call instead selects unfolding $(s)$ or residualization $(d)$; these are different decisions. The exact checking rules are:

$\tau ⊢c:S$

$\tau (x)=b$

$\tau ⊢x:b$

$\tau ⊢e_i:S(1\le i\le a)$

$\tau ⊢{\mathsf{op}}_s(e_1,\dots ,e_a):S$

$\tau ⊢e_i:D(1\le i\le a)$

$\tau ⊢{\mathsf{op}}_d(e_1,\dots ,e_a):D$

$\tau ⊢e_0:S$$\tau ⊢e_1:b$$\tau ⊢e_2:b$

$\tau ⊢{\mathsf{if}}_s(e_0,e_1,e_2):b$

$\tau ⊢e_0:D$$\tau ⊢e_1:D$$\tau ⊢e_2:D$

$\tau ⊢{\mathsf{if}}_d(e_0,e_1,e_2):D$

$\tau ⊢e_i:S(1\le i\le a)$

$\tau ⊢{\mathsf{call}}_{s}f(e_1,\dots ,e_a)():S$

When , both call forms with dynamic arguments have binding time $D$:

$\tau ⊢e_i:S(1\le i\le m)$

$\tau ⊢{\mathsf{call}}_{s}f(e_1,\dots ,e_m)(e_{m+1},\dots ,e_a):D$

$\tau ⊢e_i:S(1\le i\le m)$

$\tau ⊢{\mathsf{call}}_{d}f(e_1,\dots ,e_m)(e_{m+1},\dots ,e_a):D$

$\tau ⊢e:S$

$\tau ⊢\mathsf{lift}(e):D$

For $\mathsf{define}(f(x_1,\dots ,x_m)(x_{m+1},\dots ,x_a))e$, checking uses ${\tau }_f(x_i)=S$ for $i\le m$ and $D$ otherwise; its body must have binding time $S$ when $m=a$, and $D$ when . These are exactly the rule families of the source card [JGS93].

The check becomes operational only after its two representations are fixed. Write $q::=\mathsf{val}(v)\mid \mathsf{code}(r)$, with $\lfloor \mathsf{val}(v)\rfloor =v$ and $\lfloor \mathsf{code}(r)\rfloor =r$. A specialization environment $\xi =({\rho }_s;{\eta }_d)$ maps static variables to source values and dynamic variables to residual expressions. The judgment $P^b;\xi {⊢}_{\mathsf{off}}{e}^b\Downarrow q$ is the least relation generated by the following rules. The vector forms apply the scalar rules left to right.

$P^b;\xi {⊢}_{\mathsf{off}}c\Downarrow \mathsf{val}([[c]])$

${\rho }_s(x)=v$

$P^b;\xi {⊢}_{\mathsf{off}}x\Downarrow \mathsf{val}(v)$

${\eta }_d(x)=r$

$P^b;\xi {⊢}_{\mathsf{off}}x\Downarrow \mathsf{code}(r)$

$P^b;\xi {⊢}_{\mathsf{off}}\overrightarrow{e}\Downarrow \mathsf{val}(\overrightarrow{v})$$\delta (\mathsf{op},\overrightarrow{v})=v$

$P^b;\xi {⊢}_{\mathsf{off}}{\mathsf{op}}_s(\overrightarrow{e})\Downarrow \mathsf{val}(v)$

$P^b;\xi {⊢}_{\mathsf{off}}\overrightarrow{e}\Downarrow \mathsf{code}(\overrightarrow{r})$

$P^b;\xi {⊢}_{\mathsf{off}}{\mathsf{op}}_d(\overrightarrow{e})\Downarrow \mathsf{code}(\mathsf{op}(\overrightarrow{r}))$

$P^b;\xi {⊢}_{\mathsf{off}}{e}_0\Downarrow \mathsf{val}(v_0)$$j=1\text{ if }{v}_0\ne \mathsf{false},j=2\text{ otherwise}$$P^b;\xi {⊢}_{\mathsf{off}}{e}_j\Downarrow q$

$P^b;\xi {⊢}_{\mathsf{off}}{\mathsf{if}}_s(e_0,e_1,e_2)\Downarrow q$

$P^b;\xi {⊢}_{\mathsf{off}}{e}_i\Downarrow \mathsf{code}(r_i)(0\le i\le 2)$

$P^b;\xi {⊢}_{\mathsf{off}}{\mathsf{if}}_d(e_0,e_1,e_2)\Downarrow \mathsf{code}(\mathsf{if}{r}_0{r}_1{r}_2)$

If $P^b(f)=({\overrightarrow{x}}_s;{\overrightarrow{x}}_d;e_f^b)$, unfolding and residual calls are separate rules:

$P^b;\xi {⊢}_{\mathsf{off}}{\overrightarrow{e}}_s\Downarrow \mathsf{val}(\overrightarrow{v})$$P^b;\xi {⊢}_{\mathsf{off}}{\overrightarrow{e}}_d\Downarrow \mathsf{code}(\overrightarrow{r})$$P^b;([{\overrightarrow{x}}_s\mapsto \overrightarrow{v}];[{\overrightarrow{x}}_d\mapsto \overrightarrow{r}]){⊢}_{\mathsf{off}}{e}_f^b\Downarrow q$

$P^b;\xi {⊢}_{\mathsf{off}}{\mathsf{call}}_{s}f({\overrightarrow{e}}_s)({\overrightarrow{e}}_d)\Downarrow q$

$P^b;\xi {⊢}_{\mathsf{off}}{\overrightarrow{e}}_s\Downarrow \mathsf{val}(\overrightarrow{v})$$P^b;\xi {⊢}_{\mathsf{off}}{\overrightarrow{e}}_d\Downarrow \mathsf{code}(\overrightarrow{r})$

$P^b;\xi {⊢}_{\mathsf{off}}{\mathsf{call}}_{d}f({\overrightarrow{e}}_s)({\overrightarrow{e}}_d)\Downarrow \mathsf{code}(\mathsf{call}{f}_{\overrightarrow{v}}(\overrightarrow{r}))$

$P^b;\xi {⊢}_{\mathsf{off}}e\Downarrow \mathsf{val}(v)$

$P^b;\xi {⊢}_{\mathsf{off}}\mathsf{lift}(e)\Downarrow \mathsf{code}(\mathsf{quote}(v))$

Rule Off-Call-D names the residual state reached at the displayed static tuple. The rules determine residual expressions; the following graph card determines the residual program used by the soundness theorem.

Constraint generation erases the subscripts, assigns an unknown in $\{S,D\}$ to every occurrence and formal parameter, and reads the premises of the displayed rules as equations. For example, a static operator generates $b_i=S$; a dynamic conditional generates $b_0=b_1=b_2=D$; and a call equates each argument with the corresponding formal division. A boundary is repaired only by inserting $\mathsf{lift}$. Starting with every unknown at $S$, repeatedly changing a violated unknown to $D$ computes the least solution because every generated constraint is monotone on the two-point lattice.

Proof of Lemma 127.13 — Binding-time consistency

Proof. Induct on the finite offline-specialization derivation, and invert the matching final binding-time rule. This choice is essential in Off-Call-S: its body specialization is a strict subderivation, whereas the callee’s binding-time derivation lives under the different division ${\tau }_f$. The program check supplies that matching derivation under ${\tau }_f$.

Rules Off-Const and Off-Var-S/D match BT-Const and BT-Var. The induction hypotheses give source values to Off-Op-S and Off-If-S, and residual syntax to Off-Op-D and Off-If-D. Each call rule’s matching binding-time rule checks its argument lists against the callee division. In Off-Call-S, apply the induction hypothesis to the body subderivation using the program check for $e_f^b$. Rule Off-Call-D constructs residual syntax. Rule Off-Lift changes the source value supplied by its induction hypothesis into quoted residual syntax. These are all offline rule families. ◻

Proof of Lemma 127.14 — Completed-graph node simulation

Proof. For $k\in \mathbb{N}$, prove both implications simultaneously for every graph node and the main expression when the given finite evaluation derivation has height below $k$. Use strong induction on $k$, followed by induction on the fixed offline-specialization derivation supplied by definition 127.12. Constants, variables, operators, lifts, and both conditional forms use strict argument or selected-branch subderivations.

For an unfolded static call, inversion of source evaluation exposes the callee-body derivation strictly below the enclosing call; apply the outer height induction and rebuild the residual evaluation. For a residual dynamic call, graph closure supplies the unique target node and its equation. In the source-to-residual direction, inversion of the source call again exposes a strictly shorter body derivation, to which the outer induction applies. In the residual-to-source direction, inversion of the residual named call exposes the equation-body derivation strictly below that call; apply the same outer induction in the opposite direction and rebuild the source call. Crucially, a back edge is handled by smaller evaluation height, not by an induction hypothesis on the graph node or on its specialization body. These are both call forms and every offline rule family. Induction on $k$ removes the bound. ◻

Proof of Theorem 127.15 — Well-annotated-program soundness

Proof. Apply lemma 127.14 to the main-expression clause of the completed graph. The definition of ${\mathsf{run}}_0$ supplies the displayed static and dynamic environments on the source side and the dynamic environment on the residual side. The two implications of the lemma give the equivalence for each returned value. The proof therefore depends on the completed, reachability-closed graph, rather than treating a back-edge body as a structural subderivation. ◻

Monovariance can force a useless division. Fix the actual Scheme0 definition $$\mathsf{define}(\mathsf{power}kx)\mathsf{if}(=k0)1(\ast x(\mathsf{call}\mathsf{power}(-k1)x)).$$ The primitive $(-k1)$ is defined on positive naturals; the conditional prevents its use at zero. Suppose one call has dynamic exponent and another has known exponent four. A single monovariant division marks $k$ dynamic at both sites.

Here is the finite copying transformation used to repair that division. Let $P$ be a finite Scheme0 program containing (127.1) and no definitions named ${\mathsf{power}}_d$ or ${\mathsf{power}}_s$. A power-site map $\chi$ assigns $d$ or $s$ to every nonrecursive syntactic call site of $\mathsf{power}$ in $P$. The program ${\mathsf{Split}}_{\chi }(P)$ deletes the original definition, inserts two alpha-distinct copies ${\mathsf{power}}_d$ and ${\mathsf{power}}_s$, redirects the recursive call in each copy to that copy, and redirects every other call site $\ell$ to ${\mathsf{power}}_{\chi (\ell )}$. Every other syntax node and definition is copied homomorphically. The collapse map $\lfloor -{\rfloor }_{\mathsf{split}}$ renames either copy back to $\mathsf{power}$ and identifies their duplicate definitions. Therefore $\lfloor {\mathsf{Split}}_{\chi }(P){\rfloor }_{\mathsf{split}}=P$, including bodies and call sites.

For offline specialization, the two copies receive different annotated definitions. Writing the static arguments before the semicolon, their bodies are The displayed lifts make every dynamic primitive operand dynamic. Both annotated definitions erase to their Scheme0 copies. A site may be assigned $s$ only after its exponent premise checks at binding time $S$; all remaining sites use $d$, inserting a lift when a known actual flows to a dynamic formal. Thus the transformation and its admissible call-site annotations are separate, explicit data.

Proof of Proposition 127.16 — Binding-time split preservation

Proof. Prove the two implications simultaneously by induction on the finite evaluation derivation from the side supplying the implication. Constants, variables, primitives, and conditionals rebuild the same rule because ${\mathsf{split}}_{\chi }$ is homomorphic there. A call to any function other than $\mathsf{power}$ uses the induction hypotheses for its argument and body derivations. At an external power call, the selected copy has the same formals and collapsed body as (127.1); apply the induction hypotheses to the arguments and then to the strictly smaller body derivation. At a recursive power call, the copy calls itself, while collapse calls $\mathsf{power}$; the recursive body derivation is again strictly smaller. These are all call cases. The reverse induction collapses either copied name to $\mathsf{power}$, so it has the same cases and establishes the converse.

For specialization, Off-If-S evaluates the equality tests at $4,3,2,1,0$. At each positive exponent, Off-Op-S computes the decrement and Off-Call-S unfolds the next state. At zero, Off-Lift emits $1$. The four enclosing Off-Op-D instances retain multiplication by the residual variable $x$, giving the displayed term. ◻

The same pair separates online state from an offline monovariant division. For $$f(k;x)=\mathsf{if}\mathsf{0}k\mathsf{then}x\mathsf{else}(x+1),$$ consider one call $f(k;x)$ with unknown $k$ and one call $f(0;x)$. Monovariance joins the first call into the formal division and marks $k$ dynamic, so the offline specializer residualizes the conditional at both call sites. The online specializer sees the second actual value $0$ and returns only $x$. Function splitting recovers that result offline by assigning the second call its own all-static copy. Thus online is more precise on this fixed program and division; the calculation is not a system-independent ordering.

For the first projection, fix the represented arithmetic language $$q::=\mathsf{Lit}(n)\mid \mathsf{Input}\mid \mathsf{Add}(q,q)$$ and the Scheme0 equations These equations use the card’s constructor tests, selectors, calls, and base addition. Specializing with respect to $\mathsf{Add}(\mathsf{Lit}(2),\mathsf{Input})$ unfolds the first and third equations and yields $d\mapsto 2+d$. Hence the first-projection instance is $$\mathsf{eval}(\mathsf{mix}({\mathsf{intExp}}^a,⌜\mathsf{Add}(\mathsf{Lit}(2),\mathsf{Input})⌝),d)=2+d.$$ The general compiler equation below is the same calculation with $q$ arbitrary.

Let $⌜p⌝$ be the Scheme0 representation of $p$, and let $p^a=\mathsf{ann}(p,{\delta }_p)$ be its two-level annotation under checked division ${\delta }_p$. Thus $p^a$ contains the division information rather than hiding it as an implicit argument. Fix the historical self-applicable offline program $\mathsf{mix}$ with full Scheme0 interface $$\mathsf{mix}:\mathsf{AnnProg}\times \mathsf{StaticTuple}\rightharpoonup \mathsf{Prog}$$ and equation $$\mathsf{mix}(p^a,s)=r⟹\mathsf{eval}(r,d)=v⟺\mathsf{eval}(|p^a|,(s,d))=v.$$ The annotation $p^a$, suppressed in informal projection slogans, is part of the executable interface. The equation is not asserted for definition 127.5.

Proof of Proposition 127.17 — Scheme0 self-application typing boundary

Proof. The checked annotations satisfy ${\mathsf{mix}}^a,{\mathsf{power}}^a\in \mathsf{AnnProg}$, and the Scheme0 representation satisfies $\mathsf{AnnProg}\subseteq \mathsf{StaticTuple}$. Therefore each displayed pair lies in $\mathsf{AnnProg}\times \mathsf{StaticTuple}$, the domain sort of $\mathsf{mix}$. Its codomain is $\mathsf{Prog}$, so any returned value has that sort. Partiality of the signature prevents a termination conclusion. The cited construction supplies the annotation shapes but no general termination theorem for self-application . ◻

The following meta-sort ledger types every self-application. Let $\mathsf{Prog}\subseteq \mathsf{StaticTuple}\subseteq \mathsf{Data}$ be the represented Scheme0 programs, $\mathsf{AnnProg}\subseteq \mathsf{StaticTuple}\subseteq \mathsf{Data}$ their checked annotations, $\mathsf{run}:\mathsf{Prog}\times \mathsf{Data}\rightharpoonup \mathsf{Data}$, and let $\mathsf{int},\mathsf{mix}\in \mathsf{Prog}$. The interpreter accepts $[⌜q⌝,d]:\mathsf{Data}$, and the annotation encodings ${\mathsf{int}}^a$ and ${\mathsf{mix}}^a$ are members of $\mathsf{StaticTuple}$. The specializer accepts $[p^a,s]:\mathsf{Data}$ with $p^a:\mathsf{AnnProg}$ and returns $r:\mathsf{Prog}$. Hence, if the following three applications return, their outputs have the displayed meta-sorts; the equations introduce names for those returned programs rather than asserting termination: The displayed inclusions into $\mathsf{StaticTuple}$ and $\mathsf{Data}$, realized by Scheme0’s quoted program and annotation representations, license the two self-applications when they terminate. The typing proposition above discharges none of the three termination antecedents. An arbitrary typed specializer need not have such a reflexive representation.

Proof of Theorem 127.18 — The three Futamura equations

Proof. Instantiate (127.2) with $p^a={\mathsf{int}}^a$ and $s=⌜q⌝$. The interpreter equation proves the first line. For the second, use $p^a={\mathsf{mix}}^a$, $s={\mathsf{int}}^a$, and dynamic input $⌜q⌝$. The right side is $\mathsf{compile}(q)$. For the third, use $p^a={\mathsf{mix}}^a$, $s={\mathsf{mix}}^a$, and dynamic input ${\mathsf{int}}^a$. The right side is $\mathsf{compiler}$. The stated termination hypotheses license precisely these applications. ◻

A typed self-interpreter does not discharge those hypotheses. In the $F_{\omega }$ card of chapter 17, an evaluator at object type $A$ has shape ${\mathsf{eval}}_A:\mathsf{Rep}(A)\to A$. Its own syntax has type $\mathsf{Rep}(\mathsf{Rep}(A)\to A)$, not $\mathsf{Rep}(A)$; the attempted application ${\mathsf{eval}}_A⌜{\mathsf{eval}}_A⌝$ therefore fails at the argument type. Scheme0’s untyped program-as-data inclusion avoids that particular mismatch, but self-applying $\mathsf{mix}$ still requires the binding-time and termination facts in (127.2).

The binding-time analysis has a local abstract-interpretation map. Take the two-point lattice $S\le D$; map a concrete partial environment to $S$ at exactly its known variables and to $D$ elsewhere. Constants transfer to $S$, variables by lookup, base applications by join, a dynamic test forces the result and both branches to $D$, and calls join actual annotations into the callee’s formal division.

Proof of Lemma 127.19 — Finite binding-time analysis

Proof. Each transfer clause is a projection, constant, or finite join in $S\le D$, hence monotone. The product lattice has finite height at most the number of program variables; every strict iteration changes at least one coordinate from $S$ to $D$, so iteration terminates. At the post-fixed point, induct on expression syntax. The variable case is lookup; an operation can remain static only when every operand does; the conditional and call cases use their displayed propagation constraints. ◻

This is an explicit instance of the vocabulary in chapter 25. It does not import that chapter’s flow-sensitive domains, widening theorem, or verified analyzer: the lattice, transfer, and termination argument above are the entire connection.

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 127.5, then complete exercise 127.6.

Exercise 127.4¶

★★☆ Give the useless monovariant annotation of power in which both arguments are dynamic. Perform the function split above, solve both divisions, and calculate the residual program at exponent four. Prove equality of the erased calls by unfolding the two copied equations.

Referenced from 3 locations

• Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
• ch:partial-evaluation: ch:partial-evaluation

Exercise 127.5¶

★★★ Let ${\mathsf{int}}_{+}$ interpret numerals, variables, and addition. Supply its encoding and use (127.2) to derive the first projection for $(x+2)+3$. State the termination assumption where it is used.

Referenced from 4 locations

• Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
• ch:partial-evaluation: ch:partial-evaluation

Exercise 127.6¶

★★★ Practical project.scheme0-fuelled-specializer Implement in Kappa the expression core, dynamic conditional, recursive call patterns, memo hits, and safe fuel exhaustion. Maintain lemma 127.3. Print A mutation that returns the left operand of static addition must fail the dynamic-conditional test. The Kappa program does not prove self-applicability or a Futamura equation.

Referenced from 5 locations

• Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
• Specialization and staging: executable records
• ch:partial-evaluation: fuelled numeric specialization

Exercise 127.7¶

★★☆ For $E_0=x$ and $E_{n+1}=\mathsf{if}\mathsf{0}{y}_n\mathsf{then}{E}_n\mathsf{else}{E}_n$, calculate the tree size of the residual term produced without let insertion. Then insert one fresh let at each level and prove the resulting dag has linear size using proposition 127.11 under its termination hypothesis.

Referenced from 3 locations

• Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
• ch:partial-evaluation: ch:partial-evaluation

Exercise 127.8¶

★★☆ Compare the polyvariant key $(f,\overrightarrow{n})$ with the following monovariant policy on calls $\mathsf{power}(2;x)$ and $\mathsf{power}(3;y)$. The monovariant table has key $f$; when distinct static tuples collide, it promotes every differing static component to a dynamic formal, emits one copy of the erased source equation with that promoted formal, and redirects every colliding call to the copy. Write both residual programs and state which static distinction is lost. Prove preservation of the polyvariant program by the corresponding call cases of theorem 127.9. Prove preservation of the monovariant program directly by induction on the promoted exponent; it is not an instance of that theorem’s $(f,\overrightarrow{n})$-keyed algorithm.

Referenced from 3 locations

• Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
• ch:partial-evaluation: ch:partial-evaluation

Exercise 127.9¶

★★★ Using (127.2), derive the second projection for an arbitrary $⌜q⌝$ and the third at ${\mathsf{int}}^a$. Type each meta-level application with the ledger above and state its termination premise.

Referenced from 3 locations

• Partial Evaluation, Binding-Time Analysis, and the Futamura Projections
• ch:partial-evaluation: ch:partial-evaluation