The many-sorted Kleene theorem

Ambient data and hypotheses. Fix a type $S$ of sorts carrying a Finite instance, so $S$ has finitely many elements; it is moreover nonempty, since a sort $s : S$ is supplied as the last argument. A signature over $S$ is a family

$$\mathrm{sig} : \mathrm{List}\,S \to S \to \mathrm{Type},$$

so that for an argument–sort list $w = [w_1,\dots,w_k]$ and a result sort $r$, the type $\mathrm{sig}\,w\,r$ is the collection of operation symbols of that profile. A sorted variable family is $X : S \to \mathrm{Type}$, where $X\,r$ is the type of variables of sort $r$. Two finiteness hypotheses are assumed:

• $\mathtt{hsig} : \mathrm{SigFinite}\,\mathrm{sig}$, which unfolds to: the type $\sum_{w : \mathrm{List}\,S}\ \sum_{r : S}\ \mathrm{sig}\,w\,r$ of all triples (argument–sort list, result sort, operation symbol) is a finite type. Since $\mathrm{List}\,S$ is infinite, this forces $\mathrm{sig}\,w\,r$ to be empty for all but finitely many pairs $(w,r)$.
• $\mathtt{hX} : \mathrm{SFinite}\,X$, which unfolds to: the type $\sum_{r : S} X\,r$ of all (sort, variable-of-that-sort) pairs is a finite type.

Finally a specific sort $s : S$ is fixed.

Terms and the free algebra. $\mathrm{Term}\,\mathrm{sig}\,X$ is the $S$-indexed inductive family of well-sorted terms (defined mutually with tuples of terms): a term of sort $r$ is either $\mathrm{var}(x)$ for a variable $x : X\,r$, or $\mathrm{app}(\sigma;\,t_1,\dots,t_k)$ where $\sigma : \mathrm{sig}\,w\,r$ with $w = [w_1,\dots,w_k]$ and each $t_i : \mathrm{Term}\,\mathrm{sig}\,X\,w_i$. Write $\mathrm{Term}\,\mathrm{sig}\,X\,r$ for the type of sort-$r$ terms. The free (term) algebra $\mathcal F := \mathrm{freeAlgebra}\,\mathrm{sig}\,X$ is the $\mathrm{sig}$-algebra whose carrier at sort $r$ is $\mathrm{Term}\,\mathrm{sig}\,X\,r$ and which interprets every symbol $\sigma$ by term formation: $\sigma^{\mathcal F}(t_1,\dots,t_k) = \mathrm{app}(\sigma;\,t_1,\dots,t_k)$.

The objects being compared. Both sides of the asserted equation are subsets of the powerset $\mathcal P\big(\mathrm{Term}\,\mathrm{sig}\,X\,s\big)$, i.e. sets of languages of sort-$s$ terms. The theorem asserts that, for this fixed $s$, the two sets of languages coincide.

Left side — $\mathrm{RecS}(\mathcal F, s)$. This is

$$\big\{\,L \subseteq \mathrm{Term}\,\mathrm{sig}\,X\,s \ \big|\ \mathrm{sRecognizable}(\mathcal F, s, L)\,\big\},$$

and $\mathrm{sRecognizable}(\mathcal F, s, L)$ holds iff there exist:

• a $\mathrm{sig}$-algebra $\mathcal B$: a carrier $\mathcal B_\bullet : S \to \mathrm{Type}$ together with, for every $w, r$ and every $\sigma : \mathrm{sig}\,w\,r$, an operation $\sigma^{\mathcal B} : \mathcal B_{w_1}\times\cdots\times\mathcal B_{w_k} \to \mathcal B_r$;
• a proof that $\mathcal B$ is finite, meaning $\sum_{r : S}\mathcal B_r$ is a finite type;
• a homomorphism $f : \mathcal F \to \mathcal B$, i.e. a family of maps $f_r : \mathrm{Term}\,\mathrm{sig}\,X\,r \to \mathcal B_r$ satisfying, for every $\sigma : \mathrm{sig}\,w\,r$ and all arguments,

$$f_r\big(\mathrm{app}(\sigma;\,t_1,\dots,t_k)\big) = \sigma^{\mathcal B}\big(f_{w_1}(t_1),\dots,f_{w_k}(t_k)\big);$$

• a subset $M \subseteq \mathcal B_s$;

such that

$$f_s^{-1}(M) = L, \qquad\text{i.e.}\qquad L = \{\,t : \mathrm{Term}\,\mathrm{sig}\,X\,s \ \mid\ f_s(t) \in M\,\}.$$

The condition on $f$ constrains only its behaviour on $\mathrm{app}$-nodes; its values on variable terms $\mathrm{var}(x)$ are otherwise unconstrained.

Right side — $\mathrm{RegS}(\mathrm{sig}, X, s)$. This is

$$\big\{\,L \subseteq \mathrm{Term}\,\mathrm{sig}\,X\,s \ \big|\ \mathrm{sRegular}(\mathrm{sig}, X, s, L)\,\big\},$$

and $\mathrm{sRegular}(\mathrm{sig}, X, s, L)$ holds iff there exist:

• a sorted family of extra variables $E : S \to \mathrm{Type}$; put $Z := X \oplus E$, the sortwise disjoint sum, $Z\,r = X\,r \sqcup E\,r$;
• a proof of $\mathrm{SFinite}(Z)$, i.e. $\sum_{r : S}\big(X\,r \sqcup E\,r\big)$ is a finite type;
• a regular expression $R : \mathrm{RegExpr}\,\mathrm{sig}\,Z\,s$, which is by definition an ordinary term $R : \mathrm{Term}\,(\mathrm{regSig}\,\mathrm{sig}\,Z)\,Z\,s$ of sort $s$ over the variable family $Z$ and the regular signature $\mathrm{regSig}\,\mathrm{sig}\,Z = \mathrm{RegSym}\,\mathrm{sig}\,Z$, whose operation symbols of profile $(w, r)$ are exactly:
  • $\mathrm{base}(\sigma)$ for each $\sigma : \mathrm{sig}\,w\,r$ (same profile $(w,r)$),
  • $\mathrm{empty}(r)$, of profile $([\,],\,r)$ — a nullary symbol, one for every sort $r$,
  • $\mathrm{iter}(r, z)$, of profile $([r],\,r)$, parameterised by a chosen variable $z : Z\,r$,
  • $\mathrm{plus}(r)$, of profile $([r, r],\,r)$,
  • $\mathrm{subst}(t, r, z)$, of profile $([t, r],\,r)$, parameterised by a chosen variable $z : Z\,t$;

such that

$$\mathrm{interpExpr}\,\mathrm{sig}\,Z\,s\,(R) \;=\; \big\{\,\mathrm{relabel}(\iota)(t) \ \big|\ t \in L\,\big\},$$

where $\iota := \mathrm{extIncl}\,X\,E$ is the sortwise left injection $x \mapsto \mathrm{inl}(x) : X\,r \to Z\,r$, and $\mathrm{relabel}(\iota)$ renames every variable occurring in a term along $\iota$ while leaving the operation structure unchanged. Both sides of this equality are subsets of $\mathrm{Term}\,\mathrm{sig}\,Z\,s$ (terms over the extended variable family $Z$); $L$ enters only through its relabelled image.

Interpretation of regular expressions. $\mathrm{interpExpr}\,\mathrm{sig}\,Z\,s\,(R)$ is $(\mathrm{interp}\,\mathrm{sig}\,Z)_s(R)$, the value at $R$ of the evaluation homomorphism from the free algebra over $\mathrm{regSig}\,\mathrm{sig}\,Z$ with variables $Z$ into the algebra $\mathrm{regPowerAlgebra}\,\mathrm{sig}\,Z$, whose carrier at sort $r$ is $\mathcal P\big(\mathrm{Term}\,\mathrm{sig}\,Z\,r\big)$ and which sends each variable $z : Z\,r$ to the singleton language $\{\mathrm{var}(z)\}$. Unfolding the recursion, $\mathrm{interpExpr}(R) \subseteq \mathrm{Term}\,\mathrm{sig}\,Z\,s$ is:

• $R = \mathrm{var}(z)$ with $z : Z\,s$: value $\{\mathrm{var}(z)\}$;
• $R = \mathrm{base}(\sigma)(R_1,\dots,R_k)$ with $\sigma : \mathrm{sig}\,w\,s$: value $\big\{\,\mathrm{app}(\sigma;\,u_1,\dots,u_k) \ \mid\ u_i \in \mathrm{interpExpr}(R_i)\text{ for each }i\,\big\}$;
• $R = \mathrm{empty}(s)$: value $\varnothing$;
• $R = \mathrm{plus}(s)(R_1, R_2)$: value $\mathrm{interpExpr}(R_1)\cup\mathrm{interpExpr}(R_2)$;
• $R = \mathrm{iter}(s, z)(R_1)$ with $z : Z\,s$: value $\mathrm{iterate}\big(z,\ \mathrm{interpExpr}(R_1)\big)$;
• $R = \mathrm{subst}(t, s, z)(R_1, R_2)$ with $z : Z\,t$, $R_1$ of sort $t$, $R_2$ of sort $s$: value $\mathrm{substP}\big(z,\ \mathrm{interpExpr}(R_1),\ s,\ \mathrm{interpExpr}(R_2)\big)$.

The substitution operation. For $z : Z\,t$, a language $\Lambda \subseteq \mathrm{Term}\,\mathrm{sig}\,Z\,t$, a sort $r$, and a language $K \subseteq \mathrm{Term}\,\mathrm{sig}\,Z\,r$,

$$\mathrm{substP}(z, \Lambda, r, K) \;=\; \bigcup_{P \in K}\ \Theta_{z,\Lambda}(P),$$

where $\Theta_{z,\Lambda}(P) \subseteq \mathrm{Term}\,\mathrm{sig}\,Z\,r$ is the evaluation of the term $P$ in the powerset algebra of the term algebra under the variable assignment that sends the parameter variable $z$ to $\Lambda$ and every other variable $y$ to $\{\mathrm{var}(y)\}$. Concretely, $\Theta_{z,\Lambda}(P)$ is the set of all terms obtained from $P$ by replacing each occurrence of $z$ independently by some term of $\Lambda$ and leaving all other variables fixed; thus $\Theta_{z,\Lambda}(\mathrm{var}(z)) = \Lambda$, $\Theta_{z,\Lambda}(\mathrm{var}(y)) = \{\mathrm{var}(y)\}$ for $y \ne z$, and $\Theta_{z,\Lambda}$ distributes elementwise through $\mathrm{app}$.

The iteration operation. For $z : Z\,s$ and $\Lambda \subseteq \mathrm{Term}\,\mathrm{sig}\,Z\,s$, define stages over $i \in \mathbb N$ by

$$\mathrm{iterStage}(z,\Lambda,0) = \{\mathrm{var}(z)\},\qquad \mathrm{iterStage}(z,\Lambda,i{+}1) = \mathrm{iterStage}(z,\Lambda,i)\ \cup\ \mathrm{substP}\big(z,\ \mathrm{iterStage}(z,\Lambda,i),\ s,\ \Lambda\big),$$

and set $\mathrm{iterate}(z,\Lambda) = \bigcup_{i \in \mathbb N}\mathrm{iterStage}(z,\Lambda,i)$. In words: start from $\{\mathrm{var}(z)\}$; at each stage, for every term $P \in \Lambda$, substitute the terms produced so far into the $z$-occurrences of $P$, and accumulate.

The full assertion. For the fixed sort $s$, the theorem states equality of the following two subsets of $\mathcal P\big(\mathrm{Term}\,\mathrm{sig}\,X\,s\big)$: a language $L$ of sort-$s$ terms belongs to the left side iff there exist a $\mathrm{sig}$-algebra $\mathcal B$ with finite total carrier, a homomorphism $f : \mathcal F \to \mathcal B$, and a subset $M \subseteq \mathcal B_s$ with $L = f_s^{-1}(M)$; and $L$ belongs to the right side iff there exist an extra-variable family $E$ making $X \oplus E$ have finite total variable type, together with a regular expression $R$ over $\mathrm{regSig}\,\mathrm{sig}\,(X\oplus E)$ of sort $s$ whose interpreted language equals the $\iota$-relabelled image $\{\mathrm{relabel}(\iota)(t) : t \in L\}$. The equation asserts that membership in the left side holds precisely when membership in the right side does, with no further relationship imposed between the data $(E, R)$ and the data $(\mathcal B, f, M)$.

Degenerate and edge cases.

• $S$ is finite and, because $s : S$ is given, nonempty.
• $\mathtt{hX}$ allows $\sum_r X\,r$ to be empty, and $\mathtt{hsig}$ allows $\mathrm{sig}$ to have no operation symbols at all. If in addition no term of sort $s$ exists, then $\mathrm{Term}\,\mathrm{sig}\,X\,s$ is empty, $\mathcal P\big(\mathrm{Term}\,\mathrm{sig}\,X\,s\big) = \{\varnothing\}$, and the claim reduces to "$\varnothing$ lies on the left side iff it lies on the right side".
• In $\mathrm{sRegular}$ the family $E$ is unconstrained except that $\mathrm{SFinite}(X \oplus E)$ must hold; given $\mathtt{hX}$ this amounts to $\sum_r E\,r$ being finite. Every $E\,r$ may be empty, in which case $Z$ is $X$ up to the left injection $\iota$.
• The symbols $\mathrm{empty}$, $\mathrm{plus}$, $\mathrm{iter}$, $\mathrm{subst}$ are present in $\mathrm{regSig}\,\mathrm{sig}\,Z$ for every sort (respectively sort pair), independently of $\mathrm{sig}$. $\mathrm{plus}$ only ever combines two languages whose common sort equals the result sort.
• $R$ may be a bare variable $\mathrm{var}(z)$ with $z : Z\,s$, whose interpretation is the singleton $\{\mathrm{var}(z)\}$.
• $\mathrm{iterate}(z,\Lambda)$ always contains $\mathrm{var}(z)$ (from stage $0$), regardless of $\Lambda$; if $\Lambda = \varnothing$ then $\mathrm{substP}(z,\cdot,s,\varnothing) = \varnothing$ and $\mathrm{iterate}(z,\varnothing) = \{\mathrm{var}(z)\}$.
• $\mathcal B$ ranges over all $\mathrm{sig}$-algebras with finite total carrier (not only quotients of $\mathcal F$); $f$ is any homomorphism from the term algebra, its values on variable terms free.
• The equality inside $\mathrm{sRegular}$ is between subsets of $\mathrm{Term}\,\mathrm{sig}\,(X\oplus E)\,s$, i.e. terms over the extended variables, not over $X$.