Proposition 4.10: every recognizable language is regular

The theorem rec_subset_reg is universally quantified over: an arbitrary type $S$ of "sorts" equipped with a Finite instance (so $S$ has only finitely many elements); an arbitrary many‑sorted signature $\mathrm{sig} : \mathrm{List}\,S \to S \to \mathrm{Type}$, which assigns to each input word $w$ and output sort $s'$ a type $\mathrm{sig}(w,s')$ of operation symbols of that profile; and an arbitrary sorted family of variables $X : S \to \mathrm{Type}$. It takes two finiteness hypotheses,

i.e. the total type of all operation symbols across all profiles is finite, and the total type of all variables across all sorts is finite (finiteness here is the propositional "is a finite type", not a chosen enumeration). It also fixes one sort $s : S$ (whose mere presence forces $S$ to be inhabited). Write $\mathrm{Term}(\mathrm{sig}, V, s')$ for the type of well‑sorted terms of sort $s'$ built from a variable family $V$ and the symbols of $\mathrm{sig}$, and let $\mathcal{F} := \mathrm{freeAlgebra}(\mathrm{sig}, X)$ be the term algebra, whose carrier at sort $s'$ is $\mathrm{Term}(\mathrm{sig}, X, s')$ and whose operation for a symbol $\sigma$ is the formal constructor sending an argument tuple to the term $\sigma(\dots)$. The conclusion is the set inclusion

read as an inclusion between two collections of subsets of $\mathrm{Term}(\mathrm{sig}, X, s)$: every set $L \subseteq \mathrm{Term}(\mathrm{sig}, X, s)$ that is "$s$‑recognizable" over $\mathcal{F}$ is also "$s$‑regular" over $\mathrm{sig}$ and $X$.

Unfolding "recognizable": $L \in \mathrm{RecS}(\mathcal{F}, s)$ asserts the existence of a $\mathrm{sig}$‑algebra $B$ — a carrier family $B_\bullet : S \to \mathrm{Type}$ together with, for every symbol $\sigma \in \mathrm{sig}(w, s')$, an operation $B.\mathrm{op}\,\sigma$ taking a $w$‑indexed tuple of arguments drawn from $B_\bullet$ to an element of $B_{s'}$ — such that $B$ is finite in the sense that $\sum_{s' : S} B_{s'}$ is a finite type; together with a homomorphism $f : \mathcal{F} \to B$, meaning a sorted map $f_\bullet$ satisfying $f_{s'}\big(\sigma(\vec a)\big) = B.\mathrm{op}\,\sigma\,(f\text{ applied componentwise to }\vec a)$ for every symbol and every argument tuple; and a subset $M \subseteq B_{s}$; such that

i.e. $L$ is exactly $\{\, t \in \mathrm{Term}(\mathrm{sig}, X, s) : f_{s}(t) \in M \,\}$. This is an exact equality of sets; no surjectivity or any further condition is placed on $f$ or $M$, and degenerate choices $M = \varnothing$ and $M = B_s$ are included (making $L = \varnothing$ and $L = \mathrm{Term}(\mathrm{sig}, X, s)$ recognizable).

Unfolding "regular": $L \in \mathrm{RegS}(\mathrm{sig}, X, s)$ asserts the existence of an auxiliary sorted variable family $E : S \to \mathrm{Type}$ such that the sortwise disjoint union $Z := \big(s' \mapsto X(s') \sqcup E(s')\big)$ is finite in the sense that $\sum_{s' : S}\big(X(s') \sqcup E(s')\big)$ is a finite type, together with a "regular expression" $R$ of sort $s$ (defined below), such that

an exact equality of subsets of $\mathrm{Term}(\mathrm{sig}, Z, s)$, where $\bar\iota$ relabels a term over $X$ into a term over $Z$ by replacing every variable $x$ (at every sort, recursively through the whole term, leaving function symbols untouched) with its left injection $\mathrm{inl}(x) \in X(s') \sqcup E(s')$; so the right‑hand side is the image of $L$ under this inclusion‑relabeling. A regular expression of sort $s$ is an element of $\mathrm{Term}(\widehat{\mathrm{sig}}, Z, s)$: a term of sort $s$ whose variables are drawn from $Z$ and whose function symbols come from the extended signature $\widehat{\mathrm{sig}} := \mathrm{RegSym}(\mathrm{sig}, Z)$, which at profile $(w, s')$ consists of a symbol $\mathrm{base}(\sigma)$ for each original $\sigma \in \mathrm{sig}(w, s')$ (with the same profile); for $w = []$, a nullary symbol $\mathrm{empty}(s')$ for every output sort $s'$; for $w = [s']$, a unary symbol $\mathrm{iter}(s', z)$ for each $z \in Z(s')$; for $w = [s', s']$, a binary symbol $\mathrm{plus}(s')$; and for $w = [t', s']$, a binary symbol $\mathrm{subst}(t', s', z)$ for each $z \in Z(t')$.

The semantics $\llbracket R \rrbracket := \mathrm{interpExpr}(\mathrm{sig}, Z, s, R)$ is the value at sort $s$, applied to $R$, of the unique $\widehat{\mathrm{sig}}$‑algebra homomorphism from the free $\widehat{\mathrm{sig}}$‑algebra on variable set $Z$ into the algebra $\mathrm{regPowerAlgebra}(\mathrm{sig}, Z)$ that sends each variable $z \in Z(s')$ to the singleton set $\{\mathrm{var}(z)\}$. The algebra $\mathrm{regPowerAlgebra}(\mathrm{sig}, Z)$ has carrier $s' \mapsto \mathrm{Set}\big(\mathrm{Term}(\mathrm{sig}, Z, s')\big)$ (sets of ordinary $Z$‑terms) and interprets the extended symbols as:

• $\mathrm{base}(\sigma)$ with $\sigma \in \mathrm{sig}(w, s')$, applied to a tuple of sets $(L_i)_i$ indexed by the sorts of $w$, yields $\big\{\, y \;:\; \exists\, (t_i)_i,\ (\forall i,\ t_i \in L_i)\ \wedge\ y = \sigma(t_1,\dots,t_k)\,\big\}$, the set of formal applications of $\sigma$ whose $i$‑th argument ranges over $L_i$;
• $\mathrm{empty}(s')$ yields the empty set $\varnothing \subseteq \mathrm{Term}(\mathrm{sig}, Z, s')$;
• $\mathrm{iter}(s', z)$ (with $z \in Z(s')$), applied to a single set $K$, yields $\mathrm{iterate}(z, K) := \bigcup_{i \in \mathbb{N}} \mathrm{iterStage}(z, K, i)$, where $\mathrm{iterStage}(z, K, 0) = \{\mathrm{var}(z)\}$ and $\mathrm{iterStage}(z, K, i+1) = \mathrm{iterStage}(z, K, i)\ \cup\ \mathrm{substP}\big(z,\ \mathrm{iterStage}(z, K, i),\ s',\ K\big)$;
• $\mathrm{plus}(s')$, applied to two sets $K_1, K_2$, yields $K_1 \cup K_2$;
• $\mathrm{subst}(t', s', z)$ (with $z \in Z(t')$), applied to a set $K_1$ of sort $t'$ and a set $K_2$ of sort $s'$, yields $\mathrm{substP}(z, K_1, s', K_2)$;

where $\mathrm{substP}(z, D, s', K) := \bigcup_{P \in K} g_{s'}(P)$, and $g$ is the homomorphism from the free $\mathrm{sig}$‑algebra on $Z$ into its power algebra induced by the variable assignment sending $z$ (at its own sort) to the set $D$ and every other variable $y$ (at any sort) to $\{\mathrm{var}(y)\}$; concretely $g_{s'}(P)$ is the set of all terms obtained from $P$ by replacing each occurrence of $z$ independently with an arbitrary element of $D$ while leaving every other variable unchanged, and $\mathrm{substP}$ takes the union of this over all $P \in K$. In particular $\mathrm{iterate}(z, K)$ is the set of terms reachable from $\mathrm{var}(z)$ by finitely many successive rounds of substituting elements of $K$ for $z$, and it always contains $\mathrm{var}(z)$ itself via stage $0$. The theorem asserts that for every such $S$, Finite S instance, $\mathrm{sig}$, $X$, proofs $\mathrm{hsig}$ and $\mathrm{hX}$, and sort $s$, and for every $L \subseteq \mathrm{Term}(\mathrm{sig}, X, s)$, the existence of the finite algebra $B$, homomorphism $f$, and subset $M$ above entails the existence of the auxiliary family $E$ and regular expression $R$ above.