Dependent Multi-Stage Type Theory

Proof. First, induction on a type-equivalence derivation proves regularity: both endpoint types check at the displayed kind and stage. Constructor congruences rebuild their formation rules, reflexivity has formation as a premise, symmetry exchanges endpoints, and transitivity composes the two induction hypotheses. The corrected system has no MD-QT-CSP case.

Prove both orientations simultaneously by induction on the displayed type-equivalence derivation. In MD-QT-Code, the conclusion has the required head and its premise is the required body equality. In reflexivity, the additional body-formation hypothesis supplies body reflexivity at $A\alpha$. Symmetry exchanges the two induction statements.

For transitivity in the first orientation, the first induction hypothesis writes the middle type as ${▹}_{\alpha }\tau$ and gives $\rho \equiv \tau$ at $A\alpha$. Regularity of that equality supplies the formation premise needed by the second induction hypothesis. The second hypothesis writes the final type as ${▹}_{\alpha }\upsilon$ and gives $\tau \equiv \upsilon$; transitivity at $A\alpha$ completes the case. The reverse orientation exchanges the two induction statements. The Pi, application, and stage-quantifier congruences cannot have a code constructor on the displayed side. These are every type-equivalence rule in the corrected system.

The published proof’s simultaneous-inversion architecture motivates this induction , but its exact signature also has MD-QT-CSP. That missing case is not imported: at a code head it gives the noncommutative stage-order counterexample above. The explicit body-formation premise is necessary because published type-level CSP can form a code-headed type at a later word without furnishing code-formation inversion at that word. ◻

Proof. The source’s printed quotation-inversion premise uses $@A$; the quotation conclusion and MD-Quote force $@A\alpha$. We use that corrected stage annotation, which is also forced by the simultaneous inversion induction. Induct upward through trailing uses of MD-Conv. The first non-conversion rule is respectively MD-Quote or MD-Escape. In the quote case, regularity of the direct quote premise supplies the body-formation hypothesis of lemma 130.1; that lemma transports the body premise through every trailing type conversion and preserves the syntactic code head. In the escape case, retain the body type $\rho$ from MD-Escape. With no trailing conversion it is syntactically the conclusion type. Otherwise the trailing conversions compose to $\mathrm{\Gamma }⊢\rho \equiv \tau ::\ast @A\alpha$. These cases establish exactly the stated alternatives without assuming code-formation inversion for a type introduced only by published type-level CSP. ◻

Proof. Prove weakening, exchange, ordinary substitution, and stage substitution simultaneously for context well-formedness and the six judgment families. Context extension uses the type-kinding induction hypothesis for the declared type. In MD-Var, ordinary substitution uses the premise $\mathrm{\Gamma }⊢N:\xi @B$ when the selected variable is $x$, and otherwise rebuilds membership in the substituted context. The variable case of stage substitution changes both the declaration and its exact stage annotation.

For MD-Kind-Pi, MD-Pi, MD-Abs, and every dependent congruence, alpha-rename the term binder away from $N$, apply the induction hypotheses to the domain and binder-extended premise, and rebuild the rule. MD-TApp, MD-App, and MD-Q-App additionally use the structural composition law for dependent substitution in their result kind or type. The constructor rules for code, quotation, escape, and CSP apply the induction hypothesis at the premise stage and then rebuild the derived word-labelled rule determined by the substituted annotation.

For MD-TForall, MD-SAbs, MD-QT-Forall, and MD-Q-SAbs, alpha-rename the bound stage variable outside the free stage variables of the substituting word $D$ and the substituted expressions. The freshness premise is then preserved. Stage application substitutes in its result type as well as its term premise. Reflexivity, symmetry, and transitivity use the corresponding formation or equality induction hypotheses. The conversion rules MD-TConv and MD-Conv use, respectively, the simultaneously proved kind- and type-equivalence clauses; this is why a typing-only induction would be insufficient. Each computational equality axiom uses the typing clauses for its premises and the substitution composition law for its contractum. These cases exhaust context formation, kind formation, type kinding, term typing, and the three equivalence families.

Finally, prove the interaction equation by structural induction on $E$. Constructor cases commute componentwise. At a term or stage binder, rename the binder outside the free names of $N$, $N[D/\alpha ]$, and $D$, then use the induction hypothesis for the body. The resulting representatives differ only by those bound-name choices, which proves alpha-equivalence and the stated deterministic-representative corollary. ◻

Proof. Take a signature containing $$\mathsf{Nat}::\ast ,F::\mathrm{\Pi }n:\mathsf{Nat}.\ast ,c:\mathsf{Nat},$$ and put $$L=(\lambda z:\mathsf{Nat}.z)c,T=(\lambda x:\mathsf{Nat}.\lambda y:Fx.y)L.$$ Rules MD-TApp, MD-Abs, and MD-App derive $L:\mathsf{Nat}@\epsilon$ and $$T:(\mathrm{\Pi }y:FL.FL)@\epsilon .$$ Contracting the outer redex gives $$T⟶U=\lambda y:FL.y.$$ Reducing the argument first and then contracting the outer redex gives $$T⟶(\lambda x:\mathsf{Nat}.\lambda y:Fx.y)c⟶V=\lambda y:Fc.y.$$ Rule MD-Q-Beta, followed by MD-QT-App and dependent-product congruence, gives $\mathrm{\Pi }y:FL.FL\equiv \mathrm{\Pi }y:Fc.Fc::\ast @\epsilon$, so conversion types both arms at the original result type. The only redex in $U$ occurs inside its binder annotation. No displayed full context reaches it; hence $U$ and $V$ are distinct full normal forms. They have no common reduct. ◻

Proof. Induct on the reduction derivation. For full beta, invert trailing MD-Conv rules, then invert MD-App and MD-Abs. Ordinary substitution from lemma 130.3 types the contractum at the dependent result type; reapply the inverted conversions. Quote–escape inversion uses lemma 130.2: escape inversion produces a body type $\rho$, while quote inversion types the contractum at $\rho @A\alpha$. If $\rho$ is syntactically $\tau$, this is already the required judgment; otherwise escape inversion supplies $\mathrm{\Gamma }⊢\rho \equiv \tau ::\ast @A\alpha$, and MD-Conv gives it. Stage beta first inverts MD-SApp and MD-SAbs; stage substitution types $M[C/\alpha ]$ at $\tau [C/\alpha ]@A$, and alpha-renaming preserves the freshness premise.

For compatibility in the displayed full contexts beneath an ordinary abstraction, application, quotation, escape, stage abstraction, or stage application, apply the induction hypothesis to the selected premise and rebuild respectively MD-Abs, MD-App, MD-Quote, MD-Escape, MD-SAbs, or MD-SApp. The quotation case changes the premise stage to $A\alpha$; the escape case changes it back to $A$. A step beneath CSP is typed by the induction hypothesis at $A$ and rebuilt by MD-CSP at $A\alpha$. A trailing MD-Conv reuses its unchanged type-equivalence premise after applying the induction hypothesis to the term premise. These are every compatible term constructor and conversion. There is no compatibility case for a binder annotation or another type expression. Each staged evaluation context selects one of these cases, so the staged assertion follows from the same derivation. ◻

Proof. Prove erasure of kinding, typing, and the three equivalence judgments simultaneously. Kind and type constants use their erased signature entries. Dependent product formation, ordinary abstraction, and ordinary application become the simple arrow rules. Erasure commutes with dependent result substitution: $$(\sigma [N/x]{)}^{\mathrm{♮}}={\sigma }^{\mathrm{♮}}.$$ Code, quotation, escape, stage abstraction/application, and CSP erase to their premises. Conversion uses the simultaneous assertion $$\tau \equiv \sigma ⟹{\tau }^{\mathrm{♮}}={\sigma }^{\mathrm{♮}}.$$ Constructor congruences preserve that equality, and each computational equality has identical erasure or one simple beta equality. Reflexivity, symmetry, and transitivity preserve it. These cases cover every retained rule; the corrected system has no MD-QT-CSP case.

For reduction, ordinary beta uses $(M[N/x]{)}^{\mathrm{♮}}=M^{\mathrm{♮}}[N^{\mathrm{♮}}/x]$, proved by structural induction on $M$, and contracts the erased beta redex. Stage substitution changes only stage annotations and their derived staging nodes; erasure deletes both, so stage beta has equal erasures. Quote and escape are both erased, so splice also has equal erasures. An induction on the full-context derivation transports the corresponding beta sequence or syntactic equality through the erased context. These are all three root contractions and every term-only compatibility family. The qualification is essential: a hypothetical beta step inside a type annotation would erase to equality, as proposition 130.4 demonstrates. ◻

Proof. By lemma 130.6, $M^{\mathrm{♮}}$ is simply typed. An ordinary beta step gives a nonempty target beta reduction; splice and stage beta leave the translation equal. Let $s(M)$ count stage-abstraction and stage-application nodes, and let $q(M)$ count quotation and escape nodes. Order $(s(M),q(M))$ lexicographically. A stage-beta contraction strictly decreases the first component. It may expand derived word-labelled quotation, escape, or CSP notation, but it cannot change the first component; quote and escape expansion may increase the second. A splice preserves the first component and strictly decreases the second. Stage substitution introduces no stage abstraction or stage-application node. Ordinary beta may increase both components, but an infinite source reduction with infinitely many ordinary-beta steps would give an infinite simply typed beta reduction. If it had only finitely many, its tail would strictly decrease the displayed lexicographic pair at every step, also impossible. This lexicographic argument repairs the published proof’s insufficient raw-size sentence. Only strong normalization of the simply typed target is imported; the source-to-target simulation is the local lemma above. Classifying constant-headed spines as final forms does not add a full-reduction step. ◻

Proof. Prove the two assertions simultaneously by induction on the displayed word-parallel derivation. Alpha-rename term and stage binders outside the free names of the substituting expression or word before applying an induction hypothesis. At an ordinary-beta root, let $y$ be its term binder and let $a,a^{\prime }$ be its annotation-free argument endpoints. Ordinary beta uses the ordinary-substitution assertion twice and the substitution-composition equation. After alpha-renaming $y\ne x$ outside the free variables of $v$, the decisive equation is $$u^{\prime }[a^{\prime }/y][v^{\prime }/x]{\equiv }_{\alpha }{u}^{\prime }[v^{\prime }/x][a^{\prime }[v^{\prime }/x]/y].$$ At a stage-beta root, let $D$ be its finite stage-word argument. Stage beta uses the stage-substitution assertion on its body. After renaming the bound stage variable $\delta$ outside $C$, its composition equation is $$u^{\prime }[D/\delta ][C/\alpha ]{\equiv }_{\alpha }{u}^{\prime }[C/\alpha ][D[C/\alpha ]/\delta ].$$

For a word-splice root with shell word $B$, ordinary substitution leaves the shell unchanged and the body induction hypothesis supplies the premise of the same root rule. Stage substitution changes its shell word to $B[C/\alpha ]$. If this word is nonempty, apply the word-splice rule to the body induction hypothesis. If it is empty, both shells erase by definition and that induction hypothesis is already the required conclusion. A primitive quotation, escape, or CSP congruence whose label is $\alpha$ expands to a shell indexed by $C$; induction on the length of $C$ rebuilds the required single congruence derivation. The other constructor congruences rebuild directly. These cases exhaust the three root rules and the seven congruence schemas. ◻

Proof. Define the complete development $u^{\star }$ recursively. A term has at most one outer word-splice shell: reading its consecutive outer escape labels and then the immediately following quotation labels determines the nonempty word $B$. At that shell and at the other two root-redex shapes set and otherwise rebuild the outer constructor from the complete developments of its term children.

First prove $u{\Rightarrow }_w{u}^{\star }$ by structural induction. At a root redex, apply the corresponding word-parallel root rule to the induction hypotheses for its term children. Otherwise apply congruence. Next induct on $u{\Rightarrow }_{w}v$. The root cases use lemma 130.8; the word-splice case uses the induction hypothesis for its body. A congruence derivation either rebuilds a nonredex constructor or retains one of the three root shapes. Ordinary beta and stage beta then use their root rules on the induction hypotheses for the children.

The remaining overlap is a congruence derivation from an outer shell ${\mathsf{e}}_B({\mathsf{q}}_B(u))$. A congruence derivation cannot contract the outermost escape. Induction on $|B|$ therefore gives exactly two possibilities. Either every shell constructor remains, or an inner word-splice step removes a prefix of $B$. In both cases the reduct has the form $${\mathsf{e}}_C({\mathsf{q}}_C(v)),C\ne \epsilon ,u{\Rightarrow }_{w}v,$$ where $C$ is respectively $B$ or the unique nonempty suffix left after the contracted prefix. For $B=\beta \gamma$, contracting the inner $\beta$-shell leaves ${\mathsf{e}}_{\gamma }({\mathsf{q}}_{\gamma }(v))$. The induction hypothesis gives $v{\Rightarrow }_w{u}^{\star }$, and the word-splice root rule sends the retained $C$-shell to $u^{\star }$ in one step. This treats the congruence-versus-generalized-root overlap. Thus the induction proves the triangle property $$u{\Rightarrow }_{w}v⟹v{\Rightarrow }_w{u}^{\star }.$$ Both reducts in the statement therefore reduce to $u^{\star }$. ◻

Proof. Every ${⟶}_{\mathrm{a}}$ step is a word-parallel step. Conversely, induction on a word-parallel derivation expands it to ${{⟶}_{\mathrm{a}}}^{\ast }$: congruence interleaves the finite child sequences; ordinary and stage beta contribute one root contraction after the child sequences; and a word-splice root indexed by $B$ contributes exactly $|B|$ primitive splice contractions after the body sequence. By lemma 130.9, the word-parallel relation has the diamond property. The two inclusions imply $$({⟶}_{\mathrm{a}}{)}^{\ast }=({\Rightarrow }_w{)}^{\ast }.$$ Induction on the length of one word-parallel path, with an inner induction that moves its first step across the other path one diamond at a time, proves confluence of its reflexive-transitive closure. The displayed equality therefore gives confluence of ${⟶}_{\mathrm{a}}$. ◻

Proof. Structural induction on terms and on the displayed full contexts gives both directions needed for lifting: For ordinary beta these statements use $\lfloor P[Q/x]{\rfloor }_{\mathrm{a}}=\lfloor P{\rfloor }_{\mathrm{a}}[\lfloor Q{\rfloor }_{\mathrm{a}}/x]$; for stage beta they use the exact equation $$\lfloor P[B/\alpha ]{\rfloor }_{\mathrm{a}}=\lfloor P{\rfloor }_{\mathrm{a}}[B/\alpha ],$$ where $B$ is the substituted stage word. Splice is homomorphic. No annotation case occurs because neither relation reduces there.

Project the two reductions from $M$ to the annotation-free relation. By proposition 130.10, their erasures have a common target $u$. Lift the two joining sequences back one step at a time. The lifted endpoints are the required $N^{\prime }$ and $N^{″}$. The counterpeak of proposition 130.4 shows why the conclusion cannot in general be strengthened to $N^{\prime }=N^{″}$. ◻

Proof. Apply theorem 130.11. Normality makes both joining sequences empty, so the theorem’s final annotation-free terms are equal. ◻

Proof. Prove both orientations simultaneously by induction on the type-equivalence derivation. Rules MD-QT-Pi, MD-QT-Code, and MD-QT-Forall preserve the displayed outer constructor, and MD-QT-Refl preserves it syntactically. Rule MD-QT-App has a type application at both endpoints, so none of the three hypotheses can hold in that case. Symmetry exchanges the two induction statements. In a transitivity derivation, the first induction hypothesis gives the same head for the middle type and the second gives that head for the final type. The inversion-stable fragment has no MD-QT-CSP case. These are all type-equivalence rules. ◻

Proof. Inspect the four productions of $v^{\epsilon }$. A neutral constant-headed spine gives the stated neutral alternative. In the other three productions, invert trailing uses of MD-Conv. The first non-conversion rule is respectively MD-Abs, MD-Quote, or MD-SAbs, so its result type is headed respectively by $\mathrm{\Pi }$, ${▹}_{\beta }$, or $\mathrm{\forall }$. Every trailing conversion preserves that head by lemma 130.13; in the code case it also preserves $\beta$. Hence exactly the production named in each clause can remain besides the neutral alternative. The empty-stage context hypothesis excludes a variable head through the exact-stage premise of MD-Var. ◻

Proof. Induct on the final typing rule. The induction hypothesis includes uniqueness for each premise to which staged evaluation descends.

For MD-Const, the term belongs to $h^A$. In MD-Var, the exact stage premise contradicts the context hypothesis when $A=\epsilon$; at a nonempty stage the variable belongs to $h^A$.

For MD-Abs, an abstraction at $\epsilon$ is a value because its body is not selected there. At a nonempty stage, apply the induction hypothesis to the body under $\mathrm{\Gamma },x:\tau @A$. The added declaration is not at $\epsilon$. A body value gives the abstraction-value production; a body decomposition is lifted by the unique $\lambda x:\tau .E_D^A$ context production.

For MD-App, first apply the induction hypothesis to the function. Its decomposition lifts uniquely to $E_D^{A}N$. If the function is a value, apply the induction hypothesis to the argument; its decomposition lifts uniquely to $v^A{E}_D^A$. If both are values and $A\ne \epsilon$, the production $v^A{v}^A$ makes the whole application a value. If $A=\epsilon$, the function has dependent-product type, so clause 1 of lemma 130.14 leaves two cases. A lambda head gives the unique ordinary-beta redex; a head in $h^{\epsilon }$ extends uniquely to the final spine $h^{\epsilon }{v}^{\epsilon }$. Quotation and stage- abstraction heads are excluded by the cited lemma.