The $s$-regular languages $\mathrm{Reg}_s(\mathbf{T}_\Sigma(X))$

extVars

Working over an implicit type of sorts $S$, this defines, from two $S$-indexed families of types $X, E : S \to \mathrm{Type}$ (each is a "sorted set" over $S$, both passed as explicit arguments), a new sorted set $\mathrm{extVars}\ X\ E : S \to \mathrm{Type}$. Its value at a sort $s$ is the disjoint-sum (coproduct) type $X_s \oplus E_s$. Intuitively it enlarges the variable family $X$ by adjoining, sort by sort, the extra variables $E$.

extIncl

Again over an implicit sort type $S$, and given two sorted sets $X, E : S \to \mathrm{Type}$ (both explicit), this defines a sorted map $\mathrm{extIncl}\ X\ E$ from $X$ to $\mathrm{extVars}\ X\ E$, i.e. a family of functions indexed by sorts. At every sort $s$ it is the function $x \mapsto \mathrm{inl}\ x$ sending each $x : X_s$ to the left injection $\mathrm{inl}\ x : X_s \oplus E_s$. The sort index is not otherwise used. This is the canonical inclusion of the original variables into the enlarged family, and it is injective.

sRegular

Over an implicit sort type $S$, this defines a predicate $\mathrm{sRegular}\ sig\ X\ s\ L$ of four explicit arguments: a signature $sig : \mathrm{List}\ S \to S \to \mathrm{Type}$ (which assigns to each input word $w$ and output sort $s'$ a type of operation symbols of that arity), a sorted set of variables $X : S \to \mathrm{Type}$, a distinguished sort $s : S$, and a set $L$ of terms of sort $s$ built from $sig$ with variables taken from $X$, i.e. $L \subseteq \mathrm{Term}\ sig\ X\ s$ (a set given by an arbitrary total predicate, so it may be empty or the whole type). The predicate asserts that there exists a sorted set $E : S \to \mathrm{Type}$ of "extension variables" satisfying both of the following.

Finiteness. $\mathrm{SFinite}(\mathrm{extVars}\ X\ E)$ holds, which unfolds to: the dependent sum

$$\sum_{s' : S}\bigl(X_{s'} \oplus E_{s'}\bigr)$$

is a finite type. That is, the disjoint union over all sorts of the original variables together with the extension variables is finite. Consequently $\sum_{s':S} X_{s'}$ must itself be finite; if the original variable space is infinite, no witness $E$ exists and the predicate is false for every $L$. The sort type $S$ need not be finite.

Denotation by a regular expression. There exists an expression

$$R : \mathrm{RegExpr}\ sig\ (\mathrm{extVars}\ X\ E)\ s,$$

which by definition is a term of sort $s$ over the enlarged signature $\mathrm{regSig}\ sig\ (\mathrm{extVars}\ X\ E)$ with variables in $\mathrm{extVars}\ X\ E$. The operation symbols of this enlarged signature, at input word $w$ and output sort $s'$, are: every original symbol of $sig\ w\ s'$ ("base"); one nullary symbol at each sort ("empty"); for each variable $z : (\mathrm{extVars}\ X\ E)_{s'}$ a unary symbol $[s'] \to s'$ ("iter"); one binary symbol $[s', s'] \to s'$ ("plus"); and for every pair of sorts $t, s'$ and every variable $z : (\mathrm{extVars}\ X\ E)_t$ a binary symbol $[t, s'] \to s'$ ("subst"). This expression $R$ must satisfy

$$\mathrm{interpExpr}\ sig\ (\mathrm{extVars}\ X\ E)\ s\ R \;=\; \bigl\{\, \mathrm{relabel}(\iota)(t) \;\bigm|\; t \in L \,\bigr\},$$

an equality of subsets of $\mathrm{Term}\ sig\ (\mathrm{extVars}\ X\ E)\ s$. Here $\iota = \mathrm{extIncl}\ X\ E$, and $\mathrm{relabel}(\iota)(t)$ is the term obtained from $t$ by replacing every variable occurrence $x$ (at any sort) by $\mathrm{inl}\ x$, while leaving all applied-operation structure unchanged; the right-hand side is the set-image of $L$ under this relabeling. Because $\iota$ is injective, the right-hand side is a faithful copy of $L$ with all its variables re-tagged as "left". $E$ is permitted to be the empty family (each $E_{s'}$ an empty type), in which case $\mathrm{extVars}\ X\ E$ is essentially $X$ itself.

Meaning of the left-hand side. $\mathrm{interpExpr}\ sig\ Z\ s\ R$, with $Z = \mathrm{extVars}\ X\ E$, is the subset of $\mathrm{Term}\ sig\ Z\ s$ obtained by recursively evaluating the expression tree $R$ in the power-set algebra over the free $sig$-algebra on $Z$ (carrier at sort $s'$ equal to $\{\,$subsets of $\mathrm{Term}\ sig\ Z\ s'\,\}$), under the assignment sending each variable $z : Z_{s'}$ to the singleton $\{\mathrm{var}\ z\}$. The node symbols are interpreted as follows:

• a "base" node with original symbol $\sigma : sig\ w\ s'$ applied to argument sets $L_1, \dots, L_k$ yields $\{\, \mathrm{app}\ \sigma\ (t_1, \dots, t_k) \mid t_i \in L_i \text{ for all } i \,\}$;
• an "empty" node at sort $s'$ yields $\varnothing$;
• a "plus" node applied to sets $A$ and $B$ yields $A \cup B$;
• an "iter" node carrying variable $z : Z_{s'}$ applied to a set $A \subseteq \mathrm{Term}\ sig\ Z\ s'$ yields $\bigcup_{i \in \mathbb{N}} \mathrm{iterStage}(z, A, i)$, where $\mathrm{iterStage}(z, A, 0) = \{\mathrm{var}\ z\}$ and $\mathrm{iterStage}(z, A, i{+}1) = \mathrm{iterStage}(z, A, i)\ \cup\ \mathrm{substP}\bigl(z,\, \mathrm{iterStage}(z, A, i),\, s',\, A\bigr)$;
• a "subst" node carrying variable $z : Z_t$ applied to a set $A \subseteq \mathrm{Term}\ sig\ Z\ t$ and a set $K \subseteq \mathrm{Term}\ sig\ Z\ s'$ yields $\mathrm{substP}(z, A, s', K) = \bigcup_{P \in K} \mathrm{substHom}(z, A)(P)$, i.e. the union over $P \in K$ of all terms obtained from $P$ by replacing every occurrence of the variable $z$ with (members of) $A$, other variables being left as themselves.

RegS

Over an implicit sort type $S$, and given explicit arguments a signature $sig$, a sorted set of variables $X$, and a sort $s : S$, this defines $\mathrm{RegS}\ sig\ X\ s$ as the set of all sets $L$ of $sig$-terms of sort $s$ with variables in $X$ — that is, all $L \subseteq \mathrm{Term}\ sig\ X\ s$ — for which $\mathrm{sRegular}\ sig\ X\ s\ L$ holds. It is thus a subset of the powerset of $\mathrm{Term}\ sig\ X\ s$: the collection of those term-languages at sort $s$ that are "$s$-regular" in the sense of the predicate above.