ch:dependent-staging: ch:dependent-staging

From $\mathrm{\Gamma }⊢v:\mathsf{Vec}An@\epsilon$, rule MD-CSP derives $\mathrm{\Gamma }⊢{\mathrm{\%}}_{\alpha }v:\mathsf{Vec}An@\alpha$; the corresponding type is well formed at $\alpha$ by MD-TCSP. Rule MD-Quote therefore gives After removing ${\mathrm{\%}}_{\alpha }$, the quotation premise would require $$\mathrm{\Gamma }⊢v:\mathsf{Vec}An@\alpha .$$ The declaration of $v$ is at $\epsilon$, and MD-Var requires an exact stage match, so that premise fails.

Inversion of the redex typing gives $\mathrm{\Gamma }⊢\mathrm{\Lambda }\alpha .M:\mathrm{\forall }\alpha .\tau @A$ and hence, after renaming $\alpha$ fresh for $\mathrm{\Gamma },A,B$, the premise $\mathrm{\Gamma }⊢M:\tau @A$. Rule MD-SApp types the redex at $\tau [B/\alpha ]@A$. The stage-substitution clause of lemma 130.3 yields $$\mathrm{\Gamma }[B/\alpha ]⊢M[B/\alpha ]:\tau [B/\alpha ]@A[B/\alpha ].$$ Freshness makes the context and $A$ unchanged, giving exactly the type of the contractum. If the result type were left as $\tau$, a free occurrence of $\alpha$ in $\tau$ would remain after its binder disappeared; the claimed conclusion would be ill formed and would not match the MD-SApp conclusion.

Write the outer redex as $(\mathrm{\Lambda }\alpha .M)B$. If $M⟶M^{\prime }$, the peak is $$(\mathrm{\Lambda }\alpha .M)B⟶M[B/\alpha ],(\mathrm{\Lambda }\alpha .M)B⟶(\mathrm{\Lambda }\alpha .M^{\prime })B.$$ Compatibility of stage substitution with full reduction, proved by induction on the inner reduction, gives $M[B/\alpha ]{⟶}^{\ast }{M}^{\prime }[B/\alpha ]$. Stage substitution does not duplicate a term occurrence, but it can expand one labelled escape–quotation pair into a shell containing $|B|$ primitive splices. For example, with a constant $c$ and $B=\beta \gamma$, take $$M=⟨{\sim }_{\alpha }⟨c{⟩}_{\alpha }{⟩}_{\alpha }.$$ After the outer stage-beta step its residual inner redex is $${\mathsf{q}}_{\beta \gamma }({\mathsf{e}}_{\beta \gamma }({\mathsf{q}}_{\beta \gamma }(c))).$$ Contract the $\beta$-splice and then the $\gamma$-splice to obtain $${\mathsf{q}}_{\beta \gamma }({\mathsf{e}}_{\beta \gamma }({\mathsf{q}}_{\beta \gamma }(c)))\stackrel{\beta \text{-splice}}{⟶}{\mathsf{q}}_{\beta \gamma }({\mathsf{e}}_{\gamma }({\mathsf{q}}_{\gamma }(c)))\stackrel{\gamma \text{-splice}}{⟶}{\mathsf{q}}_{\beta \gamma }(c).$$ For a word of length $n$, the same shell induction transports the residual through exactly $n$ primitive splice contractions; for the empty word the two substituted endpoints coincide. Contracting stage beta on the right gives $M^{\prime }[B/\alpha ]$. Thus the residual inner step is transported through stage substitution, while the residual outer redex remains at the root of $(\mathrm{\Lambda }\alpha .M^{\prime })B$.

For the splice peak, write the term as ${\sim }_{\alpha }⟨M{⟩}_{\alpha }$ with an ordinary beta step $M⟶M^{\prime }$. The root step yields $M$, which takes that beta step to $M^{\prime }$. Quotation and escape compatibility yield ${\sim }_{\alpha }⟨M^{\prime }{⟩}_{\alpha }$, whose root splice step also yields $M^{\prime }$. These are the two required common reducts.

Use the signature constants $a_0,a_1:A$ from the chapter. Persist them and form at stage $\alpha$ $$v_2=\mathsf{cons}1({\mathrm{\%}}_{\alpha }{a}_1)(\mathsf{cons}0({\mathrm{\%}}_{\alpha }{a}_0)\mathsf{nil}):\mathsf{Vec}A2@\alpha .$$ Then MD-Quote gives $⟨v_2{⟩}_{\alpha }:{▹}_{\alpha }(\mathsf{Vec}A2)@\epsilon$. The generator is the empty-stage term $G_2=⟨v_2{⟩}_{\alpha }$; staged evaluation stops immediately at that quotation because its constant-headed constructor applications at stage $\alpha$ are future-stage values, not contractions. Inverting its type with lemma 130.2 verifies the body judgment at the extended stage $\alpha$. The CSP markers make persistence explicit but are removable by MD-Q-Percent, since MD-Const types the signature constants at both stages. This closed example therefore satisfies the empty-stage hypothesis of theorem 130.15.

Start generation in the empty store. Allocation chooses its least unused location, so $$(\varnothing ,\mathsf{new}0)⟼(\{{\ell }_0\mapsto 0\},{\ell }_0).$$ Unrestricted CSP constructs the code value $C=⟨!({\mathrm{\%}}_{\alpha }{\ell }_0){⟩}_{\alpha }$. The generation boundary returns $C$ and discards the generation store, leaving $(\varnothing ,C)$.

For the first later evaluation, allocation again chooses location zero: $$(\varnothing ,\mathsf{new}0)⟼(\{{\ell }_0\mapsto 0\},{\ell }_0),(\{{\ell }_0\mapsto 0\},!{\ell }_0)⟼(\{{\ell }_0\mapsto 0\},0).$$ For the second, the same rule with initializer one gives $$(\varnothing ,\mathsf{new}1)⟼(\{{\ell }_0\mapsto 1\},{\ell }_0),(\{{\ell }_0\mapsto 1\},!{\ell }_0)⟼(\{{\ell }_0\mapsto 1\},1).$$ The identical closed code value $C$ therefore returns zero or one according to a store allocated after generation. A canonical-forms argument that treats a closed code value as carrying every resource needed by its body is false; equivalently, the store-independent reduct assumed when commuting a generated code step with an unrelated later allocation is false. The pure calculus’s CSP rule therefore requires a world/store discipline before it can persist locations.