Erasure and Execution of Dependent Definitions

Definition 126.1 — The Timpl-erasure system card¶

The source is the full Timpl signature of convention 110.16, extended by the accepted datatype and recursive declarations of chapter 122, chapter 123 together with the relevance annotation of definition 126.9. Neither definition 122.1 nor definition 123.1 carries relevance marks, so the annotation is extra data supplied with an already accepted declaration; it is checked by the judgment in definition 126.3, and no QTT grade or starred modality is assumed. Accepted source annotations are rechecked by the kernel-soundness theorem theorem 48.19; erasure does not replace that source judgment.

The target Texec is the untyped call-by-value calculus A constructor tag records its runtime arity. A closure records a recursive function tag and the runtime part of its environment. Values are $$w::=\lambda x.t\mid C_k(w_1,\dots ,w_n)\mid \mathsf{clos}(f,\overrightarrow{w}).$$ Every target case has pairwise distinct branch tags. Erasure obtains one branch per constructor from an accepted source case; raw case lists with a duplicate tag are not Texec phrases. This side condition makes branch selection functional. Write ${\delta }_t(f)=(\overrightarrow{y};\overrightarrow{x};t_f)$ for the compiled recursive tag $f$, with captured environment $\overrightarrow{y}$ and formal parameters $\overrightarrow{x}$. Each occurrence of a primitive natural-number or vector eliminator also receives a fresh recursive tag. The tag records the occurrence, its ordered runtime free variables, and the relevance marks on its branch binders. Thus primitive eliminators add no target syntax: they compile to the same $\mathsf{clos}/\mathsf{call}$ forms as user declarations. Their exact tag bodies are given with the erasure equations in definition 126.10. Evaluation is the deterministic left-to-right call-by-value relation $t\Downarrow w$ generated by $$\frac{\phantom{X}}{w\Downarrow w}\mathrm{E}-\mathrm{Val}\frac{\begin{array}{c}{t}_1\Downarrow \lambda x.t\\ t_2\Downarrow w_2\\ t[w_2/x]\Downarrow w\end{array}}{t_1{t}_2\Downarrow w}\mathrm{E}-\mathrm{App}$$ $$\frac{(t_i\Downarrow w_i{)}_{1\le i\le n}}{C_k(t_1,\dots ,t_n)\Downarrow C_k(w_1,\dots ,w_n)}\mathrm{E}-\mathrm{Con}\frac{(t_i\Downarrow w_i{)}_i}{\mathsf{clos}(f,\overrightarrow{t})\Downarrow \mathsf{clos}(f,\overrightarrow{w})}\mathrm{E}-\mathrm{Clos}$$ $$\frac{\begin{array}{c}t\Downarrow C_k(\overrightarrow{w})\\ t_k[\overrightarrow{w}/{\overrightarrow{x}}_k]\Downarrow w\end{array}}{\mathsf{case}t\mathsf{of}\{C_j({\overrightarrow{x}}_j)\Rightarrow t_j{\}}_j\Downarrow w}\mathrm{E}-\mathrm{Case}$$ $$\frac{\begin{array}{c}{\delta }_t(f)=(\overrightarrow{y};\overrightarrow{x};t_f)\\ t\Downarrow \mathsf{clos}(f,\overrightarrow{w})\\ (t_i\Downarrow w_i{)}_{1\le i\le n}\\ t_f[\overrightarrow{w}/\overrightarrow{y}][{\overrightarrow{w}}_i/\overrightarrow{x}]\Downarrow w\end{array}}{\mathsf{call}(t,t_1,\dots ,t_n)\Downarrow w}\mathrm{E}-\mathrm{Call}$$ There is no rule for a case whose scrutinee is a lambda or a closure, none for an application whose head is a constructor block, and none for a $\mathsf{call}$ whose head is not a closure or whose argument count differs from $|\overrightarrow{x}|$; a term that reaches such a configuration is stuck. Representation well-formedness rules out malformed stored arities, but it does not by itself prove that an arbitrary target application reaches a lambda or that an arbitrary case reaches a block. For a source term equipped with an evaluation derivation, theorem 126.14 constructs the matching target derivation and thereby rules out those dynamic failures.

The observation on closed terminating Timpl data is the constructor tree with erased fields removed. The theorem below proves target well-formedness, a constructor/closure representation invariant, and forward simulation. Since Texec is untyped, no target type-preservation claim is made.

Definition 126.3 — Runtime relevance¶

Fix an environment marking each source variable $x^{\varrho }:A$, with $\varrho \in \{\mathsf{runtime},\mathsf{erased}\}$. The runtime source phrases used by this chapter are Here $I_C$ is the raw natural-number eliminator of definition 28.21. Its displayed branch is a checked eta-long branch; the successor branch of $\mathsf{vind}$ is treated the same way. Eta expansion preserves source typing and judgmental equality by Timpl’s $\mathrm{\Pi }$-eta rule. This erasure card chooses the checked eta-long representative, and the source term $e$ in the simulation theorem below is that representative; no operational equation for a different surface spelling is assumed. The grammar therefore covers every term former in convention 110.16: universes, lifts, and type expressions occur in annotations, motives, and opaque erased argument slots and are static premises, while the remaining term constructors occur explicitly above. The generic constructor and case forms cover accepted user datatypes. The primitive constructors of $\mathbf{1},\mathbf{2},\mathbb{N}$, and $\mathsf{Vec}$ use the fixed annotations below; their primitive eliminators use the four displayed forms. Formally, let $a^{\mathsf{s}}$ range over any checked raw Timpl term. An application argument, constructor field, call capture, or call input whose declaration mark is erased is an opaque $a^{\mathsf{s}}$ slot rather than a recursive $e$ slot. In particular, a type argument may occupy an erased application or call slot without becoming a runtime phrase. Other premises concluded by Rel-Erased remain the explicit syntax shown in their rule: for example, S-J evaluates its proof to expose reflexivity even though the target deletes that proof. Thus target deletion does not by itself mean that every erased source premise is unevaluated.

The last form is a saturated call to a declaration in an accepted first-order Timpl-rec group; $\overrightarrow{y}$ is its captured environment. Unsaturated or first-class uses of a recursive declaration are outside this erasure card.

There are two judgments $\mathrm{\Gamma }⊢e\mathsf{runtime}$ and $\mathrm{\Gamma }⊢e\mathsf{erased}$. The second means that the whole phrase occupies a static position and is deleted. It is generated by source typing: $$\frac{\mathrm{\Gamma }⊢e:A}{\mathrm{\Gamma }⊢e\mathsf{erased}}\mathrm{Rel}-\mathrm{Erased}.$$ The runtime rules are $$\frac{x^{\mathsf{runtime}}:A\in \mathrm{\Gamma }}{\mathrm{\Gamma }⊢x\mathsf{runtime}}\mathrm{Rel}-\mathrm{Var}\frac{\mathrm{\Gamma },x^{\mathsf{runtime}}:A⊢b\mathsf{runtime}}{\mathrm{\Gamma }⊢{\lambda }^{ϵ,\mathsf{runtime}}(x:A).b\mathsf{runtime}}\mathrm{Rel}-\mathrm{Lam}-\mathrm{R}$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢f\mathsf{runtime}\\ \mathrm{\Gamma }⊢a\mathsf{runtime}\end{array}}{\mathrm{\Gamma }⊢f{}^{ϵ,\mathsf{runtime}}a\mathsf{runtime}}\mathrm{Rel}-\mathrm{App}-\mathrm{R}.$$ $$\frac{\begin{array}{c}\mathrm{\Gamma },x^{\mathsf{erased}}:A⊢b\mathsf{runtime}\\ \mathrm{\Gamma }⊢a\mathsf{erased}\end{array}}{\mathrm{\Gamma }⊢{\lambda }^{{ϵ}^{\prime },\mathsf{erased}}(x:A).b{}^{ϵ,\mathsf{erased}}a\mathsf{runtime}}\mathrm{Rel}-\mathrm{App}-\mathrm{E}.$$ Thus this exact fragment accepts erased application only as an administrative redex with its erased abstraction visible. A surface elaborator may expose such a redex when a closed head normalizes to an erased abstraction, but that preprocessing theorem is not part of Timpl-erasure; an application of a variable at an erased domain is rejected by this card. Dependent pairs and their projections retain both components: $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢a\mathsf{runtime}\\ \mathrm{\Gamma }⊢b\mathsf{runtime}\end{array}}{\mathrm{\Gamma }⊢(a,b)\mathsf{runtime}}\mathrm{Rel}-\mathrm{Pair}.$$ $$\frac{\mathrm{\Gamma }⊢s\mathsf{runtime}}{\mathrm{\Gamma }⊢{\mathsf{pr}}_1(s)\mathsf{runtime}}\mathrm{Rel}-\mathrm{Fst}\frac{\mathrm{\Gamma }⊢s\mathsf{runtime}}{\mathrm{\Gamma }⊢{\mathsf{pr}}_2(s)\mathsf{runtime}}\mathrm{Rel}-\mathrm{Snd}.$$ The proof constructor has a target tag when a proof is retained inside a runtime pair or user constructor: $$\frac{\mathrm{\Gamma }⊢a:A}{\mathrm{\Gamma }⊢{\mathsf{refl}}_a\mathsf{runtime}}\mathrm{Rel}-\mathrm{Refl}.$$ If the accepted constructor annotation is $c:(x_1^{{\kappa }_1}:A_1)\cdots (x_n^{{\kappa }_n}:A_n)\to D\overrightarrow{p}\overrightarrow{ı}$, where ${\kappa }_i$ is the constructor-field retention mark, then $$\frac{(\mathrm{\Gamma }⊢a_i{\kappa }_i{)}_{1\le i\le n}}{\mathrm{\Gamma }⊢c(\overrightarrow{a})\mathsf{runtime}}\mathrm{Rel}-\mathrm{Con}.$$ For a constructor case, give the variables of branch $k$ independent branch-use marks ${\overrightarrow{\varrho }}_k$, and write ${\overrightarrow{x}}_k^{{\overrightarrow{\varrho }}_k}$ for the resulting branch context. If the field-retention vector of $c_k$ is ${\overrightarrow{\kappa }}_k$, admissibility requires $${\varrho }_{k,i}=\mathsf{runtime}⟹{\kappa }_{k,i}=\mathsf{runtime}.$$ The converse is not required: a retained constructor field may be ignored by the branch body. Then $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢e\mathsf{runtime}\\ (\mathrm{\Gamma },{\overrightarrow{x}}_k^{{\overrightarrow{\varrho }}_k}⊢e_k\mathsf{runtime}{)}_k\end{array}}{\mathrm{\Gamma }⊢\mathsf{case}e\mathsf{of}\{c_k({\overrightarrow{x}}_k)\Rightarrow e_k{\}}_k\mathsf{runtime}}\mathrm{Rel}-\mathrm{Case}.$$ Motives, index equations, and inaccessible patterns belong to the Rel-Erased premises of the source typing derivation and produce no target phrase. Finally, if the checked source declaration record is $${\delta }_s(f)=({\overrightarrow{y}}^{\overrightarrow{\sigma }};{\overrightarrow{x}}^{\overrightarrow{\varrho }};b_f),$$ then $$\frac{\begin{array}{c}(\mathrm{\Gamma }⊢y_j{\sigma }_j{)}_j\\ (\mathrm{\Gamma }⊢a_i{\varrho }_i{)}_i\\ {\overrightarrow{y}}^{\overrightarrow{\sigma }},{\overrightarrow{x}}^{\overrightarrow{\varrho }}⊢b_f\mathsf{runtime}\end{array}}{\mathrm{\Gamma }⊢f⟨\overrightarrow{y}⟩(\overrightarrow{a})\mathsf{runtime}}\mathrm{Rel}-\mathrm{Call}.$$

The four primitive eliminators have separate rules. Their omitted formation premises are exactly their Timpl typing rules and are not replaced by the relevance judgment: $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢b\mathsf{runtime}\\ \mathrm{\Gamma }⊢e_t\mathsf{runtime}\\ \mathrm{\Gamma }⊢e_f\mathsf{runtime}\end{array}}{\mathrm{\Gamma }⊢{\mathsf{ind}}_{\mathbf{2}}(x.C;e_t,e_f,b)\mathsf{runtime}}\mathrm{Rel}-\mathrm{Bool}-\mathrm{Elim}.$$ $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢e_0\mathsf{runtime}\\ \mathrm{\Gamma },n^{{\varrho }_n}:\mathbb{N},r^{{\varrho }_r}:C(n)⊢e_s\mathsf{runtime}\\ \mathrm{\Gamma }⊢m\mathsf{runtime}\end{array}}{\mathrm{\Gamma }⊢I_C(e_0;n^{{\varrho }_n}.r^{{\varrho }_r}.e_s;m)\mathsf{runtime}}\mathrm{Rel}-\mathrm{Nat}-\mathrm{Elim}.$$ The predecessor stored by $C_{\mathsf{suc}}$ is runtime even when the branch mark ${\varrho }_n$ is erased: the recursive closure needs it to make its next call. The branch mark controls only whether $e_s$ may use that predecessor. For identity elimination, the proof and motive are static, but the reflexive endpoint is retained exactly when the reflexive branch uses it: $$\frac{\begin{array}{c}\mathrm{\Gamma },z^{{\varrho }_z}:A⊢e_r\mathsf{runtime}\\ \mathrm{\Gamma }⊢a{\varrho }_z\\ \mathrm{\Gamma }⊢e_q\mathsf{erased}\end{array}}{\mathrm{\Gamma }⊢{\mathsf{J}}_{A;a;b}(x.y.p.C;z^{{\varrho }_z}.e_r;e_q)\mathsf{runtime}}\mathrm{Rel}-\mathrm{J}.$$ The annotations $A,a,b,C$ are the raw annotations of definition 30.1; in particular, $a$ is not guessed from the proof. Finally, abbreviate the successor-branch context by $${\mathrm{\Delta }}_s:=\mathrm{\Gamma },n^{{\varrho }_n}:\mathbb{N},a^{{\varrho }_a}:A,x{s}^{\mathsf{runtime}}:\mathsf{Vec}(A,n),r^{{\varrho }_r}:P(n,xs).$$ Then $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢e_0\mathsf{runtime}\\ {\mathrm{\Delta }}_s⊢e_s\mathsf{runtime}\\ \mathrm{\Gamma }⊢m{\varrho }_m\\ \mathrm{\Gamma }⊢ys\mathsf{runtime}\end{array}}{\mathrm{\Gamma }⊢\mathsf{vind}(P;e_0;n^{{\varrho }_n}.a^{{\varrho }_a}.xs.r^{{\varrho }_r}.e_s;m,ys)\mathsf{runtime}}\mathrm{Rel}-\mathrm{Vec}-\mathrm{Elim}.$$ If ${\varrho }_m=\mathsf{runtime}$, admissibility also requires the predecessor field of $\mathsf{vcons}$ to be runtime, because the recursive target call then receives that predecessor as its runtime index. The structural field $xs$ is runtime in every admissible annotation. More generally, a runtime-marked branch variable may name only a runtime constructor field; an erased branch variable may name a retained field and simply leave it unused.

Thus an erased variable can occur only below a premise concluded by Rel-Erased; recursive closures capture exactly the runtime variables listed in $\overrightarrow{y}$. An accepted source declaration is erasable when its checked Timpl term satisfies this judgment.

Definition 126.5 — Source call-by-value evaluation¶

Write $e\Downarrow v$ for the source evaluation relation used by this chapter. Texec uses the same evaluation glyph in definition 126.1; the disjoint source and target grammars determine which rule card applies, and no derivation mixes their rules. Source values are lambdas under either relevance mark, pairs of values, reflexivity values, and primitive or declared constructors whose runtime fields are values and whose erased fields remain as checked static source terms. Call the pairs, reflexivity values, and primitive or declared constructor values the source data values. An erased abstraction may be an intermediate source value, but Rel-App-E admits it in a runtime term only at a visible administrative redex; hence it has no final target value-representation clause. If a source argument $a_i$ has mark ${\varrho }_i$, write ${\hat{a}}_i$ for the runtime value $v_i$ when ${\varrho }_i=\mathsf{runtime}$ and $a_i\Downarrow v_i$, and write ${\hat{a}}_i=a_i$ without an evaluation premise when ${\varrho }_i=\mathsf{erased}$. Thus erased type arguments are well-typed static syntax, not source runtime phrases. If ${\delta }_s(f)=({\overrightarrow{y}}^{\overrightarrow{\sigma }};{\overrightarrow{x}}^{\overrightarrow{\varrho }};b_f)$ is a checked source declaration, the rules are as follows.

On values, annotated applications, pairs, projections, constructors, cases, and the four primitive eliminators, this card is exactly the optional implementation relation ${\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}$ of definition 124.2, after the uniform renaming $T-\ast \mapsto S-\ast$ and ${\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}\mapsto \Downarrow$. The only rule added here is S-Call for a checked recursive declaration record ${\delta }_s$. Thus the two cards do not choose different call-by-value orders on their common grammar.

Values and functions use $$\frac{\phantom{X}}{v\Downarrow v}\mathrm{S}-\mathrm{Val}$$ $$\frac{\begin{array}{c}f\Downarrow {\lambda }^{ϵ,\mathsf{runtime}}(x:A).b\\ a\Downarrow v_a\\ b[v_a/x]\Downarrow v\end{array}}{f{}^{ϵ,\mathsf{runtime}}a\Downarrow v}\mathrm{S}-\mathrm{App}-\mathrm{R}$$ $$\frac{\begin{array}{c}f\Downarrow {\lambda }^{ϵ,\mathsf{erased}}(x:A).b\\ b[a/x]\Downarrow v\end{array}}{f{}^{ϵ,\mathsf{erased}}a\Downarrow v}\mathrm{S}-\mathrm{App}-\mathrm{E}.$$ The erased rule substitutes its checked static argument but does not evaluate it. Pairing and projection use $$\frac{\begin{array}{c}a\Downarrow v_a\\ b\Downarrow v_b\end{array}}{(a,b)\Downarrow (v_a,v_b)}\mathrm{S}-\mathrm{Pair}\frac{s\Downarrow (v_a,v_b)}{{\mathsf{pr}}_1(s)\Downarrow v_a}\mathrm{S}-\mathrm{Fst}\frac{s\Downarrow (v_a,v_b)}{{\mathsf{pr}}_2(s)\Downarrow v_b}\mathrm{S}-\mathrm{Snd}.$$ For every primitive or declared constructor and every accepted datatype case, $$\frac{(a_i\Downarrow v_i{)}_{{\kappa }_i=\mathsf{runtime}}}{c(a_1,\dots ,a_n)\Downarrow c({\hat{a}}_1,\dots ,{\hat{a}}_n)}\mathrm{S}-\mathrm{Con}$$ $$\frac{\begin{array}{c}e\Downarrow c_k(\hat{\overrightarrow{a}})\\ e_k[\hat{\overrightarrow{a}}/{\overrightarrow{x}}_k]\Downarrow v\end{array}}{\mathsf{case}e\mathsf{of}\{c_j({\overrightarrow{x}}_j)\Rightarrow e_j{\}}_j\Downarrow v}\mathrm{S}-\mathrm{Case}.$$ The Boolean rules are the two instances $$\frac{\begin{array}{c}b\Downarrow \mathsf{tt}\\ e_t\Downarrow v\end{array}}{{\mathsf{ind}}_{\mathbf{2}}(x.C;e_t,e_f,b)\Downarrow v}\mathrm{S}-\mathrm{Bool}-\mathrm{T}\frac{\begin{array}{c}b\Downarrow \mathsf{ff}\\ e_f\Downarrow v\end{array}}{{\mathsf{ind}}_{\mathbf{2}}(x.C;e_t,e_f,b)\Downarrow v}\mathrm{S}-\mathrm{Bool}-\mathrm{F}.$$ For the next two rules, abbreviate $$N_C(e_0,e_s;m):=I_C(e_0;n^{{\varrho }_n}.r^{{\varrho }_r}.e_s;m).$$ Natural-number elimination is generated by $$\frac{\begin{array}{c}m\Downarrow \mathsf{0}\\ e_0\Downarrow v\end{array}}{N_C(e_0,e_s;m)\Downarrow v}\mathrm{S}-\mathrm{Nat}-\mathrm{Z}$$ $$\frac{\begin{array}{c}m\Downarrow \mathsf{suc}(v_n)\\ N_C(e_0,e_s;v_n)\Downarrow v_r\\ e_s[v_n/n,v_r/r]\Downarrow v\end{array}}{N_C(e_0,e_s;m)\Downarrow v}\mathrm{S}-\mathrm{Nat}-\mathrm{S}.$$ The identity rule evaluates the proof to the only constructor that exposes a root computation: $$\frac{\begin{array}{c}{e}_q\Downarrow {\mathsf{refl}}_{v_q}\\ e_r[a/z]\Downarrow v\end{array}}{{\mathsf{J}}_{A;a;b}(x.y.p.C;z^{{\varrho }_z}.e_r;e_q)\Downarrow v}\mathrm{S}-\mathrm{J}.$$ Vector elimination has its two indexed rules: $$\frac{\begin{array}{c}m\Downarrow \mathsf{0}\\ ys\Downarrow \mathsf{vnil}\\ e_0\Downarrow v\end{array}}{\mathsf{vind}(P;e_0;n^{{\varrho }_n}.a^{{\varrho }_a}.xs.r^{{\varrho }_r}.e_s;m,ys)\Downarrow v}\mathrm{S}-\mathrm{Vec}-\mathrm{Nil}$$ $$\frac{\begin{array}{c}m\Downarrow \mathsf{suc}(v_n)\\ ys\Downarrow \mathsf{vcons}(v_n,v_a,v_{xs})\\ \mathsf{vind}(P;e_0;n^{{\varrho }_n}.a^{{\varrho }_a}.xs.r^{{\varrho }_r}.e_s;v_n,v_{xs})\Downarrow v_r\\ e_s[v_n/n,v_a/a,v_{xs}/xs,v_r/r]\Downarrow v\end{array}}{\mathsf{vind}(P;e_0;n^{{\varrho }_n}.a^{{\varrho }_a}.xs.r^{{\varrho }_r}.e_s;m,ys)\Downarrow v}\mathrm{S}-\mathrm{Vec}-\mathrm{Cons}.$$ Finally, saturated user recursion evaluates only its runtime captures and inputs; erased captures and inputs are substituted as checked static syntax: $$\frac{\begin{array}{c}(y_j\Downarrow u_j{)}_{{\sigma }_j=\mathsf{runtime}}\\ (a_i\Downarrow v_i{)}_{{\varrho }_i=\mathsf{runtime}}\\ b_f[\hat{\overrightarrow{y}}/\overrightarrow{y},\hat{\overrightarrow{a}}/\overrightarrow{x}]\Downarrow v\\ {\delta }_s(f)=({\overrightarrow{y}}^{\overrightarrow{\sigma }};{\overrightarrow{x}}^{\overrightarrow{\varrho }};b_f)\end{array}}{f⟨\overrightarrow{y}⟩(\overrightarrow{a})\Downarrow v}\mathrm{S}-\mathrm{Call}.$$ There is no rule for a neutral scrutinee, a mismatched constructor, or a call with the wrong arity. Hence the relation is partial on raw closed syntax; the theorem below assumes an evaluation derivation rather than inferring termination from typing.

Definition 126.9 — Relevance annotation of an accepted declaration¶

Let $\mathcal{B}$ be a block accepted by definition 122.1 and $\mathcal{G}$ a group accepted by definition 123.1. A relevance annotation of the pair assigns one $\varrho \in \{\mathsf{runtime},\mathsf{erased}\}$ to every constructor field of every ${\mathrm{\Theta }}_s$, to every binder of every input telescope ${\mathrm{\Delta }}_i$, to every binder introduced by a clause split of $\mathcal{G}$, and to the branch binders of each primitive natural-number, identity, or vector eliminator occurrence. The primitive constructors use the same convention: $\mathsf{suc}$’s predecessor and $\mathsf{vcons}$’s recursive vector field are runtime. Write ${\kappa }_n,{\kappa }_a$ for the chosen constructor-field marks on $\mathsf{vcons}$’s predecessor and element fields, respectively; these are distinct from the branch-use marks ${\varrho }_n,{\varrho }_a$. It is admissible when

1. every type-valued binder—a binder whose declared type is judgmentally a universe—is marked erased;

2. every position at which the accepted clause matrices split is marked runtime;

3. every argument named by an accepted structural or lexicographic certificate of definition 123.1 is marked runtime; and

4. for a primitive vector branch, ${\varrho }_n=\mathsf{runtime}$ implies ${\kappa }_n=\mathsf{runtime}$, and ${\varrho }_a=\mathsf{runtime}$ implies ${\kappa }_a=\mathsf{runtime}$; and

5. for every user-constructor branch binder, ${\varrho }_{k,i}=\mathsf{runtime}$ implies ${\kappa }_{k,i}=\mathsf{runtime}$; and

6. the runtime arity recorded for a target constructor tag $C_c$ is the number of runtime fields of $c$, taken in source order.

For a vector eliminator whose index $m$ is runtime, ${\kappa }_n=\mathsf{runtime}$ as well. Every type-valued argument is erased: Texec has no representation for a universe or a source type expression. A data-valued index, such as a natural-number length, may instead be marked runtime when the source runtime grammar and the target representation contain its value forms. Subject to these constraints, the remaining annotation is a choice, and definition 126.3 is the judgment that decides whether that choice survives deletion; the counterexample after it is the choice that does not.

Definition 126.10 — Erasure¶

For an erasable term $e$, write $|e|$ for its Texec erasure. The decisive clauses are Dependent pairs, projections, reflexivity, and the nonrecursive Boolean eliminator erase by Let list the runtime fields of a constructor. For a recursive input telescope $(x_1^{{\varrho }_1}:A_1),\dots ,(x_n^{{\varrho }_n}:A_n)$, define by ${\varrho }_{j_k}=\mathsf{runtime}$, in source order. The remaining clauses are Here $|\overrightarrow{y}|$ contains exactly those captures whose source marks are runtime, in declaration order, and the target pattern retains $x_{k,i}$ exactly when the corresponding constructor field has ${\kappa }_{k,i}=\mathsf{runtime}$. A retained field whose branch-use mark is erased therefore still contributes an unused target pattern binder; this is what makes the pattern arity equal to the target constructor arity. Types, motives, the proof argument of Rel-J, and every entire premise concluded by Rel-Erased produce no target phrase. A proof retained in a pair or a constructor is represented by $C_{\mathsf{refl}}$; erasure does not silently delete an unmarked $\mathrm{\Sigma }$-component.

It remains to give the exact recursive tags promised above. Erasure is defined on the checked annotated derivation, whose eliminator nodes carry stable occurrence identifiers and lexical capture slots. Substitution fills a slot with a target expression; it does not regenerate the tag or flatten that expression’s free variables. This convention is the one needed for the literal substitution equation below.

For an ordinary checked recursive declaration $${\delta }_s(f)=({\overrightarrow{y}}^{\overrightarrow{\sigma }};{\overrightarrow{x}}^{\overrightarrow{\varrho }};b_f)\text{with}{\overrightarrow{y}}^{\overrightarrow{\sigma }},{\overrightarrow{x}}^{\overrightarrow{\varrho }}⊢b_f\mathsf{runtime},$$ the compiler creates the target entry $${\delta }_t(f)=(\overrightarrow{y}{|}_{\overrightarrow{\sigma }=\mathsf{runtime}};\overrightarrow{x}{|}_{\overrightarrow{\varrho }=\mathsf{runtime}};|b_f|).$$ The relevance derivation proves that the free variables of $|b_f|$ are among precisely those two retained lists. Thus the closure emitted at a call stores the first list, the call supplies the second list, and E-Call substitutes the target values in source declaration order. This construction is applied simultaneously to every declaration of an accepted recursive group; a recursive occurrence in $|b_f|$ names the corresponding compiled tag rather than unfolding its body.

For a natural-number eliminator at occurrence $o$, put $t_0=|e_0|$, $t_s=|e_s|$, let $\overrightarrow{y}$ be its lexical runtime capture slots in source-context order, and choose the tag ${\nu }_N(o)$. Set $${\delta }_t({\nu }_N(o))=(\overrightarrow{y};m;\mathsf{case}m\mathsf{of}\{\begin{array}{l}{C}_{\mathsf{0}}\Rightarrow t_0,\\ C_{\mathsf{suc}}(n)\Rightarrow t_s^{\mathrm{♮}}.\end{array})$$ When ${\varrho }_r=\mathsf{runtime}$, define $$t_s^{\mathrm{♮}}:=(\lambda r.t_s)\mathsf{call}(\mathsf{clos}({\nu }_N(o),\overrightarrow{y}),n);$$ when ${\varrho }_r=\mathsf{erased}$, put $t_s^{\mathrm{♮}}=t_s$. The explicit beta-redex is load bearing: target call-by-value evaluates the recursive call to a value before substituting that value for $r$, just as S-Nat-S does. A direct occurrence of $n$ in $t_s$ requires ${\varrho }_n=\mathsf{runtime}$; the administrative recursive call also uses the retained successor field $n$ whenever ${\varrho }_r=\mathsf{runtime}$. Then $$|I_C(e_0;n^{{\varrho }_n}.r^{{\varrho }_r}.e_s;m)|=\mathsf{call}(\mathsf{clos}({\nu }_N(o),\overrightarrow{y}),|m|).$$

For a vector eliminator, define $u_0=|e_0|$, $u_s=|e_s|$, take the ordered lexical runtime capture slots $\overrightarrow{z}$, and choose the occurrence tag ${\nu }_V(o^{\prime })$. Its one scrutinee input follows an optional runtime index input: $${\delta }_t({\nu }_V(o^{\prime }))=(\overrightarrow{z};[m{]}_{{\varrho }_m},ys;\mathsf{case}ys\mathsf{of}\{\begin{array}{l}{C}_{\mathsf{vnil}}\Rightarrow u_0,\\ C_{\mathsf{vcons}}([n{]}_{{\kappa }_n},[a{]}_{{\kappa }_a},xs)\Rightarrow u_s^{\mathrm{♮}}.\end{array})$$ The pattern retains the predecessor and element exactly under their constructor-field marks, and $xs$ is the retained structural child. The admissibility implications above ensure that every runtime occurrence of a branch variable has a corresponding target binder. When ${\varrho }_r=\mathsf{runtime}$, put $$u_s^{\mathrm{♮}}:=(\lambda r.u_s)\mathsf{call}(\mathsf{clos}({\nu }_V(o^{\prime }),\overrightarrow{z}),[n{]}_{{\varrho }_m},xs).$$ For ${\varrho }_r=\mathsf{erased}$, put $u_s^{\mathrm{♮}}=u_s$. As in the natural-number tag, the beta-redex forces the recursive call before installing its value in the step body.

Erased branch variables do not occur in $u_s$ by the relevance derivation. Consequently $$|\mathsf{vind}(P;e_0;n^{{\varrho }_n}.a^{{\varrho }_a}.xs.r^{{\varrho }_r}.e_s;m,ys)|=\mathsf{call}(\mathsf{clos}({\nu }_V(o^{\prime }),\overrightarrow{z}),[|m|{]}_{{\varrho }_m},|ys|).$$ Square brackets mean that the listed target argument is present exactly for the runtime mark. Freshness of ${\nu }_N(o),{\nu }_V(o^{\prime })$ includes the source eliminator occurrence, so two syntactically equal branch bodies at different scopes cannot capture one another’s variables.

Finally, identity elimination has no recursive tag: This structural clause recurses only on the displayed branch subderivation. By lemma 126.11 it agrees with $|e_r[a/z]|$, but that larger substituted phrase is not used to define erasure. The clause is safe only with the three premises of Rel-J; in particular it is not a rule saying that an arbitrary proof may be inspected or that equality reflection holds. These equations exhaust the source grammar of definition 126.3.

Definition 126.12 — Value representation¶

The relation $v\mathcal{R}w$ between a closed source value and a closed Texec value is generated by

1. a source lambda with a runtime binder relates to the target lambda that erasure emits. Erased abstractions occur only inside the administrative redex of Rel-App-E, so they have no standalone clause in this value relation. The administrative closure $\mathsf{clos}(f,\overrightarrow{w})$ occurring inside a translated saturated call is well formed when its tag is the compiled tag and its stored values are related to the runtime captures. It has no standalone source-value case, because definition 126.3 excludes first-class recursive declarations;

2. a source constructor relates to the target block with the same tag and runtime arity when corresponding retained fields are related; and

3. $(v_1,v_2)$ relates to $C_{\mathsf{pair}}(w_1,w_2)$ when $v_i\mathcal{R}{w}_i$ for $i=1,2$, and every reflexivity value relates to the nullary tag $C_{\mathsf{refl}}$; and

4. the canonical Timpl constants $\mathsf{0}$, $\mathsf{tt}$, $\mathsf{ff}$, $\star$ relate to their fixed nullary target tags, and $\mathsf{suc}(v)$ relates to $C_{\mathsf{suc}}(w)$ whenever $v\mathcal{R}w$.

A target term is representation well formed for a declaration environment when every constructor has the declared runtime arity, every case has pairwise distinct tags, every branch for a constructor tag binds that same runtime arity, every closure tag names an erased body, every captured environment has the stored runtime length, and every generated call supplies the target entry’s runtime input arity. The property is inherited by subterms under their displayed binders. It is a syntactic representation invariant, not a progress theorem: it does not assert that an arbitrary application head evaluates to a lambda or that an arbitrary case scrutinee evaluates to a constructor.

Definition 126.15 — The Timpl-co-erasure card¶

Timpl-co-erasure instantiates the stream type and head/tail definitions of definition 124.1 at one fixed closed accepted Timpl data type $A:{\mathcal{U}}_i$, with accepted retention annotations for every constructor of $A$. Function-valued and otherwise non-data stream elements remain outside this card. For a compiled group with the generated state datatype $S={\mathsf{State}}_{\mathcal{G}}$ of definition 124.11, that helper block must be an accepted Timpl data type with explicit admissible retention annotations, and its generated maps $h:S\to A$ and $t:S\to S$ must satisfy runtime relevance under those annotations.

There is one further execution restriction. Call a closed data type runtime first order when every retained constructor or pair field is again runtime-first-order data and no retained field has a $\mathrm{\Pi }$-type; erased fields may have arbitrary accepted Timpl types. A first-order map body is built from variables of runtime-first-order data type, $\star ,\mathsf{tt},\mathsf{ff},\mathsf{0},\mathsf{suc}$, reflexivity, pairs, and accepted data constructors, together with datatype cases and the Boolean, natural, identity, and vector eliminators when every runtime premise and branch is again a first-order map body. Constructor arguments at erased fields are arbitrary checked static terms. There is no lambda or application inside a body and no named call; the only permitted lambda and application are the outer $\lambda s.r$ defining $h$ or $t$ and its saturated call at the state. Acceptance requires $A$, $S$, the initial state expression, and both generated map bodies to satisfy these conditions. This finite grammar is exactly the boundary at which weak source CBV and the normalizer of lemma 124.3 have the same retained constructor result.

Write $${\mathrm{\Gamma }}_{\mathrm{r}};{\mathrm{\Gamma }}_{\mathrm{e}}{⊢}_{\mathsf{fo}}r:B$$ for the least formation judgment generated by those clauses. The context ${\mathrm{\Gamma }}_{\mathrm{r}}$ contains data variables at runtime-first-order types. The context ${\mathrm{\Gamma }}_{\mathrm{e}}$ contains variables that may occur only in checked static arguments. A branch extends the appropriate context by each field according to its relevance annotation; the recursive-result binder of a natural or vector eliminator extends ${\mathrm{\Gamma }}_{\mathrm{r}}$. Thus the judgment records a finite syntax derivation. It is not the extensional relation ${\Downarrow }_{\mathsf{T}}$ of definition 124.2.

Thus the card covers neither an arbitrary unannotated state telescope nor a head or transition rejected by Timpl-erasure, and it excludes a generated map with a retained higher-order field or an internal helper application. The target signature fixes $C_{\mathsf{stream}}$ as an arity-two tag whose fields are nullary closures: $h$ is a nullary head thunk and $k$ a nullary tail closure. Erasure of the coiterator elaboration of definition 124.11 is $$|\mathsf{coiter}(h,t,s)|:=C_{\mathsf{stream}}(\mathsf{clos}(h_{\ast },|s|),\mathsf{clos}(t_{\ast },|s|)),$$ where $h_{\ast }$ and $t_{\ast }$ are fresh nullary closure tags, not the ordinary compiled tags of $h$ and $t$. For a fresh target variable $s^{\prime }$, their entries are $${\delta }_t(h_{\ast })=(s;\cdot ;|h(s)|)$$ and $${\delta }_t(t_{\ast })=(s;\cdot ;(\lambda s^{\prime }.C_{\mathsf{stream}}(\mathsf{clos}(h_{\ast },s^{\prime }),\mathsf{clos}(t_{\ast },s^{\prime })))|t(s)|).$$ The beta-redex in the second body computes the next state once and stores the result in both closures of the next stream block. In particular, compiling $t:S\to S$ as an ordinary tag would be wrong: that tag returns a state, whereas a tail observation must return a $C_{\mathsf{stream}}$ block. The target observer is a separate inductive judgment rather than an extra Texec term former. Write $\mathsf{Obs}(q,o,w)$ when the target stream block $q$ produces value $w$ after observation word $o$. It is generated by $$\frac{\mathsf{call}(h)\Downarrow w}{\mathsf{Obs}(C_{\mathsf{stream}}(h,k),\mathsf{head},w)}\mathrm{Obs}-\mathrm{Head}$$ and $$\frac{\begin{array}{c}\mathsf{call}(k)\Downarrow C_{\mathsf{stream}}(h^{\prime },k^{\prime })\\ \mathsf{Obs}(C_{\mathsf{stream}}(h^{\prime },k^{\prime }),o,w)\end{array}}{\mathsf{Obs}(C_{\mathsf{stream}}(h,k),\mathsf{tail}\cdot o,w)}\mathrm{Obs}-\mathrm{Tail}.$$ Thus exactly one of the two closures is forced per observation symbol, and the tail premise requires the forced closure to return the next $C_{\mathsf{stream}}$ block. This card inherits the source productivity theorem only for accepted stream groups and proves no normalization or generic coinductive simulation.