Corollary 4.8: every regular language is recognizable

Read-back.

Fix a type $S$ of sorts in the lowest universe and assume $S$ is a finite type ([Finite S]). A signature $\mathrm{sig}$ assigns to every finite word $w \in \mathrm{List}\,S$ of argument sorts and every result sort $s' \in S$ a type $\mathrm{sig}\,w\,s'$ of operation symbols; a sorted set $A$ over $S$ assigns to every sort $s'$ a type $A_{s'}$. We are given such a signature $\mathrm{sig}$, a sorted set $X : S \to \mathrm{Type}$ of variables, a fixed sort $s \in S$, and two finiteness hypotheses:

i.e. altogether only finitely many operation symbols (over all arities and result sorts) and only finitely many variables (over all sorts). Let $\mathrm{Term}\,\mathrm{sig}\,X$ be the sorted set of well-sorted terms: a term of sort $s'$ is either $\mathrm{var}(x)$ with $x \in X_{s'}$, or $\mathrm{app}(\sigma,\vec t)$ with $\sigma \in \mathrm{sig}\,w\,s'$ and $\vec t$ a length-matching vector of terms of sorts $w$. Let $\mathcal F = \mathrm{freeAlgebra}\,\mathrm{sig}\,X$ be the term algebra, with carrier $s' \mapsto \mathrm{Term}\,\mathrm{sig}\,X\,s'$ and operations given by term formation.

The theorem asserts the set inclusion

where each side is a collection of subsets of $\mathrm{Term}\,\mathrm{sig}\,X\,s$; unfolded, the inclusion says: for every set of terms $L \subseteq \mathrm{Term}\,\mathrm{sig}\,X\,s$, if $L$ is sRegular then $L$ is sRecognizable, in the following senses.

$L$ is sRegular iff there exists a sorted set $E : S \to \mathrm{Type}$ of auxiliary variables such that, writing $X\oplus E$ for the sorted set $s' \mapsto X_{s'} \sqcup E_{s'}$: (1) $\sum_{s'} (X_{s'}\sqcup E_{s'})$ is a finite type; and (2) there exists a regular expression $R$ of sort $s$ over generators $X\oplus E$ with

where $\iota : x \mapsto \mathrm{inl}(x)$ is the left inclusion $X_{s'}\hookrightarrow X_{s'}\sqcup E_{s'}$ and $\mathrm{relabel}(\iota)$ renames every variable occurrence $x$ in a term to $\mathrm{inl}(x)$ leaving the term structure otherwise fixed (so the right-hand side is the image of $L$ under this renaming). Here a regular expression of sort $s$ over a generator set $Z$ is a term of sort $s$ with variables in $Z$ built from the operation symbols of the regular signature, which are: for each $\sigma \in \mathrm{sig}\,w\,s'$ a symbol $\mathrm{base}(\sigma)$ of arity $w \to s'$; for each sort $s'$ a nullary symbol $\mathrm{empty}(s')$; for each $z \in Z_{s'}$ a unary symbol $\mathrm{iter}(s',z)$ of arity $[s'] \to s'$; for each sort $s'$ a binary symbol $\mathrm{plus}(s')$ of arity $[s',s'] \to s'$; and for each pair of sorts $t,s'$ and each $z \in Z_t$ a binary symbol $\mathrm{subst}(t,s',z)$ of arity $[t,s'] \to s'$. The value $\mathrm{interpExpr}(\mathrm{sig},Z,s,R) \subseteq \mathrm{Term}\,\mathrm{sig}\,Z\,s$ is obtained by evaluating $R$ in the power-set algebra whose carrier at $s'$ is $\mathcal P(\mathrm{Term}\,\mathrm{sig}\,Z\,s')$, under the generator assignment $z \mapsto \{\mathrm{var}(z)\}$, with the regular symbols interpreted on subsets by:

• $\mathrm{base}(\sigma)$ sends $(L_1,\dots,L_k)$ to $\{\ \sigma(x_1,\dots,x_k)\ \mid\ x_i \in L_i\ \}$ (form the term $\sigma(\cdot)$ over all elementwise choices of members);
• $\mathrm{empty}(s')$ is $\varnothing \subseteq \mathrm{Term}\,\mathrm{sig}\,Z\,s'$;
• $\mathrm{iter}(s',z)$ sends $L_1$ to $\bigcup_{i\in\mathbb N}\Phi_i$, where $\Phi_0=\{\mathrm{var}(z)\}$ and $\Phi_{i+1}=\Phi_i\cup\mathrm{substP}(z,\Phi_i,s',L_1)$;
• $\mathrm{plus}(s')$ sends $(L_1,L_2)$ to $L_1\cup L_2$;
• $\mathrm{subst}(t,s',z)$ sends $(L_1,L_2)$ to $\mathrm{substP}(z,L_1,s',L_2)$;

where $\mathrm{substP}(z,L,s',K) = \bigcup_{P\in K} h_{z,L}(P)$, and $h_{z,L}$ is the homomorphism from $\mathcal F$ into its power-set algebra determined by the variable assignment sending $y$ (of sort $t'$) to $L$ when $t'$ is the sort of $z$ and $y = z$, and to $\{\mathrm{var}(y)\}$ otherwise; concretely, $\mathrm{substP}(z,L,s',K)$ is the set of all terms obtained from some $P \in K$ by replacing each occurrence of $z$, independently, with some element of $L$. Thus $\mathrm{iter}(s',z)$ applied to $L_1$ is the least set containing $\mathrm{var}(z)$ and closed under substituting members of $L_1$ for $z$.

$L$ is sRecognizable (for the algebra $\mathcal F$ and sort $s$) iff there exists a $\mathrm{sig}$-algebra $B$ such that: (1) $B$ is finite, meaning $\sum_{s'} B.\mathrm{carrier}_{s'}$ is a finite type; and (2) there exist a homomorphism of $\mathrm{sig}$-algebras $f : \mathcal F \to B$ (a sorted family of maps $f_{s'} : \mathrm{Term}\,\mathrm{sig}\,X\,s' \to B.\mathrm{carrier}_{s'}$ commuting with every operation of $\mathrm{sig}$) and a subset $M \subseteq B.\mathrm{carrier}_s$ with

Scope notes: the outer statement is a plain inclusion of families of subsets, hence a universally quantified implication over all $L \subseteq \mathrm{Term}\,\mathrm{sig}\,X\,s$; nothing constrains the auxiliary set $E$, the regular expression $R$, the recognizing algebra $B$, the homomorphism $f$, or the accepting subset $M$ beyond what is stated (in particular $E_{s'}$ may be empty at some or all sorts, provided $\sum_{s'}(X_{s'}\sqcup E_{s'})$ stays finite); the degenerate case $L = \varnothing$ is included and is sRegular (take $R = \mathrm{empty}(s)$) and sRecognizable (take $M = \varnothing$); if $S$ is empty there is no sort $s$ and the statement is vacuous; the $\mathrm{iter}$ interpretation always contains $\mathrm{var}(z)$ (the $i = 0$ stage) and its union ranges over all of $\mathbb N$; and the hypotheses hsig (SigFinite sig) and hX (SFinite X) are assumed but do not reappear explicitly in the conclusion.