Recognition context and the auxiliary languages $L_u(C,K,l)$

Term.varsIn and TermVec.varsAllIn (mutual)

These two mutually recursive predicates are parameterized by a fixed sort type $S$, a signature $sig$ over $S$, an $S$-sorted family of variable sets $X$ (so $X_s$ is the set of variables of sort $s$), and a predicate $\mathrm{pred}$ that assigns to every sort $t \in S$ and every variable $x \in X_t$ a proposition $\mathrm{pred}\,t\,x$. Given an implicit sort $s$ and a term $P$ of sort $s$ built over $sig$ with variables drawn from $X$, the proposition $\mathrm{varsIn}\,\mathrm{pred}\,P$ is defined by structural recursion: if $P$ is a variable leaf $\mathrm{var}\,x$ (with $x \in X_s$), then $\mathrm{varsIn}\,\mathrm{pred}\,P$ is $\mathrm{pred}\,s\,x$; if $P$ is an operator application $\mathrm{app}\,\sigma\,ts$ (an operation symbol $\sigma$ applied to an argument vector $ts$), then $\mathrm{varsIn}\,\mathrm{pred}\,P$ is $\mathrm{varsAllIn}\,\mathrm{pred}\,ts$. The companion $\mathrm{varsAllIn}\,\mathrm{pred}$ acts on a term-vector $ts$ of type $w$ (a list of sorts): it is $\mathrm{True}$ when $ts$ is the empty vector, and $\mathrm{varsIn}\,\mathrm{pred}\,t \wedge \mathrm{varsAllIn}\,\mathrm{pred}\,ts'$ when $ts$ is a cons cell $\mathrm{cons}\,t\,ts'$. Consequently $\mathrm{varsIn}\,\mathrm{pred}\,P$ holds exactly when every variable occurrence appearing anywhere in the tree of $P$ satisfies $\mathrm{pred}$ at its sort; for a term with no variable leaves (all leaves being nullary operator applications) the predicate is vacuously $\mathrm{True}$.

KleeneCtx

$\mathrm{KleeneCtx}\,sig\,X$ is a structure (record), parameterized by a signature $sig$ over the sort type $S$ and an $S$-sorted variable family $X$, that bundles three fields. The first field $n$ is a function $n : S \to \mathbb{N}$ assigning a natural number to each sort. The second field $\mathrm{Nop}$ is, for every list of sorts $w$, every sort $s$, and every operation symbol $\sigma \in sig\,w\,s$, a function that takes an argument tuple whose $i$-th component lies in $\mathrm{Fin}(n\,s_i)$ (the type $\mathrm{Fin}(k) = \{0,1,\dots,k-1\}$, empty when $k = 0$) — one component per sort listed in $w$ — and returns an element of $\mathrm{Fin}(n\,s)$. The third field $\mathrm{fgen}$ is an $S$-indexed map that assigns to each sort $s$ and each variable $x \in X_s$ an element of $\mathrm{Fin}(n\,s)$. Nothing in the structure forbids $n\,s = 0$ for some sorts. Throughout the remaining declarations, $ctx$ denotes an arbitrary term of this structure type.

KleeneCtx.NAlg

For a context $ctx$, $\mathrm{NAlg}$ is the $sig$-algebra whose carrier at each sort $s$ is the finite type $\mathrm{Fin}(ctx.n\,s)$ and whose interpretation of operation symbols is the field $ctx.\mathrm{Nop}$. In other words it packages $s \mapsto \mathrm{Fin}(ctx.n\,s)$ together with $ctx.\mathrm{Nop}$ into an $\mathrm{Algebra}\,sig$.

KleeneCtx.Z

$Z$ is the $S$-sorted family defined by $Z_s = X_s \oplus \mathrm{Fin}(ctx.n\,s)$, the disjoint-sum (tagged union) of the original variable set at sort $s$ with the finite type $\mathrm{Fin}(ctx.n\,s)$. This uses $\mathrm{extVars}\,X\,E$, whose value at sort $s$ is $X_s \oplus E_s$. Thus an element of $Z_s$ is either a left-tagged original variable $\mathrm{inl}\,x$ with $x \in X_s$, or a right-tagged numeral $\mathrm{inr}\,m$ with $m \in \mathrm{Fin}(ctx.n\,s)$.

KleeneCtx.fHom

$\mathrm{fHom}$ is the $sig$-algebra homomorphism from the free $sig$-algebra on the variable family $X$ (whose carrier at sort $s$ is the set of terms $\mathrm{Term}\,sig\,X\,s$) to the algebra $\mathrm{NAlg}$, obtained as the evaluation homomorphism induced by the assignment $ctx.\mathrm{fgen}$. Its underlying map sends a term $t$ of sort $s$ to $\mathrm{Term.eval}\,\mathrm{NAlg}\,ctx.\mathrm{fgen}\,t$: each variable leaf $\mathrm{var}\,x$ is sent to $ctx.\mathrm{fgen}\,s\,x \in \mathrm{Fin}(ctx.n\,s)$, and each application $\mathrm{app}\,\sigma\,ts$ is sent to $ctx.\mathrm{Nop}\,\sigma$ applied to the recursively evaluated arguments. It also carries the proof that this map commutes with all operations.

KleeneCtx.hAssign

$\mathrm{hAssign}$ is the $S$-indexed map from $Z$ to the family $s \mapsto \mathrm{Fin}(ctx.n\,s)$ defined case-wise on the sum: for a sort $s$ and an element $z \in Z_s = X_s \oplus \mathrm{Fin}(ctx.n\,s)$, if $z = \mathrm{inl}\,x$ it returns $ctx.\mathrm{fgen}\,s\,x$, and if $z = \mathrm{inr}\,m$ it returns $m$ itself (the identity on the numeral component).

KleeneCtx.hHom

$\mathrm{hHom}$ is the $sig$-algebra homomorphism from the free $sig$-algebra on the family $Z$ (carrier at sort $s$ equal to the terms $\mathrm{Term}\,sig\,Z\,s$) to $\mathrm{NAlg}$, obtained as the evaluation homomorphism induced by $\mathrm{hAssign}$. Its underlying map sends a term $Q$ of sort $s$ over the variable family $Z$ to its value in $\mathrm{Fin}(ctx.n\,s)$, where a left-tagged leaf $\mathrm{inl}\,x$ is evaluated via $ctx.\mathrm{fgen}$, a right-tagged leaf $\mathrm{inr}\,m$ is evaluated to $m$, and applications are evaluated via $ctx.\mathrm{Nop}$.

KleeneCtx.hVal

$\mathrm{hVal}$ takes a sorted term $Q$ over the family $Z$ — that is, an element of $\Sigma\,s : S,\ \mathrm{Term}\,sig\,Z\,s$, a dependent pair consisting of a sort $Q_1$ and a term $Q_2$ of sort $Q_1$ over $Z$ — and returns the natural number $\big(\mathrm{hHom}(Q_2)\big).\mathrm{val}$, i.e. the underlying $\mathbb{N}$ of the element $\mathrm{hHom}(Q_2) \in \mathrm{Fin}(ctx.n\,Q_1)$ (its representative in $\{0,1,\dots,ctx.n\,Q_1 - 1\}$).

KleeneCtx.inXC

$\mathrm{inXC}$ takes a family $C$ assigning to each sort $s$ a subset $C_s \subseteq \mathrm{Fin}(ctx.n\,s)$, a sort $t$, and an element $z \in Z_t = X_t \oplus \mathrm{Fin}(ctx.n\,t)$, and returns a proposition by case analysis on the sum: if $z = \mathrm{inl}\,x$ (an original variable) the proposition is $\mathrm{True}$; if $z = \mathrm{inr}\,m$ (a numeral) the proposition is $m \in C_t$.

KleeneCtx.auxLang

Fix a context $ctx : \mathrm{KleeneCtx}\,sig\,X$ (with $S$, $sig$, $X$ implicit). Given a sort $u \in S$, a family $C$ with $C_s \subseteq \mathrm{Fin}(ctx.n\,s)$ for every sort $s$, a function $K : S \to \mathbb{N}$, and a target element $l \in \mathrm{Fin}(ctx.n\,u)$, the term $\mathrm{auxLang}\,ctx\,u\,C\,K\,l$ is a subset of the terms of sort $u$ over the signature $sig$ with variables in the family $Z$ (where $Z_s = X_s \oplus \mathrm{Fin}(ctx.n\,s)$). It consists of exactly those terms $P$ of sort $u$ over $Z$ satisfying the conjunction of all three of the following conditions.

(1) Variable-membership condition. $\mathrm{Term.varsIn}\,(ctx.\mathrm{inXC}\,C)\,P$ holds: every variable leaf occurring in $P$ satisfies $\mathrm{inXC}\,C$ at its sort; equivalently, every numeral leaf $\mathrm{inr}\,m$ of some sort $t$ appearing in $P$ has $m \in C_t$, while original-variable leaves $\mathrm{inl}\,x$ impose no constraint.

(2) Strict-subterm value bound. For every sorted term $Q$ over $Z$ (an element of $\Sigma\,s : S,\ \mathrm{Term}\,sig\,Z\,s$, with sort $Q_1$ and term $Q_2$) such that

$$\mathrm{SubtermLT}\,Q\,\langle u, P\rangle \quad\text{and}\quad \neg\,\mathrm{Min}\,Q \quad\text{and}\quad \mathrm{Term.varsIn}\,(ctx.\mathrm{inXC}\,C)\,Q_2,$$

it must hold that

$$\mathrm{hVal}\,Q \;<\; K\,Q_1,$$

that is, the natural number $\big(\mathrm{hHom}(Q_2)\big).\mathrm{val}$ is strictly less than $K$ evaluated at the sort $Q_1$ of $Q$. Here:

• $\mathrm{SubtermLT}\,Q\,\langle u, P\rangle$ is the transitive closure (one or more steps) of the immediate-subterm relation $\mathrm{ImmSub}$ applied to the pair $Q$ and the sorted term $\langle u, P\rangle$; $\mathrm{ImmSub}\,a\,b$ holds when $b$'s term component is an application $\mathrm{app}\,\sigma\,ts$ for some symbol $\sigma$ and argument vector $ts$, and $a$'s term component occurs as one of the entries of $ts$. So $Q$ ranges over the proper subterms of $P$ (paired with their sorts) reachable by at least one descent step.
• $\neg\,\mathrm{Min}\,Q$ is the negation of the statement "$\mathrm{Min}\,Q$", where $\mathrm{Min}\,Q$ means that no sorted term $a$ satisfies $\mathrm{ImmSub}\,a\,Q$; i.e. $\neg\,\mathrm{Min}\,Q$ says it is not the case that $Q$ has no immediate subterm, so $Q_2$ is an application to a non-empty argument vector (it is not a variable leaf and not a nullary application).
• $\mathrm{Term.varsIn}\,(ctx.\mathrm{inXC}\,C)\,Q_2$ says every variable leaf of $Q_2$ satisfies $\mathrm{inXC}\,C$, as in condition (1).

If no $Q$ meets all three antecedents (for instance when $P$ is itself a variable or a shallow term), condition (2) is vacuously satisfied. If for some qualifying $Q$ one has $K\,Q_1 = 0$, then $\mathrm{hVal}\,Q < 0$ is impossible (values are natural numbers), so any $P$ admitting such a $Q$ is excluded.

(3) Evaluation target condition. $\mathrm{hHom}(P) = l$: evaluating $P$ through the homomorphism $\mathrm{hHom}$ into $\mathrm{NAlg}$ (numeral leaves interpreted as themselves, original-variable leaves via $ctx.\mathrm{fgen}$, operations via $ctx.\mathrm{Nop}$) yields exactly the prescribed element $l$ of $\mathrm{Fin}(ctx.n\,u)$.