Corollary 4.4: Rec is a closed subset of the regular algebra

Read-back of MSKleene.rec_closed_reg

Fix a type $S$ that carries a Finite instance (so there are only finitely many "sorts"). A signature $\mathrm{sig}$ assigns to every pair $(w,s)$ — with $w=[s_1,\dots,s_k]$ a finite list of sorts and $s$ a sort — a type $\mathrm{sig}(w,s)$ of operation symbols of input arity $w$ and result sort $s$; no finiteness whatsoever is assumed of $\mathrm{sig}$. Let $Z$ be an $S$-indexed family of types $(Z_s)_{s\in S}$ ("generators"), and let $hZ$ be the hypothesis that the dependent sum $\sum_{s\in S} Z_s$ is a finite type. Write $\mathrm{Term}(r)$ for the type of many-sorted terms of sort $r$ built from these generators and the symbols of $\mathrm{sig}$: each $z:Z_r$ yields a term $\mathrm{var}(z):\mathrm{Term}(r)$, and each $\sigma:\mathrm{sig}(w,r)$ together with terms $t_i:\mathrm{Term}(s_i)$ yields a term $\sigma(t_1,\dots,t_k):\mathrm{Term}(r)$. Let $\mathcal T$ be the free $\mathrm{sig}$-algebra on $Z$: its carrier at sort $r$ is $\mathrm{Term}(r)$ and its interpretation of a symbol $\sigma$ is formal application.

Recognizability. For a sort $r$ and a set $L\subseteq\mathrm{Term}(r)$, "$L$ is $r$-recognizable in $\mathcal T$" means that there exist

• a $\mathrm{sig}$-algebra $B$ (a carrier family $(B_r)_{r\in S}$ with an interpretation of every symbol of $\mathrm{sig}$) such that the dependent sum $\sum_{r\in S} B_r$ is a finite type;
• a homomorphism of $\mathrm{sig}$-algebras $f:\mathcal T\to B$, i.e. a family of maps $f_r:\mathrm{Term}(r)\to B_r$ satisfying $f_r\big(\sigma(t_1,\dots,t_k)\big)=B.\mathrm{op}\,\sigma\,\big(f_{s_1}(t_1),\dots,f_{s_k}(t_k)\big)$ for every symbol $\sigma$ of $\mathrm{sig}$;
• a set $M\subseteq B_r$;

such that

$$L \;=\; f_r^{-1}(M)\;=\;\{\, t:\mathrm{Term}(r)\ \mid\ f_r(t)\in M \,\}.$$

Nothing further is required of $B$, $f$, or $M$.

The statement. Given the finite sort type $S$, the signature $\mathrm{sig}$, the family $Z$, the hypothesis $hZ$ ($\sum_s Z_s$ finite), an implicit list of sorts $w=[s_1,\dots,s_k]$ (with $k\ge 0$), an implicit result sort $s$, an element $\mathrm{sym}$ of the type $\mathrm{RegSym}\,\mathrm{sig}\,Z\,w\,s$ of "regular" symbols, a tuple $Ls=(L_1,\dots,L_k)$ with $L_i\subseteq\mathrm{Term}(s_i)$ for each $i$, and a hypothesis $hLs$ stating that for every $i\in\{1,\dots,k\}$ the set $L_i$ is $s_i$-recognizable in $\mathcal T$ (when $k=0$ this hypothesis holds vacuously), the theorem asserts:

$$\Lambda \ \text{ is } s\text{-recognizable in } \mathcal T, \qquad \text{where } \ \Lambda \;:=\; (\mathrm{regPowerAlgebra}\,\mathrm{sig}\,Z).\mathrm{op}\ \mathrm{sym}\ Ls \ \subseteq\ \mathrm{Term}(s).$$

The set $\Lambda$ is defined by cases on which of the five constructors $\mathrm{sym}$ is (each case constrains the implicit $w$ and $s$):

• $\mathrm{sym}=\mathrm{base}(\sigma)$ for a symbol $\sigma:\mathrm{sig}(w,s)$ of the original signature, with $w$ arbitrary:

$$\Lambda=\{\,\sigma(t_1,\dots,t_k)\ \mid\ t_i\in L_i \text{ for all } i\,\}$$

(the elementwise application of $\sigma$ to the argument sets; if $w=[\,]$ then $\Lambda=\{\sigma()\}$ is a singleton and $hLs$ says nothing).

• $\mathrm{sym}=\mathrm{empty}(s)$: this constructor forces $w=[\,]$, so $Ls$ is the empty tuple and $hLs$ is vacuous; then

$$\Lambda=\varnothing.$$

• $\mathrm{sym}=\mathrm{iter}(s,z)$ carrying a generator $z:Z_s$: this forces $w=[s]$, so $Ls=(L_1)$ with $L_1\subseteq\mathrm{Term}(s)$ and $hLs$ says $L_1$ is $s$-recognizable; then

$$\Lambda=\bigcup_{i\in\mathbb N}\Sigma_i,\qquad \Sigma_0=\{\mathrm{var}(z)\},\qquad \Sigma_{i+1}=\Sigma_i\ \cup\ \mathrm{substP}\!\left(z,\ \Sigma_i,\ s,\ L_1\right),$$

i.e. $\Sigma_{i+1}$ adjoins to $\Sigma_i$ every term obtained from some $P\in L_1$ by replacing each occurrence of $\mathrm{var}(z)$ in $P$, independently, by a term of $\Sigma_i$.

• $\mathrm{sym}=\mathrm{plus}(s)$: this forces $w=[s,s]$, so $Ls=(L_1,L_2)$ with $L_1,L_2\subseteq\mathrm{Term}(s)$ and $hLs$ says both are $s$-recognizable; then

$$\Lambda=L_1\cup L_2.$$

• $\mathrm{sym}=\mathrm{subst}(t,s,z)$ carrying a generator $z:Z_t$ (the constructor's two sort arguments are $t$ and the result sort $s$): this forces $w=[t,s]$, so $Ls=(L_1,L_2)$ with $L_1\subseteq\mathrm{Term}(t)$ and $L_2\subseteq\mathrm{Term}(s)$, and $hLs$ says $L_1$ is $t$-recognizable and $L_2$ is $s$-recognizable; then

$$\Lambda=\mathrm{substP}(z,L_1,s,L_2)=\bigcup_{P\in L_2}\widehat h_{\,z,L_1}(P),$$

the set of all terms obtained from some $P\in L_2$ by independently replacing every occurrence of $\mathrm{var}(z)$ by a term of $L_1$.

Throughout, $\mathrm{substP}(z,A,r,K)$ — for $z:Z_v$, $A\subseteq\mathrm{Term}(v)$, $K\subseteq\mathrm{Term}(r)$ — denotes $\bigcup_{P\in K}\widehat h_{\,z,A}(P)$, where $\widehat h_{\,z,A}$ is the evaluation homomorphism from $\mathcal T$ into the power algebra of $\mathcal T$ (carrier $\mathrm{Set}(\mathrm{Term}(r))$ at each sort $r$, every symbol interpreted by elementwise application) induced by the assignment that sends the generator $z$ to the set $A$ and every other generator $y:Z_u$ to the singleton $\{\mathrm{var}(y)\}$; concretely, $\widehat h_{\,z,A}(P)$ is the set of terms produced from $P$ by substituting, independently at each occurrence of $\mathrm{var}(z)$, an arbitrary term of $A$, leaving all other variables unchanged.

The algebra $\mathrm{regPowerAlgebra}\,\mathrm{sig}\,Z$ is an algebra over the extended signature $\mathrm{RegSym}\,\mathrm{sig}\,Z$ and is used only to produce the set $\Lambda$; the witnessing algebra $B$, homomorphism $f$, and set $M$ in both the hypothesis $hLs$ and the conclusion are for the original signature $\mathrm{sig}$ and the free term algebra $\mathcal T$. "Finite" in "$\sum_s Z_s$ finite" and in "$\sum_r B_r$ finite" means finiteness of the single dependent-sum type ranging over all sorts.