Specialization, supercompilation, and staging

Scheme0 evaluation and specialization

Scheme0 expressions contain constants, variables, primitives, conditionals, and named first-order calls. Its complete call-by-value evaluator is

$P;\rho ⊢c\Downarrow [[c]]$

$\rho (x)=v$

$P;\rho ⊢x\Downarrow v$

$P;\rho ⊢\overrightarrow{e}\Downarrow \overrightarrow{v}$$\delta (\mathsf{op},\overrightarrow{v})=v$

$P;\rho ⊢\mathsf{op}(\overrightarrow{e})\Downarrow v$

$P;\rho ⊢e_0\Downarrow \mathsf{false}$$P;\rho ⊢e_2\Downarrow v$

$P;\rho ⊢\mathsf{if}{e}_0{e}_1{e}_2\Downarrow v$

$P;\rho ⊢e_0\Downarrow v_0$$v_0\ne \mathsf{false}$$P;\rho ⊢e_1\Downarrow v$

$P;\rho ⊢\mathsf{if}{e}_0{e}_1{e}_2\Downarrow v$

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

$P;\rho ⊢\mathsf{call}f\overrightarrow{e}\Downarrow v$

Thus the second branch is selected exactly at $\mathsf{false}$, and the first branch at every other value.

The online numeric projection returns either $\mathsf{known}(n)$ or $\mathsf{res}(r)$. Its complete nonrecursive card is

${\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 uses

${\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))$

The conditional rules are

${\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))$

The fuelled call judgment is $b;\mu ;{\rho }_s{⊢}_{\mathsf{pe}}e\Downarrow q;{\mu }^{\prime }$. With $P(f)=({\overrightarrow{x}}_s;{\overrightarrow{x}}_d;e_f)$, $\pi =(f,\overrightarrow{n})$, and componentwise $\hat{\overrightarrow{q}}=\mathsf{lift}(\overrightarrow{q})$, every noncall rule above lifts by threading the table through its premises from left to right while leaving the budget unchanged. Its three call rules are

$b;\mu ;{\rho }_s{⊢}_{\mathsf{pe}}{\overrightarrow{e}}_s\Downarrow \mathsf{known}(\overrightarrow{n});{\mu }_1$$b;{\mu }_1;{\rho }_s{⊢}_{\mathsf{pe}}{\overrightarrow{e}}_d\Downarrow \overrightarrow{q};{\mu }_2$$\mathrm{name}({\mu }_2(\pi ))=h$

$b;\mu ;{\rho }_s{⊢}_{\mathsf{pe}}\mathsf{call}f({\overrightarrow{e}}_s;{\overrightarrow{e}}_d)\Downarrow \mathsf{res}(\mathsf{call}h(\hat{\overrightarrow{q}}));{\mu }_2$

$0;\mu ;{\rho }_s{⊢}_{\mathsf{pe}}{\overrightarrow{e}}_s\Downarrow \mathsf{known}(\overrightarrow{n});{\mu }_1$$0;{\mu }_1;{\rho }_s{⊢}_{\mathsf{pe}}{\overrightarrow{e}}_d\Downarrow \overrightarrow{q};{\mu }_2$$\pi \notin \mathrm{dom}({\mu }_2)$

$0;\mu ;{\rho }_s{⊢}_{\mathsf{pe}}\mathsf{call}f({\overrightarrow{e}}_s;{\overrightarrow{e}}_d)\Downarrow \mathsf{res}(\mathsf{call}f(\overrightarrow{n};\hat{\overrightarrow{q}}));{\mu }_2$

$(b+1);\mu ;{\rho }_s{⊢}_{\mathsf{pe}}{\overrightarrow{e}}_s\Downarrow \mathsf{known}(\overrightarrow{n});{\mu }_1$$(b+1);{\mu }_1;{\rho }_s{⊢}_{\mathsf{pe}}{\overrightarrow{e}}_d\Downarrow \overrightarrow{q};{\mu }_2$$\pi \notin \mathrm{dom}({\mu }_2)h\mathsf{fresh}$${\mu }_3={\mu }_2[\pi \mapsto h]$$b;{\mu }_3;[{\overrightarrow{x}}_s\mapsto \overrightarrow{n}]{⊢}_{\mathsf{pe}}{e}_f\Downarrow q_f;{\mu }_4$${\mu }_5=\mathsf{complete}({\mu }_4,\pi ,h({\overrightarrow{x}}_d)=\mathsf{lift}(q_f))$

$(b+1);\mu ;{\rho }_s{⊢}_{\mathsf{pe}}\mathsf{call}f({\overrightarrow{e}}_s;{\overrightarrow{e}}_d)\Downarrow \mathsf{res}(\mathsf{call}h(\hat{\overrightarrow{q}}));{\mu }_5$

The offline binding-time checker uses $b\in \{S,D\}$ and a division $\tau$ from variables to binding times. Its exact 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$

For , calls with dynamic arguments use

$\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 offline specialization, write $q::=\mathsf{val}(v)\mid \mathsf{code}(r)$ and $\xi =({\rho }_s;{\eta }_d)$. Its complete scalar rule card is

$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)$, calls and lifting use

$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))$

The corresponding vector judgments apply these scalar rules from left to right. Offline residualization returns a program only through a finite completed graph $(\nu ,E,r_0)$: $\nu$ injectively names every reached static call state, $E$ contains the specialized equation for each named state, every residual call targets another state in $\mathrm{dom}(\nu )$, and the main expression yields $r_0$. A state is named before its body is specialized, so a revisit is a back edge. If this reachability expansion does not terminate, no residual program is returned. The finite-return proof maintains ${\mathcal{I}}_k(\mu ,{\mu }_{\ast })$: every pending entry has one allocating ancestor and one eventual equation, every completed entry simulates its source body below height $k$, and fuel-zero retention is closed under source calls. Recursive hits are justified by smaller evaluation height, not by induction on the cyclic table.

SC-CBV driving, folding, and whistle

An SC-CBV configuration is a residual context focused on one expression. The source’s $\mathsf{letrec}$ is macro-expanded using its distinguished global fixpoint before concrete evaluation. The chapter’s pedagogical projection ${\mathsf{drive}}_0$ is partial and contains only beta, known-case, and open-case configurations; the full driver is the ordered source ledger R1–R20. Write $R⟨e⟩$ for context plugging, let $a$ range over obstructed expressions, and let $\rho$ record fresh residual names paired with earlier calls. For $B=\{p_i\Rightarrow e_i{\}}_i$, put $$B_x^R=\{p_i\Rightarrow {\mathsf{D}}_{[]}((R⟨e_i⟩)[p_i/x]){\}}_i,B_R=\{p_i\Rightarrow {\mathsf{D}}_{[]}(R⟨e_i⟩){\}}_i.$$ The complete ordered ledger is where the last equation requires that $y$ was not introduced by a preceding split. For R13, let $L=\mathsf{let}x=e\mathsf{in}f$ and $Q=x\in \mathsf{strict}(f)\cap \mathsf{linear}(f)$. Then Here $R_{\mathsf{case}}=R⟨\mathsf{C}[[];B]⟩$ in R19; the rules are tried in numerical order. The obstructed grammar is $$a::=x\mid n\oplus a\mid a\oplus n\mid a\oplus a\mid a\overrightarrow{e}.$$

The application ledger completes the driver card. An entry for a configuration $Q$, with ordered free-variable vector $\overrightarrow{x}$, is $\rho (h)=\lambda \overrightarrow{x}.Q$; write $(h,Q)\in \rho$ for this assertion. Put $\hat{g}=R⟨g⟩$. The alternatives are tried in the displayed order: If none of A1–A3 applies, choose the first residual name $h$ allowed by the chapter’s allocation condition and put For $\mathrm{Sub}(e)$, the finite set of strict proper subexpressions of $e$, the remaining ordered alternatives are

The pedagogical projection’s beta rule is

${\mathsf{drive}}_0(R⟨(\lambda x.e)v⟩)=\{([v/x],R⟨e⟩)\}$

For $\mathcal{B}=\{c_i({\overrightarrow{x}}_i)\Rightarrow e_i{\}}_{i\in I}$, put $${\theta }_j=[c_j({\overrightarrow{z}}_j)/y],Q_j=R{\theta }_j⟨\mathsf{case}{c}_j({\overrightarrow{z}}_j)\mathsf{of}\mathcal{B}⟩.$$ A known constructor case selects one branch and substitutes its fields; an open-variable case refines the scrutinee once for every constructor and retains the case for the next known-case node:

$j\in I$

${\mathsf{drive}}_0(R⟨\mathsf{case}{c}_j(\overrightarrow{v})\mathsf{of}\mathcal{B}⟩)=\{([\overrightarrow{v}/{\overrightarrow{x}}_j],R⟨e_j⟩)\}$

$y\text{is free}j\in I$

${\mathsf{drive}}_0(R⟨\mathsf{case}y\mathsf{of}\mathcal{B}⟩)=\{({\theta }_j,Q_j){\}}_{j\in I}$

For beta and known-case edges, compatibility means the closed parent takes one concrete call-by-value contraction to the instantiated child; for an open-case edge it means equality after shape refinement. Alpha-equivalent configurations fold to the earlier residual function. Homeomorphic embedding on constructor trees is generated by

$x\preccurlyeq y$

$n_1\preccurlyeq n_2$

$s\preccurlyeq t_i$

$s\preccurlyeq c(t_1,\dots ,t_k)$

$s_i\preccurlyeq t_i(1\le i\le k)$

$c(s_1,\dots ,s_k)\preccurlyeq c(t_1,\dots ,t_k)$

When the whistle fires, most-specific generalization returns substitutions $({\theta }_1,{\theta }_2)$ and a common pattern $g$ with $g{\theta }_1=e_1$ and $g{\theta }_2=e_2$; processing continues on the smaller generalized nodes under the source’s memo invariant.

The dual-context staging core

$\mathsf{Tstage}$ separates persistent assumptions $u::A\in \mathrm{\Delta }$ from ordinary assumptions $x:A\in \mathrm{\Gamma }$:

$x:A\in \mathrm{\Gamma }$

$\mathrm{\Delta };\mathrm{\Gamma }⊢x:A$

$u::A\in \mathrm{\Delta }$

$\mathrm{\Delta };\mathrm{\Gamma }⊢u:A$

$\mathrm{\Delta };\mathrm{\Gamma },x:A⊢M:B$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\lambda x:A.M:A\to B$

$\mathrm{\Delta };\mathrm{\Gamma }⊢M:A\to B$$\mathrm{\Delta };\mathrm{\Gamma }⊢N:A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢MN:B$

$\mathrm{\Delta };\varnothing ⊢M:A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{box}M:◻A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢M:◻A$$\mathrm{\Delta },u::A;\mathrm{\Gamma }⊢N:B$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{let}\mathsf{box}u=M\mathsf{in}N:B$

Staged computation has the two contractions

$(\lambda x:A.M)N⟶M[N/x]$

$\mathsf{let}\mathsf{box}u=\mathsf{box}M\mathsf{in}N⟶N[M/u]$

Its complete compatible closure is

$M⟶M^{\prime }$

$\lambda x:A.M⟶\lambda x:A.M^{\prime }$

$M⟶M^{\prime }$

$MN⟶M^{\prime }N$

$N⟶N^{\prime }$

$MN⟶M{N}^{\prime }$

$M⟶M^{\prime }$

$\mathsf{let}\mathsf{box}u=M\mathsf{in}N⟶\mathsf{let}\mathsf{box}u=M^{\prime }\mathsf{in}N$

$N⟶N^{\prime }$

$\mathsf{let}\mathsf{box}u=M\mathsf{in}N⟶\mathsf{let}\mathsf{box}u=M\mathsf{in}{N}^{\prime }$

There is no congruence beneath a box. The box-introduction premise’s empty ordinary context is the scope invariant; persistent substitution may cross a box and ordinary substitution may not.

Davies–Pfenning’s conservative two-level source is a different card. It has run-time and compile-time judgments $\mathrm{\Delta };\mathrm{\Gamma }{⊢}^{r}e:\tau$ and $\mathrm{\Delta }{⊢}^{c}e:\sigma$, with separately phase-marked Mini-ML constructors for functions, products, unit, naturals, case, and fixed points. For $p\in \{r,c\}$, let ${\mathcal{C}}_r=\mathrm{\Delta };\mathrm{\Gamma }$ and ${\mathcal{C}}_c=\mathrm{\Delta }$. Its ordinary constructors have the complete phase-indexed rule schema

$x:T\in {\mathcal{C}}_p$

${\mathcal{C}}_p{⊢}^{p}x:T$

${\mathcal{C}}_p,x:T_1{⊢}^{p}e:T_2$

${\mathcal{C}}_p{⊢}^p{\lambda }^{p}x:T_1.e:T_1\to T_2$

${\mathcal{C}}_p{⊢}^p{e}_1:T_1\to T_2$${\mathcal{C}}_p{⊢}^p{e}_2:T_1$

${\mathcal{C}}_p{⊢}^p{e}_1{@}^p{e}_2:T_2$

${\mathcal{C}}_p,x:T{⊢}^{p}e:T$

${\mathcal{C}}_p{⊢}^p{\mathsf{fix}}^{p}x:T.e:T$

${\mathcal{C}}_p{⊢}^p{e}_1:T_1$${\mathcal{C}}_p{⊢}^p{e}_2:T_2$

${\mathcal{C}}_p{⊢}^p⟨e_1,e_2{⟩}^p:T_1\times T_2$

${\mathcal{C}}_p{⊢}^{p}e:T_1\times T_2$

${\mathcal{C}}_p{⊢}^p{\mathsf{proj}}_i^p(e):T_i$

${\mathcal{C}}_p{⊢}^p⟨{⟩}^p:1$

${\mathcal{C}}_p{⊢}^p{\mathsf{z}}^p:\mathsf{nat}$

${\mathcal{C}}_p{⊢}^{p}e:\mathsf{nat}$

${\mathcal{C}}_p{⊢}^p{\mathsf{s}}^{p}e:\mathsf{nat}$

${\mathcal{C}}_p{⊢}^p{e}_0:\mathsf{nat}$${\mathcal{C}}_p{⊢}^p{e}_z:T$${\mathcal{C}}_p,x:\mathsf{nat}{⊢}^p{e}_s:T$

${\mathcal{C}}_p{⊢}^p{\mathsf{case}}^p{e}_0\mathsf{of}\mathsf{z}\Rightarrow e_z\mid \mathsf{s}x\Rightarrow e_s:T$

Its only phase-changing rules are

$\mathrm{\Delta }{⊢}^{c}e:\underset{―}{\tau }$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}^{r}e:\tau$

$\mathrm{\Delta };\varnothing {⊢}^{r}e:\tau$

$\mathrm{\Delta }{⊢}^{c}e:\underset{―}{\tau }$

The mutually recursive translation sends $\underset{―}{\tau }$ to $◻\Vert \tau \Vert$ and has the exact boundary equations $$\Vert \bar{e}\Vert ={\mathsf{unbox}}_1|\bar{e}|,|\underset{―}{e}|=\mathsf{box}\Vert \underset{―}{e}\Vert .$$ The target judgment $\mathcal{S}{⊢}^{i}M:A$ uses a stack of ordinary contexts. Its load-bearing function and boundary rules are

$x:T\in \mathrm{last}(\mathcal{S})$

$\mathcal{S}{⊢}^{i}x:T$

$\mathcal{S},x:T{⊢}^{i}M:U$

$\mathcal{S}{⊢}^i\lambda x:T.M:T\to U$

$\mathcal{S}{⊢}^{i}M:T\to U$$\mathcal{S}{⊢}^{i}N:T$

$\mathcal{S}{⊢}^{i}MN:U$

$\mathcal{S};\varnothing {⊢}^{i}M:T$

$\mathcal{S}{⊢}^i\mathsf{box}M:◻T$

$\mathcal{S}{⊢}^{i}M:◻T$

$\mathcal{S};\mathrm{\Gamma }{⊢}^i{\mathsf{unbox}}_{1}M:T$

The remaining target rules are

$\mathcal{S},x:T{⊢}^{i}M:T$

$\mathcal{S}{⊢}^i\mathsf{fix}x:T.M:T$

$\mathcal{S}{⊢}^{i}M:T_1$$\mathcal{S}{⊢}^{i}N:T_2$

$\mathcal{S}{⊢}^i⟨M,N⟩:T_1\times T_2$

$\mathcal{S}{⊢}^{i}M:T_1\times T_2$

$\mathcal{S}{⊢}^i{\mathsf{proj}}_j(M):T_j$

$\mathcal{S}{⊢}^i⟨⟩:1$

$\mathcal{S}{⊢}^i\mathsf{z}:\mathsf{nat}$

$\mathcal{S}{⊢}^{i}M:\mathsf{nat}$

$\mathcal{S}{⊢}^i\mathsf{s}M:\mathsf{nat}$

$\mathcal{S}{⊢}^{i}M:\mathsf{nat}$$\mathcal{S}{⊢}^i{M}_z:T$$\mathcal{S},x:\mathsf{nat}{⊢}^i{M}_s:T$

$\mathcal{S}{⊢}^i\mathsf{case}M\mathsf{of}\mathsf{z}\Rightarrow M_z\mid \mathsf{s}x\Rightarrow M_s:T$

Box pushes an empty component and ${\mathsf{unbox}}_1$ crosses exactly one boundary. These are every target family used by the translation. Its conservative embedding proves both preservation and reflection of the two typing judgments; it is not a relabelling of $\mathsf{Tstage}$.

MacoCaml compilation boundary

The separate MacoCaml source judgment $${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_n^{\star }e:\tau ⇝e^{\prime };{\sigma }_2,\star \in \{c,s,q\},$$ threads a compile-time heap, records the integer binding level and compiler mode, and returns elaborated core syntax. Quotation and nested splice are

${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_{n+1}^{q}e:\tau ⇝e^{\prime };{\sigma }_2$

${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_n^{c\vee s}⟨e⟩:\mathsf{Code}\tau ⇝⟨e^{\prime }⟩;{\sigma }_2$

${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_{n-1}^{s}e:\mathsf{Code}\tau ⇝e^{\prime };{\sigma }_2$

${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_n^q\mathrm{\$}e:\tau ⇝\mathrm{\$}{e}^{\prime };{\sigma }_2$

The symbol $c\vee s$ denotes one rule instance at each mode. A top-level splice instead uses

${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_{n-1}^{s}e:\mathsf{Code}\tau ⇝e^{\prime };{\sigma }_2$${\sigma }_2;\mathrm{\Omega }⊢e^{\prime }{⟶}_0^{\ast }⟨v⟩;{\sigma }_3$

${\sigma }_1;\mathrm{\Omega };\mathrm{\Gamma }{⊢}_n^c\mathrm{\$}e:\tau ⇝v;{\sigma }_3$

The empty-heap consequence is theorem 129.10. These rules are not modal box rules.

Tan–Wei semantics-preserving two-stage cards

The pure comparison calculus ${\lambda }_{|2|}$ has stages $s\in \{\mathbb{1},\mathbb{2}\}$, reification effects $ϵ\in \{\mathrm{\perp },\mathrm{\top }\}$, and the two judgments $$\mathrm{\Gamma }{⊢}^{s}t:\tau \mid ϵ,\mathrm{\Gamma }⊢t:\tau \mid ϵ.$$ Its code types distinguish complete code $\mathsf{rep}(\tau )$ from a reifiable fragment $\mathsf{frag}(\tau )$. The bridge rules are

$\mathrm{\Gamma }{⊢}^{\mathbb{1}}t:\tau \mid \mathrm{\perp }$

$\mathrm{\Gamma }⊢t:\tau \mid \mathrm{\perp }$

$\mathrm{\Gamma }{⊢}^{\mathbb{1}}t:\mathsf{frag}(\tau )\mid ϵ$

$\mathrm{\Gamma }⊢t:\mathsf{rep}(\tau )\mid ϵ$

The administrative rules are

$\mathrm{\Gamma }{⊢}^{\mathbb{2}}t:\tau \mid \mathrm{\perp }$

$\mathrm{\Gamma }{⊢}^{\mathbb{1}}\mathsf{code}t:\mathsf{rep}(\tau )\mid \mathrm{\perp }$

$\mathrm{\Gamma }{⊢}^{\mathbb{2}}t:\tau \mid \mathrm{\perp }$

$\mathrm{\Gamma }{⊢}^{\mathbb{1}}\mathsf{reflect}t:\mathsf{frag}(\tau )\mid \mathrm{\top }$

$\mathrm{\Gamma }{⊢}^{\mathbb{2}}{t}_1:{\tau }_1\mid \mathrm{\perp }$$\mathrm{\Gamma },x^{\mathbb{2}}:{\tau }_1⊢t_2:\mathsf{rep}({\tau }_2)\mid ϵ$${\mathsf{WF}}^{\mathbb{2}}({\tau }_1)$

$\mathrm{\Gamma }{⊢}^{\mathbb{1}}{\mathsf{let}}_{\mathsf{c}}x=t_1\mathsf{in}{t}_2:\mathsf{rep}({\tau }_2)\mid \mathrm{\perp }$

For $x$ fresh, automatic let insertion is the root-compatible step $$P[E[\mathsf{reflect}t]]⟶P[{\mathsf{let}}_{\mathsf{c}}x=t\mathsf{in}E[\mathsf{code}x]],$$ where $E$ contains only ordinary pure evaluation frames and $P$ is a reification context. Stage erasure sends inserted ${\mathsf{let}}_{\mathsf{c}}$ to ordinary let and deletes the remaining administrative staging forms.

The ${\lambda }_{|2|}^{\mathsf{ref}}$ delta adds natural-number locations and stores. Generated-stage allocation, get, and put build fragments under ${⊢}^{\mathbb{1}}$; the corresponding executing operations occur only under ${⊢}^{\mathbb{2}}$. The run-rule delta is

$\mathsf{storeFree}(t)$$\varnothing ⊢t:\mathsf{rep}(\tau )\mid ϵ$

$\mathrm{\Gamma }{⊢}^{\mathbb{1}}\mathsf{run}t:\tau \mid \mathrm{\perp }$

Its store-freedom and empty-context premises ensure that first-stage evaluation begins and ends with the empty store. Its logical relation adds a world which is a partial bijection of locations and extends that world after allocation. The exact pure and reference consequences are lemma 129.11, theorem 129.12; neither card is $\mathsf{Tstage}$, MetaOCaml, or LMS.

Dependent multistage typing

Stages are finite words $A,B$ over stage variables. Context declarations record an exact stage, and variable use requires that exact match. Kinds and types have the complete formation and checking rules

$\mathrm{\Gamma }⊢\ast \mathsf{kind}@A$

$\mathrm{\Gamma }⊢\tau ::\ast @A$$\mathrm{\Gamma },x:\tau @A⊢K\mathsf{kind}@A$

$\mathrm{\Gamma }⊢\mathrm{\Pi }x:\tau .K\mathsf{kind}@A$

$X::K\in \mathrm{\Sigma }$

$\mathrm{\Gamma }⊢X::K@A$

$\mathrm{\Gamma }⊢\sigma ::\mathrm{\Pi }x:\tau .K@A$$\mathrm{\Gamma }⊢M:\tau @A$

$\mathrm{\Gamma }⊢\sigma M::K[M/x]@A$

$\mathrm{\Gamma }⊢\tau ::\ast @A\alpha$

$\mathrm{\Gamma }⊢{▹}_{\alpha }\tau ::\ast @A$

$\mathrm{\Gamma }⊢\tau ::K@A$$\alpha \notin \mathrm{FTV}(\mathrm{\Gamma })\cup \mathrm{FTV}(A)$

$\mathrm{\Gamma }⊢\mathrm{\forall }\alpha .\tau ::K@A$

$\mathrm{\Gamma }⊢\tau ::\ast @A$

$\mathrm{\Gamma }⊢\tau ::\ast @A\alpha$

$\mathrm{\Gamma }⊢\tau ::K@A$$\mathrm{\Gamma }⊢K\equiv J@A$

$\mathrm{\Gamma }⊢\tau ::J@A$

$\mathrm{\Gamma }⊢\tau ::\ast @A$$\mathrm{\Gamma },x:\tau @A⊢\sigma ::\ast @A$

$\mathrm{\Gamma }⊢\mathrm{\Pi }x:\tau .\sigma ::\ast @A$

The complete term-typing card begins with

$c:\tau \in \mathrm{\Sigma }$

$\mathrm{\Gamma }⊢c:\tau @A$

$x:\tau @A\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x:\tau @A$

$\mathrm{\Gamma }⊢\tau ::\ast @A$$\mathrm{\Gamma },x:\tau @A⊢M:\sigma @A$

$\mathrm{\Gamma }⊢\lambda x:\tau .M:\mathrm{\Pi }x:\tau .\sigma @A$

$\mathrm{\Gamma }⊢M:\mathrm{\Pi }x:\tau .\sigma @A$$\mathrm{\Gamma }⊢N:\tau @A$

$\mathrm{\Gamma }⊢MN:\sigma [N/x]@A$

$\mathrm{\Gamma }⊢M:\tau @A$$\mathrm{\Gamma }⊢\tau \equiv \sigma ::\ast @A$

$\mathrm{\Gamma }⊢M:\sigma @A$

Quotation, escape, stage abstraction/application, and cross-stage persistence are

$\mathrm{\Gamma }⊢M:\tau @A\alpha$

$\mathrm{\Gamma }⊢⟨M{⟩}_{\alpha }:{▹}_{\alpha }\tau @A$

$\mathrm{\Gamma }⊢M:{▹}_{\alpha }\tau @A$

$\mathrm{\Gamma }⊢{\sim }_{\alpha }M:\tau @A\alpha$

$\mathrm{\Gamma }⊢M:\tau @A$$\alpha \notin \mathrm{FTV}(\mathrm{\Gamma })\cup \mathrm{FTV}(A)$

$\mathrm{\Gamma }⊢\mathrm{\Lambda }\alpha .M:\mathrm{\forall }\alpha .\tau @A$

$\mathrm{\Gamma }⊢M:\mathrm{\forall }\alpha .\tau @A$

$\mathrm{\Gamma }⊢MB:\tau [B/\alpha ]@A$

$\mathrm{\Gamma }⊢M:\tau @A$

$\mathrm{\Gamma }⊢{\mathrm{\%}}_{\alpha }M:\tau @A\alpha$

The three equality judgments are $\mathrm{\Gamma }⊢K\equiv J@A$, $\mathrm{\Gamma }⊢\tau \equiv \sigma ::K@A$, and $\mathrm{\Gamma }⊢M\equiv N:\tau @A$. Kind equality is generated by

$\mathrm{\Gamma }⊢\tau \equiv \sigma ::\ast @A$$\mathrm{\Gamma },x:\tau @A⊢K\equiv J@A$

$\mathrm{\Gamma }⊢\mathrm{\Pi }x:\tau .K\equiv \mathrm{\Pi }x:\sigma .J@A$

$\mathrm{\Gamma }⊢K\equiv J@A$

$\mathrm{\Gamma }⊢K\equiv J@A\alpha$

$\mathrm{\Gamma }⊢K\mathsf{kind}@A$

$\mathrm{\Gamma }⊢K\equiv K@A$

$\mathrm{\Gamma }⊢K\equiv J@A$

$\mathrm{\Gamma }⊢J\equiv K@A$

$\mathrm{\Gamma }⊢K\equiv J@A$$\mathrm{\Gamma }⊢J\equiv I@A$

$\mathrm{\Gamma }⊢K\equiv I@A$

Type equality is generated by

$\mathrm{\Gamma }⊢\tau \equiv \sigma ::\ast @A$$\mathrm{\Gamma },x:\tau @A⊢\rho \equiv \pi ::\ast @A$

$\mathrm{\Gamma }⊢\mathrm{\Pi }x:\tau .\rho \equiv \mathrm{\Pi }x:\sigma .\pi ::\ast @A$

$\mathrm{\Gamma }⊢\tau \equiv \sigma ::\mathrm{\Pi }x:\rho .K@A$$\mathrm{\Gamma }⊢M\equiv N:\rho @A$

$\mathrm{\Gamma }⊢\tau M\equiv \sigma N::K[M/x]@A$

$\mathrm{\Gamma }⊢\tau \equiv \sigma ::\ast @A\alpha$

$\mathrm{\Gamma }⊢{▹}_{\alpha }\tau \equiv {▹}_{\alpha }\sigma ::\ast @A$

$\mathrm{\Gamma }⊢\tau \equiv \sigma ::\ast @A$$\alpha \notin \mathrm{FTV}(\mathrm{\Gamma })\cup \mathrm{FTV}(A)$

$\mathrm{\Gamma }⊢\mathrm{\forall }\alpha .\tau \equiv \mathrm{\forall }\alpha .\sigma ::\ast @A$

$\mathrm{\Gamma }⊢\tau \equiv \sigma ::\ast @A$

$\mathrm{\Gamma }⊢\tau \equiv \sigma ::\ast @A\alpha$

$\mathrm{\Gamma }⊢\tau ::K@A$

$\mathrm{\Gamma }⊢\tau \equiv \tau ::K@A$

$\mathrm{\Gamma }⊢\tau \equiv \sigma ::K@A$

$\mathrm{\Gamma }⊢\sigma \equiv \tau ::K@A$

$\mathrm{\Gamma }⊢\tau \equiv \sigma ::K@A$$\mathrm{\Gamma }⊢\sigma \equiv \rho ::K@A$

$\mathrm{\Gamma }⊢\tau \equiv \rho ::K@A$

Term congruence and equivalence are

$\mathrm{\Gamma }⊢\tau \equiv \sigma ::\ast @A$$\mathrm{\Gamma },x:\tau @A⊢M\equiv N:\rho @A$

$\mathrm{\Gamma }⊢\lambda x:\tau .M\equiv \lambda x:\sigma .N:\mathrm{\Pi }x:\tau .\rho @A$

$\mathrm{\Gamma }⊢M\equiv L:\mathrm{\Pi }x:\sigma .\tau @A$$\mathrm{\Gamma }⊢N\equiv O:\sigma @A$

$\mathrm{\Gamma }⊢MN\equiv LO:\tau [N/x]@A$

$\mathrm{\Gamma }⊢M\equiv N:\tau @A\alpha$

$\mathrm{\Gamma }⊢⟨M{⟩}_{\alpha }\equiv ⟨N{⟩}_{\alpha }:{▹}_{\alpha }\tau @A$

$\mathrm{\Gamma }⊢M\equiv N:{▹}_{\alpha }\tau @A$

$\mathrm{\Gamma }⊢{\sim }_{\alpha }M\equiv {\sim }_{\alpha }N:\tau @A\alpha$

$\mathrm{\Gamma }⊢M\equiv N:\tau @A$$\alpha \notin \mathrm{FTV}(\mathrm{\Gamma })\cup \mathrm{FTV}(A)$

$\mathrm{\Gamma }⊢\mathrm{\Lambda }\alpha .M\equiv \mathrm{\Lambda }\alpha .N:\mathrm{\forall }\alpha .\tau @A$

$\mathrm{\Gamma }⊢M\equiv N:\mathrm{\forall }\alpha .\tau @A$

$\mathrm{\Gamma }⊢MB\equiv NB:\tau [B/\alpha ]@A$

$\mathrm{\Gamma }⊢M\equiv N:\tau @A$

$\mathrm{\Gamma }⊢{\mathrm{\%}}_{\alpha }M\equiv {\mathrm{\%}}_{\alpha }N:\tau @A\alpha$

$\mathrm{\Gamma }⊢M:\tau @A$

$\mathrm{\Gamma }⊢M\equiv M:\tau @A$

$\mathrm{\Gamma }⊢M\equiv N:\tau @A$

$\mathrm{\Gamma }⊢N\equiv M:\tau @A$

$\mathrm{\Gamma }⊢M\equiv N:\tau @A$$\mathrm{\Gamma }⊢N\equiv L:\tau @A$

$\mathrm{\Gamma }⊢M\equiv L:\tau @A$

Its four computational axioms are

$\mathrm{\Gamma },x:\sigma @A⊢M:\tau @A$$\mathrm{\Gamma }⊢N:\sigma @A$

$\mathrm{\Gamma }⊢(\lambda x:\sigma .M)N\equiv M[N/x]:\tau [N/x]@A$

$\mathrm{\Gamma }⊢M\equiv N:\tau @A\alpha$

$\mathrm{\Gamma }⊢{\sim }_{\alpha }⟨M{⟩}_{\alpha }\equiv N:\tau @A\alpha$

$\mathrm{\Gamma }⊢\mathrm{\Lambda }\alpha .M:\mathrm{\forall }\alpha .\tau @A$

$\mathrm{\Gamma }⊢(\mathrm{\Lambda }\alpha .M)B\equiv M[B/\alpha ]:\tau [B/\alpha ]@A$

$\mathrm{\Gamma }⊢M:\tau @A\alpha$$\mathrm{\Gamma }⊢M:\tau @A$

$\mathrm{\Gamma }⊢{\mathrm{\%}}_{\alpha }M\equiv M:\tau @A\alpha$

For staged evaluation, constant-headed neutral spines and values are defined mutually by Let $D$ be either $\epsilon$ or one stage variable. The hole of $E_D^A$ lies at stage $D$, and the whole context lies at stage $A$: The redex grammar is $$R^{\epsilon }::=(\lambda x:\tau .M)v^{\epsilon }\mid (\mathrm{\Lambda }\alpha .v^{\epsilon })C,R^{\alpha }::={\sim }_{\alpha }⟨v^{\alpha }{⟩}_{\alpha }.$$ The staged relation consists exactly of These are published ${\lambda }^{\mathsf{MD}}$ rules. The theorem-bearing book-local system ${\lambda }_{\mathsf{is}}^{\mathsf{MD}}$ deletes type-equivalence rule MD-QT-CSP; code-head inversion additionally states the body-formation premise required because the remaining type-level CSP formation rule can move a code type to a later word. Its staged final forms extend the published value grammar by constant-headed spines, which repairs stuck function-constant applications without adding a full-reduction rule. Its full contexts remain in the term syntactic category and never enter a binder annotation, type, or kind. A typed dependent-annotation peak therefore refutes exact syntactic confluence; the chapter proves confluence only modulo binder-annotation erasure. These explicit boundaries govern the chapter’s preservation, term-only normalization, annotation-erased confluence, decomposition, and staged-progress proofs. They are not the exact published metatheorem package.