Recursive Function Groups and Termination

Definition 123.1 — The Timpl-rec system card¶

Timpl-rec accepts a finite mutually recursive group $$\mathcal{G}=\{f_i:({\mathrm{\Delta }}_i)\to B_i\mathsf{where}{C}_i\mid 1\le i\le q\}.$$ Each $C_i$ is an ordered Timpl-clauses matrix accepted by definition 121.1. Every strongly connected component chooses one of two decrease disciplines.

1. A structural certificate names one explicit argument position of every function in the component. All named arguments inhabit either one mutual Timpl-data block at one common parameter vector or one primitive Timpl inductive type, $\mathbb{N}$ or $\mathsf{Vec}(c,-)$ at one common element code $c$. At a recursive call the argument supplied in the callee’s named position must be a direct constructor child exposed by a clause split at the caller’s named position.

2. A lexicographic certificate names a finite tuple of arguments and a well-founded relation for each coordinate. At a recursive call, the first coordinate that changes must strictly decrease; every earlier coordinate must be definitionally unchanged.

The target Timpl-rec-core is the literal union of the indexed Timpl fragment with the accessibility predicate, eliminator, and computation rule of definition 82.2, definition 82.6. No general fixpoint is added. Every accepted call is translated with its checked accessibility predecessor proof. Size-change matrices, sized types, semantic termination, effects, and higher-order recursive arguments are outside this card.

Definition 123.2 — Function call graph¶

The function call graph has one vertex for each $f_i$. An edge $f_i\to f_j$ records every syntactic call to $f_j$ in a reachable right side of $f_i$, together with its clause path and candidate decrease certificate. Calls in shadowed rows are omitted because they cannot occur at run time. A strongly connected component is recursive exactly when it has more than one vertex or a self-loop.

Definition 123.3 — Structural descent judgment¶

At a clause leaf with branch context $\mathrm{\Theta }$, let $x$ be the designated argument before splitting. The compiler records the finite set $\mathsf{Child}(x)\subseteq \mathrm{\Theta }$ of recursive fields introduced by the single constructor split whose scrutinee is $x$. A later split of one of those fields does not add its descendants to $\mathsf{Child}(x)$. The judgment $$\mathrm{\Theta };x⊢u\mathsf{desc}x$$ holds exactly when $u$ is definitionally one of those recorded fields. It is not closed under arbitrary evaluation, transitivity, projections not introduced by the split, or user propositions about size.

Definition 123.4 — Lexicographic call certificate¶

Fix well-founded relations $R_h$ on $A_h$, for $1\le h\le d$. A call from tuple $\overrightarrow{a}$ to $\overrightarrow{b}$ has a lexicographic certificate when there is a least coordinate $k$ such that $$a_1\equiv b_1,\dots ,a_{k-1}\equiv b_{k-1},b_k{R}_k{a}_k.$$ Later coordinates are unrestricted. The certificate stores $k$, the conversion derivations for the prefix, and the proof of the strict step.

Definition 123.5 — Recursive-group rejection diagnostic¶

The Timpl-rec checker either returns a certified component list or one record $$\mathsf{RecReject}(S,f_i\to f_j,\omega ,\delta ,\overrightarrow{a},\overrightarrow{b},F).$$ Here $S$ is the computed component; $f_i\to f_j$ and $\omega$ name the source, target, and exact clause-tree call site; $\delta$ is the chosen structural or lexicographic discipline; $\overrightarrow{a}$ and $\overrightarrow{b}$ are the typed caller and callee tuples after the leaf substitution; and $F$ is the failed certificate premise. In the structural case, $F$ prints the named positions, the exposed direct-child set, and the failed definitional comparison. In the lexicographic case, it prints every earlier comparison through the first unequal coordinate and identifies either the earlier increase, the missing strict proof, or the exhausted equal tuple.

The checker computes components in source-vertex order, scans their reachable clause trees and call sites left to right, and compares lexicographic coordinates from first to last. Edges leaving $S$ are recorded but require no predecessor certificate. The first internal edge without a complete certificate is returned; no diagnostic is selected by a fixture name.

Definition 123.7 — Mutual-block carrier and direct-child relation¶

Fix the common parameter vector $\overrightarrow{p}$ of a mutual datatype block $\mathcal{B}=(D_1,\dots ,D_r)$ named by a structural certificate. The number $r$ of block families is independent of the number $q$ of functions. The certificate therefore stores, for every $f_i$, a family tag $\kappa (i):{\mathsf{Fin}}_{\mathsf{ind}}(r)$ for its named argument. Here ${\mathsf{Fin}}_{\mathsf{ind}}$ is the indexed family, constructors, and eliminator fixed in chapter 31; the extensional finite-set presentation is not being used.

To make the varying index telescopes well formed, set $$L_{\mathcal{B}}:=max(0,\underset{l}{max}\mathsf{lev}({\mathrm{\Delta }}_l),\underset{l}{max}{\ell }_l)$$ and define the tagged block payload by dependent elimination on $l:{\mathsf{Fin}}_{\mathsf{ind}}(r)$: $${\mathsf{Payload}}_{\mathcal{B}}(l):=\sum _{\overrightarrow{ı}:{\mathrm{\Delta }}_l}{D}_l\overrightarrow{p}\overrightarrow{ı}:{\mathcal{U}}_{L_{\mathcal{B}}}.$$ Each of the finitely many eliminator branches is the displayed iterated dependent sum. When a branch inhabits a smaller universe, the processor inserts the strict lift of definition 29.10; its decoding equation makes the lifted branch judgmentally equal to the displayed payload. Put $${\mathsf{Carrier}}_{\mathcal{B}}(\overrightarrow{p}):=\sum _{l:{\mathsf{Fin}}_{\mathsf{ind}}(r)}{\mathsf{Payload}}_{\mathcal{B}}(l):{\mathcal{U}}_{L_{\mathcal{B}}}.$$ Its uniform direct-child relation ${\mathsf{DChild}}_{\mathcal{B}}$ is generated once on this total space. More precisely, let $$K_{\mathcal{B}}:=max(\mathsf{lev}({\mathrm{\Delta }}_p),L_{\mathcal{B}},\underset{s}{max}\mathsf{lev}({\mathrm{\Theta }}_s)).$$ The processor submits the nonrecursive Timpl-data family $${\mathsf{DChild}}_{\mathcal{B}}:{\mathsf{Carrier}}_{\mathcal{B}}(\overrightarrow{p})\to {\mathsf{Carrier}}_{\mathcal{B}}(\overrightarrow{p})\to {\mathcal{U}}_{K_{\mathcal{B}}}$$ with the constructors below. The maximum emitted by definition 122.13 is exactly $K_{\mathcal{B}}$: it includes the parameter telescope, both carrier-index binders, every constructor telescope, and the displayed family level. No constructor argument mentions ${\mathsf{DChild}}_{\mathcal{B}}$, so definition 122.4 accepts the generated block. For every constructor $c:\mathrm{\Theta }\to D_l\overrightarrow{p}\overrightarrow{ı}$ and every field $x_r:D_k\overrightarrow{p}\overrightarrow{ȷ}$ of $\mathrm{\Theta }$ whose head is a family of $\mathcal{B}$, it has the constructor $${\mathsf{child}}_{c,r}:{\mathsf{DChild}}_{\mathcal{B}}((k,(\overrightarrow{ȷ},x_r)),(l,(\overrightarrow{ı},c\overrightarrow{x}))).$$ The relation is defined on all tagged block inhabitants; it does not mention a clause leaf. Mutual induction on $\mathcal{B}$ constructs accessibility of every $(l,(\overrightarrow{ı},a))$, because each predecessor proof selects one recursive constructor field and the induction hypothesis supplies its accessibility proof.

Definition 123.10 — The certified tagged call relation¶

Let $S$ choose the structural discipline and let $p_i$ be the position named by its certificate for $f_i$. The carrier and the measure map out of each state constructor depend on the single discipline chosen by the component: Here $\kappa (i)$ is present only in the mutual-block row, while $n_i(\overrightarrow{a})$ is the index at which the named vector argument is typed. In the mutual row, ${\iota }_l(a)$ abbreviates $(l,({\overrightarrow{ı}}_i(\overrightarrow{a}),a))$ when $a:D_l\overrightarrow{p}{\overrightarrow{ı}}_i(\overrightarrow{a})$. Write ${\mathsf{DChild}}_S$ respectively for ${\mathsf{DChild}}_{\mathcal{B}}$, ${\mathsf{DChild}}_{\mathbb{N}}$, or ${\mathsf{DChild}}_{\mathsf{Vec}(c,-)}$. Put $${\mathsf{in}}_j(\overrightarrow{b})R_S{\mathsf{in}}_i(\overrightarrow{a}):={\mathsf{DChild}}_S({\mu }_j^S(\overrightarrow{b}),{\mu }_i^S(\overrightarrow{a})).$$ Thus neither $\kappa$ nor a mutual-block carrier is silently assigned to a primitive discipline. Let $S$ instead choose the lexicographic discipline with coordinates $1\le h\le d$, relations $R_h$, and coordinate projections $\overrightarrow{\pi }$. Put $${\mathsf{in}}_j(\overrightarrow{b})R_S{\mathsf{in}}_i(\overrightarrow{a}):=\overrightarrow{\pi }({\mathsf{in}}_j(\overrightarrow{b}))\mathsf{lex}(R_1,\dots ,R_d)\overrightarrow{\pi }({\mathsf{in}}_i(\overrightarrow{a})),$$ the finite lexicographic product of lemma 123.9. In both cases the tag is not part of the measure: it selects which projection is read, and a call may cross to any $f_j$ of the component. By construction each accepted recursive edge of definition 123.2 is one $R_S$ step, and its certificate is a proof of that step.

Definition 123.13 — Body translation¶

The translation of a case-tree leaf replaces a recursive call $f_j\overrightarrow{b}$ made while defining $f_i\overrightarrow{a}$ by the recursive hypothesis supplied at the stored proof ${\mathsf{in}}_j(\overrightarrow{b})R_S{\mathsf{in}}_i(\overrightarrow{a})$. Nonrecursive calls and constructors are translated homomorphically. Constructor splits remain the Timpl eliminators generated by the clause compiler.

Definition 123.15 — Closed source and recursive-core evaluation¶

For an accepted group $\mathcal{G}$, let ${\mathrm{\Sigma }}_{\mathcal{G}}$ contain its accepted ambient Timpl signature, every Timpl-data block scrutinized by a clause tree, and every generated state block. A program root contraction is either a root contraction of definition 111.22 or a generated Block-comp equation belonging to one of those accepted blocks. The signature parameter matters because a split over a user declaration computes by its generated equation rather than by a fixed-kernel rule.

Let $\mathsf{select}(C_i,\overrightarrow{a})=(\sigma ,e)$ mean that the ordered clause tree for $f_i$, on the closed constructor tuple $\overrightarrow{a}$, selects the reachable leaf $e$ with branch substitution $\sigma$. The source root family also has $$\frac{\mathsf{select}(C_i,\overrightarrow{a})=(\sigma ,e)}{f_i\overrightarrow{a}\stackrel{R-Call}{{⇝}_0}e[\sigma ]}\mathrm{R}-\mathrm{Call}.$$ Let $\mathcal{C}(\mathcal{G})$ be the Timpl-rec-core definition produced by definition 123.13, and write ${\mathsf{compile}}_{\mathcal{G}}(t)$ for its homomorphic extension to source term contexts. The target root family replaces R-Call by the macro-contraction $$\frac{\mathsf{select}(C_i,\overrightarrow{a})=(\sigma ,e)}{{\mathsf{compile}}_{\mathcal{G}}(f_i\overrightarrow{a})\stackrel{C-Call}{{⇝}_0}{\mathsf{compile}}_{\mathcal{G}}(e[\sigma ])}\mathrm{C}-\mathrm{Call}.$$ The macro is licensed only when its left side contracts to its right side by the nonempty deterministic Timpl-rec-core sequence consisting of the generated outer definition beta contractions, the generated state-block equation, WF-$\beta$, and the administrative beta contractions introduced by body translation. It is a trace boundary, not a new target equality rule. The compiler marks that whole expansion as one administrative region. A fixed-kernel contraction strictly inside such a region is not an independent target program root; it is scheduled only as part of C-Call. Fixed-kernel contractions in homomorphic source positions and all shared Block-comp roots remain independent program roots.

For either grammar, a dynamic compatible context is a compatible term context of definition 111.22 except that it has no hole in an accessibility proof, a stored predecessor certificate, or a conversion witness introduced by the compiler. These positions remain available to kernel conversion and typing, but the program evaluator does not schedule them. Ordinary proof terms written by the programmer are not frozen. Write $⟶$ for closure of the appropriate root family under dynamic compatible contexts. The source and target grammars determine whether the third root family is R-Call or C-Call.

For closed terms, $t{\Downarrow }_{\mathsf{R}}v$ means that a finite $⟶$-sequence using the source root family carries $t$ to the closed constructor normal form $v$. For closed target terms, $t{\Downarrow }_{\mathsf{RC}}v$ means the analogous finite sequence using the target root family. Thus one source R-Call and one target C-Call have the same visible granularity, while every C-Call has the stated nonempty raw-core expansion. Neither relation borrows the execution calculus introduced in a later chapter.