Supercompilation, Driving, and Generalization

Proof. Proceed by the last driving rule. In D-Beta, substitution is the call-by-value beta step. D-Case-Known selects the constructor’s unique branch. In D-Case-Open, exhaustiveness gives an outer constructor shape for $\sigma (y)$, and disjointness makes it unique; its fields define the unique compatible extension. Applying that extension to the refined child gives the uncontracted parent instance literally. A subsequent node uses D-Case-Known. These are the three rule families of ${\mathsf{drive}}_0$. No coverage claim is made for the full grammar; R1–R20 supply that separate driver. ◻

Proof. The residual equation for $Q$ abstracts precisely its free variables. Instantiation by $\pi$ alpha-renames that equation to the one required at $Q^{\prime }$. Unfolding the residual call exposes that instantiated body. Induction on a finite evaluation derivation then matches every source contraction with the corresponding contraction of the unfolded equation; alpha-renaming preserves the selected rule and substitution. Both closed instances therefore return the same value. Named residual calls are not counted by this local argument. ◻

Proof. Let $X$ be a set with a reflexive, transitive relation ${\le }_X$. The pair $(X,{\le }_X)$ is a well-quasi-order when every infinite sequence $x_0,x_1,\dots$ contains indices with $x_i{\le }_X{x}_j$. We import the following combinatorial theorem. If $(X,{\le }_X)$ is a well-quasi-order, then its finite rooted labelled trees are well-quasi-ordered by homeomorphic embedding, where coupling compares root labels by ${\le }_X$ and corresponding children, and diving compares a tree with a descendant. Kruskal’s proof of this statement occupies physical pages 5–15, printed pages 214–224 .

Let $L$ contain the configuration-root label, the finitely many term and context tags, one label for every member of $\mathrm{dom}(G)$, one numeral label, and one variable label. Equality makes the finite set $L$ a well-quasi-order: an infinite label sequence repeats a label by the infinite pigeonhole principle. Encode $Q$ as the ordered $L$-labelled tree described before the theorem. A structural induction on the imported tree-embedding derivation proves $$E(Q)\preccurlyeq E(Q^{\prime })⟹Q\preccurlyeq Q^{\prime }.$$ The coupling case is Emb-Couple; the descendant case is Emb-Dive; and the two collapsed leaf cases are Emb-Var and Emb-Num. Kruskal therefore supplies with $E(Q_i)\preccurlyeq E(Q_j)$, and the displayed implication supplies $Q_i\preccurlyeq Q_j$. An infinite process-tree branch is such a sequence, so its later member raises the whistle against the earlier member. No termination theorem for a program transformer is imported here.

The finite-label hypothesis cannot be removed. For pairwise distinct nullary labels ${\ell }_0,{\ell }_1,\dots$, the one-node trees ${\ell }_0,{\ell }_1,\dots$ form an infinite sequence with no embedded pair, because neither diving nor equal-root coupling applies. ◻

Proof. Induct on the ordinary node count of $s$ plus that of $t$, with the finite disagreement table threaded through the recursive calls. A table hit returns its stored variable without a recursive call. Suppose $s=c(s_1,\dots ,s_k)$ and $t=c(t_1,\dots ,t_k)$. For each integer $i$ with $1\le i\le k$, process the children from left to right. The induction hypothesis gives $\mathsf{msg}(s_i,t_i)=(g_i,{\sigma }_i,{\tau }_i)$ at the table produced by the preceding children. Threading makes ${\sigma }_i$ and ${\sigma }_j$, and likewise ${\tau }_i$ and ${\tau }_j$, agree on every shared domain variable. Hence the following unions are functions: $$g=c(g_1,\dots ,g_k),\sigma =\bigcup _{i=1}^k{\sigma }_i,\tau =\bigcup _{i=1}^k{\tau }_i.$$ Then $g\sigma =s$ and $g\tau =t$ by the induction equations for every child. If a common generalization has a variable at its root, map that variable to $g$. Otherwise its root must be $c$; it restricts to a common generalization at each child, so the induction factorizations combine through the same root. This treats every equal-head arity.

For unequal heads the chosen variable $z_{u,v}$ with two singleton substitutions has the required equations. Any common generalization must place a variable at that disagreement, so mapping it to $z_{u,v}$ defines $\delta$. Memoized disagreement pairs force the same choice at repeated positions and preserve the factorization. Equal heads recurse only on strict child pairs, and unequal heads or table hits stop; hence the node-count induction also proves termination.

It remains to prove the weight assertion. Every selected split has $t\preccurlyeq s$ and $s\text{⧸}\preccurlyeq t$: in A3 the first relation is its side condition and the second follows because the earlier A2 test failed; in A4a they are the two displayed side conditions. In the equal-head arm of $\mathsf{split}$, the generalization keeps the common root. Every range member of its first witness substitution is a proper subexpression of $s$. If every disagreement on the $s$-side were a weight-one split variable, then the corresponding $t$-side subterm would also be a variable: no composite tree embeds a variable leaf. Coupling the common nodes and applying Emb-Var at those disagreements would derive $s\preccurlyeq t$, contrary to strictness. Hence at least one disagreement replaces a weight-two atom or a composite subexpression by a weight-one split variable. Consequently both the generalization and every range member have weight strictly below $\mathsf{wt}(s)$.

In the unequal-head arm, $s=s_0(e_1,\dots ,e_k)$ is a selected application configuration and therefore has at least one immediate component. The configuration encoding exposes the selected global atom in one such component. The result $s_0(y_1,\dots ,y_k)$ replaces every immediate component by a weight-one split variable, while the component containing the global atom has weight at least two. Hence the result has smaller weight, and every $e_i$ is a proper subexpression of $s$. These are exactly the two split arms used by A3 and A4a. ◻

Proof. For reflexivity, reuse the given evaluation derivation with the same call count. For transitivity, compose the two existential evaluation witnesses; the inequalities compose by transitivity of $\le$, and the two directions of operational approximation compose separately.

For congruence, fix a closing observation context $H$. Replacing the selected holes turns $H⟨C[-]⟩$ into another closing context for the original pair. Apply the assumed improvement and both assumed termination implications to that composite context. This proves all three conjuncts of strong improvement. Repeating the one-hole argument proves the finite multi-hole form.

Renaming transports an evaluation derivation rule by rule. Binders are renamed before substitution, constructor and global tags are unchanged, and the named-call count is unchanged. Applying the inverse renaming transports the derivation back, which proves cost equivalence.

For a contraction $e{⟶}_{\mathsf{cbv}}{e}^{\prime }$, splice the contraction in front of any terminating derivation for the contractum. Conversely, invert the unique first step of a terminating derivation for the redex. The two derivations have equal named-call cost except at a global unfolding, where the redex derivation has one additional named call. Thus the contractum never uses more calls, and termination is equivalent. Multi-argument beta and the known-constructor case evaluate the same arguments from left to right and then reach the same simultaneous-substitution instance; induction on the argument vector gives the stated equations.

Finally expand $\mathsf{letrec}$. Because $h$ is absent from $e$, the outer beta substitution changes no occurrence of $e$. The administrative beta and fix contractions are not named calls, so the two evaluation derivations have equal named-call cost in both directions. ◻

Proof. The decisive case is a dynamic call to $h$: changing only its first unfolding leaves recursive calls under the old binding. We therefore induct on the named-call cost of a finite evaluation derivation, with derivation height as a secondary measure.

Fix a closing observation context $H$. For the improvement direction, induct lexicographically on $(k,d)$, where $k$ is the named-call cost of a derivation of $H⟨{\mathcal{L}}_0(t)⟩$ and $d$ is its height. Copy a rule that is not a call to $h$. A premise of equal call cost has smaller height; a premise below any named call has smaller call cost. The induction hypotheses therefore transform every such premise.

At a call $h\overrightarrow{v}$, the call rule spends one named call and evaluates an instance $b_0[\overrightarrow{v}/\overrightarrow{x}]$ under ${\mathcal{L}}_0$. Apply the assumed body improvement in the closing context consisting of the actual arguments, the evaluation prefix, and the continuation. It gives a derivation of $b_1[\overrightarrow{v}/\overrightarrow{x}]$ under ${\mathcal{L}}_0$ with no larger cost. That cost is strictly smaller than the cost of the original call node, because the call node itself contributed one. The outer induction transforms the supplied derivation from binding ${\mathcal{L}}_0$ to binding ${\mathcal{L}}_1$. Reattach the call rule, prefix, and continuation. Summing premise costs shows that the complete transformed derivation uses no more named calls. This proves improvement and forward operational approximation.

For reverse operational approximation, start with a terminating derivation for ${\mathcal{L}}_1(t)$ in the closing context $H$, and use the same lexicographic measure. At a call to $h$, first apply the induction hypothesis to its body derivation; the call node contributes one, so that body has smaller cost. This gives a terminating instance of $b_1$ under ${\mathcal{L}}_0$. The reverse operational-approximation conjunct of the assumed body relation then gives a terminating instance of $b_0$ under ${\mathcal{L}}_0$. Reattach the call rule. The noncall cases copy their final rule as in the forward construction. Thus termination is preserved in the reverse direction. The improvement and two approximation results are the three conjuncts of strong improvement. ◻

Proof. For the second equation, the displayed disjointness condition for $h$ first inserts the unused binding around $u$. Inside that binding, the left program performs the named global unfolding $u{⟶}_{\mathsf{cbv}}{u}_1$; the right program performs one named call to $h$ and then beta-reduces to the same $u_1$. Thus every closing evaluation has a mate with the same result and named-call count, in both directions.

For the first equation, enumerate the finitely many free occurrences of $h$ in $q$. Closing by ${\rho }^{\prime }$ replaces the occurrence $h\pi (\overrightarrow{x})$ by $(\lambda \overrightarrow{x}.u)\pi (\overrightarrow{x})$, which beta-reduces to $u\pi$. Under the displayed letrec, the corresponding call to $h$ unfolds to $u_1\pi$. The first part of the argument, renamed by $\pi$, gives a cost-equivalent replacement at that occurrence. Apply finite-hole congruence from lemma 128.7 to all occurrences. All other variables are closed by the common map $\rho$, so the resulting terms are exactly the two terms displayed in the statement. ◻

Proof. Apply the congruence and transitivity parts of lemma 128.7 to the state-indexed recursive hypotheses. It remains to check the noncongruence step selected by each rule family. All observations below use the named-call cost of definition 128.6; no step-counting or value-equality surrogate is introduced.

Rules R1–R6 and R20 only plug a value, variable, constructor, lambda, or obstructed expression into the recorded context. Rule R7 performs the primitive contraction. Rules R8, R10, R18, and R19 expose exactly the demanded call-by-value evaluation context. Rule R9 replaces multi-argument beta reduction by call-by-value lets; both forms first evaluate the arguments from left to right and then evaluate the same simultaneous substitution instance. Rules R11, R12, R16, and R17 perform the displayed let or case contraction. Rule R15 refines the scrutinee constructor and binds precisely the pattern fields selected by that constructor.

For the substitution arm of R13, strictness of $x$ in $f$ ensures that evaluation of $e$ is demanded before the result of $f$ is returned, and linearity ensures that the substitution creates at most one demand for $e$. Hence it neither removes nor duplicates a possibly diverging call-by-value computation. The other arm leaves the call-by-value let in the residual term. Rule R14 changes the global environment by the displayed recursive value and then drives the body; unfolding that global has exactly the displayed letrec equation.

For A1, suppose $\rho (h)=\lambda \overrightarrow{x}.Q$ and $\hat{g}=Q\pi$. Closing the emitted fold gives $$\rho (h\pi (\overrightarrow{x}))=(\lambda \overrightarrow{x}.Q)\pi (\overrightarrow{x}){⟶}_{\mathsf{cbv}}Q\pi =\hat{g}.$$ The beta contraction costs no named call, and alpha-renaming preserves every later call count by lemma 128.7; hence the fold is cost equivalent to the selected configuration. Rule A2 is the identity residualization at mutual embedding. In A3 and A4a, the equations $f_g[\overrightarrow{f}/\overrightarrow{y}]=\hat{g}$ supplied by lemma 128.5 and the definition of $\mathsf{split}$ reassemble the selected configuration; the recursive hypotheses then apply to ${\mathsf{D}}_{[]}(f_g)$ and every ${\mathsf{D}}_{[]}(f_i)$. The recursive case A4b spends the state indices. Write $\hat{g}=R⟨g⟩$, choose $G(g)=v$, put $\overrightarrow{x}=\mathrm{fv}(\hat{g})$, and let $${\rho }^{\prime }=\rho \cup \{h\mapsto \lambda \overrightarrow{x}.\hat{g}\},q={\mathsf{D}}_{[],G,{\rho }^{\prime }}(R⟨v⟩).$$ The allocation condition for $h$ and abstraction of the complete ordered free-variable list make the new range entry closed. The recursive hypothesis is therefore the state-correct assertion $$R⟨v⟩{⪯}_{\mathsf{s}}{\rho }^{\prime }(q),$$ not the ill-scoped assertion with $\rho (q)$. Put $u=R⟨g⟩$, $u_1=R⟨v⟩$, and $${\mathcal{L}}_0(t)=\mathsf{letrec}h=\lambda \overrightarrow{x}.u_1\mathsf{in}t,{\mathcal{L}}_1(t)=\mathsf{letrec}h=\lambda \overrightarrow{x}.\rho (q)\mathsf{in}t.$$ The global rule in the evaluation context gives $u{⟶}_{\mathsf{cbv}}{u}_1$. Every occurrence of the residual name $h$ emitted while driving $q$ is a saturated call at a renaming of the ordered vector $\overrightarrow{x}$. The first equation of lemma 128.9 therefore gives $${\rho }^{\prime }(q){⪯}_{\mathsf{s}}{\mathcal{L}}_0(\rho (q)).$$ The unused-binding equation and the recursive hypothesis give the annotated body chain This is the body premise of lemma 128.8. That lemma yields $${\mathcal{L}}_0(h\overrightarrow{x}){⪯}_{\mathsf{s}}{\mathcal{L}}_1(h\overrightarrow{x}).$$ The second equation of lemma 128.9 gives $u{\simeq }_{\mathsf{cost}}{\mathcal{L}}_0(h\overrightarrow{x})$. Compose this equivalence with the recursive-replacement conclusion. The resulting left side is $u=\hat{g}$, and its right side is exactly the A4b residual under the outer closing map $\rho$.

In A4c, $h\notin \mathrm{fn}(e)$, so removing the unused allocation changes neither evaluation nor named-call cost. These cases exhaust the ordered ledger. Every use of a recursive result is indexed by its own $(R_{I,j},G_{I,j},{\rho }_{I,j})$, and the only change of closing map is the allocation of $h$ treated above. The displayed state-indexed clause follows. ◻

Proof. Inspect the outer form of the focus. Numerals, variables, globals, constructors, lambdas, primitives, applications, lets, letrecs, and cases are the disjoint outer forms in definition 128.1. Within one outer form, the side conditions printed in the ordered ledger are tested in order; the final arm of R8, the second arm of R13, and R20 cover failure of all earlier tests. A reachable global has exactly one value in $G$ by admissibility. For its application ledger, A1–A3 are tested in order; if none applies, the deterministic finite selector decides A4a, and the decidable occurrence test then distinguishes A4b from A4c. Thus at least one clause applies. Ordered selection prevents two clauses from being selected. ◻