$\mathbf{T}_\Sigma(Z)^{\wp}$ as a regular algebra; interpretation

regPowerAlgebra

This is a noncomputable definition. Fix an implicit type $S$ of sorts, an explicit signature $\Sigma$ over $S$ (so for every list of sorts $w$ and every sort $s$, $\Sigma_{w,s}$ is the type of operation symbols with input-sort-list $w$ and output sort $s$), and an explicit sort-indexed family of variables $Z\colon S \to \mathrm{Type}$. Write $\mathrm{Term}_\Sigma(Z)_s$ for the type of terms of sort $s$ built from $\Sigma$-operations and from variables taken from the families $Z_{s'}$; a term is either $\mathrm{var}(x)$ for some variable $x \in Z_s$, or $\mathrm{app}(\sigma, \bar t)$ applying an operation symbol $\sigma \in \Sigma_{w,s}$ to a tuple $\bar t$ of subterms matching $w$. The definition produces an algebra $\mathrm{regPowerAlgebra}\,\Sigma\,Z$ for the extended signature $\mathrm{regSig}\,\Sigma\,Z$, whose operation-symbol type at arity $w \to s$ is the inductive type $\mathrm{RegSym}\,\Sigma\,Z\,w\,s$ with exactly five constructors:

• $\mathrm{base}(\sigma)$ for any $\sigma \in \Sigma_{w,s}$, of arity $w \to s$;
• $\mathrm{empty}(s)$, of arity $[\,] \to s$;
• $\mathrm{iter}(s)$ carrying a variable $z \in Z_s$, of arity $[s] \to s$;
• $\mathrm{plus}(s)$, of arity $[s,s] \to s$;
• $\mathrm{subst}(t,s)$ carrying a variable $z \in Z_t$, of arity $[t,s] \to s$.

The carrier of $\mathrm{regPowerAlgebra}\,\Sigma\,Z$ at sort $s$ is $\mathrm{Set}\big(\mathrm{Term}_\Sigma(Z)_s\big)$, the type of arbitrary sets of $\Sigma$-terms of sort $s$ with variables in $Z$. The operation map takes an operation symbol of $\mathrm{regSig}\,\Sigma\,Z$ of arity $w \to s$ together with an argument tuple $\mathrm{args}$ that supplies, for each sort listed in $w$, a set of terms of that sort, and is defined by case analysis on the symbol:

• $\mathrm{base}(\sigma)$ with $\sigma \in \Sigma_{w,s}$: the result is $\big\{\, y \;\big|\; \exists\, \bar t \in \textstyle\prod_i (\text{$i$-th argument set}),\ \ y = \mathrm{app}(\sigma, \bar t) \,\big\},$ i.e. the set of all terms $\sigma(t_1,\dots,t_k)$ whose $i$-th immediate subterm ranges independently over the $i$-th argument set. (Membership of the tuple $\bar t$ in the product is checked componentwise; for $w = [\,]$ the condition is vacuously true, so the result is the singleton $\{\sigma()\}$.)
• $\mathrm{empty}(\_)$ at output sort $s$ (here $w = [\,]$): the result is the empty set $\varnothing \subseteq \mathrm{Term}_\Sigma(Z)_s$; the argument tuple is discarded.
• $\mathrm{iter}(\_)$ carrying a variable $z \in Z_s$ (arity $[s]\to s$): the result is $\mathrm{iterate}(z)(L)$, where $L$ is the single argument set (a set of $s$-sorted terms). By definition

$$\mathrm{iterate}(z)(L) \;=\; \bigcup_{i \in \mathbb{N}} G_i, \qquad G_0 = \{\mathrm{var}(z)\}, \qquad G_{i+1} = G_i \,\cup\, \mathrm{substP}(z)(G_i)(s)(L),$$

where $\mathrm{substP}$ is the substitution operator described in the $\mathrm{subst}$ bullet below (each stage $G_{i+1}$ adds all terms obtained by replacing occurrences of $z$ in terms of $G_i$ by elements of $L$). Because $G_0 = \{\mathrm{var}(z)\}$ is always included, $\mathrm{iterate}(z)(L)$ contains the bare-variable term $\mathrm{var}(z)$ for every $L$, including $L = \varnothing$.

• $\mathrm{plus}(\_)$ (arity $[s,s]\to s$): the result is $\mathrm{args}_1 \cup \mathrm{args}_2$, the ordinary set-theoretic union of the two argument sets (both sets of $s$-sorted terms).
• $\mathrm{subst}(\_,s)$ carrying a variable $z \in Z_t$ (arity $[t,s]\to s$, with the first sort $t$ recovered implicitly from the symbol): the result is $\mathrm{substP}(z)(\mathrm{args}_1)(s)(\mathrm{args}_2)$, where $\mathrm{args}_1 \subseteq \mathrm{Term}_\Sigma(Z)_t$ and $\mathrm{args}_2 \subseteq \mathrm{Term}_\Sigma(Z)_s$. Here

$$\mathrm{substP}(z)(L)(s)(K) \;:=\; \bigcup_{P \in K} H(P),$$

where $H$ is the underlying sorted map of the evaluation homomorphism from the free (term) algebra on $Z$ into the "power algebra" of that free algebra, induced by the assignment that sends a variable $y$ of sort $t'$ to the set $L$ when $t' = t$ and $y = z$, and to the singleton $\{\mathrm{var}(y)\}$ in every other case. Concretely $H(P)$ is the set of all terms obtained from $P$ by replacing each occurrence of the variable $z$ (of sort $t$) by some element of $L$, with the choice made independently at each occurrence, and leaving all other variables unchanged; $\mathrm{substP}$ then unions these sets over all $P$ in $K = \mathrm{args}_2$ (so if $K = \varnothing$ the result is $\varnothing$).

regGenAssign

This is a noncomputable definition with the same fixed data: an implicit sort type $S$, an explicit signature $\Sigma$ over $S$, and an explicit variable family $Z\colon S \to \mathrm{Type}$. It defines a sorted map $\mathrm{regGenAssign}\,\Sigma\,Z$ from the variable family $Z$ into the carrier family of the algebra $\mathrm{regPowerAlgebra}\,\Sigma\,Z$ (whose value at sort $s$ is $\mathrm{Set}(\mathrm{Term}_\Sigma(Z)_s)$). For each sort $s \in S$ and each variable $z \in Z_s$, the map returns the one-element set $\{\mathrm{var}(z)\} \subseteq \mathrm{Term}_\Sigma(Z)_s$, i.e. the singleton whose only member is the term consisting solely of the variable $z$. If $Z_s$ is empty for some $s$, the map at that sort is vacuous.

interp

This is a noncomputable definition with fixed data: an implicit sort type $S$, an explicit signature $\Sigma$ over $S$, and an explicit variable family $Z\colon S \to \mathrm{Type}$. It defines a homomorphism $\mathrm{interp}\,\Sigma\,Z$ of algebras over the signature $\mathrm{regSig}\,\Sigma\,Z$, with:

• domain $\mathrm{freeAlgebra}(\mathrm{regSig}\,\Sigma\,Z)(Z)$ — the free (term) algebra over the extended signature $\mathrm{regSig}\,\Sigma\,Z$ with variable family $Z$, whose carrier at sort $s$ is $\mathrm{Term}_{\mathrm{regSig}\,\Sigma\,Z}(Z)_s$ (the terms of sort $s$ over the extended signature, i.e. the "regular expressions" of sort $s$), and whose operation on symbol $\varsigma$ and argument tuple is $\mathrm{app}(\varsigma, \cdot)$;
• codomain $\mathrm{regPowerAlgebra}\,\Sigma\,Z$, the algebra of the previous definition (carrier $s \mapsto \mathrm{Set}(\mathrm{Term}_\Sigma(Z)_s)$, operations as spelled out there).

It is defined as $\mathrm{evalHom}(\mathrm{regPowerAlgebra}\,\Sigma\,Z)(\mathrm{regGenAssign}\,\Sigma\,Z)$: the evaluation homomorphism whose underlying sorted map sends a regular-expression term $R$ of sort $s$ to its value obtained by structural term-evaluation in $\mathrm{regPowerAlgebra}\,\Sigma\,Z$ under the generator assignment $\mathrm{regGenAssign}\,\Sigma\,Z$. Unfolding the recursion: a variable $z \in Z_s$ is sent to the singleton $\{\mathrm{var}(z)\}$; an application $\mathrm{app}(\varsigma, (R_1,\dots,R_k))$, with $\varsigma$ an operation symbol of $\mathrm{regSig}\,\Sigma\,Z$, is sent to the $\mathrm{regPowerAlgebra}$-interpretation of $\varsigma$ (elementwise application for $\mathrm{base}$, $\varnothing$ for $\mathrm{empty}$, the union $\bigcup_i G_i$ for $\mathrm{iter}$, set union for $\mathrm{plus}$, the operator $\mathrm{substP}$ for $\mathrm{subst}$ — exactly as described for regPowerAlgebra) applied to the recursively computed value-sets of $R_1,\dots,R_k$. The value produced is a full homomorphism structure, and hence also bundles the proof that this sorted map commutes with every operation symbol of $\mathrm{regSig}\,\Sigma\,Z$.

interpExpr

This is a noncomputable definition. It takes an implicit sort type $S$, an explicit signature $\Sigma$ over $S$, an explicit variable family $Z\colon S \to \mathrm{Type}$, an explicit sort $s \in S$, and an explicit argument $R : \mathrm{RegExpr}\,\Sigma\,Z\,s$, where $\mathrm{RegExpr}\,\Sigma\,Z\,s$ is by definition $\mathrm{Term}_{\mathrm{regSig}\,\Sigma\,Z}(Z)_s$ — a term of sort $s$ over the extended signature $\mathrm{regSig}\,\Sigma\,Z$ with variables drawn from $Z$. It returns

$$\mathrm{interpExpr}\,\Sigma\,Z\,s\,R \;=\; (\mathrm{interp}\,\Sigma\,Z).\mathrm{toFun}(s)(R) \;\subseteq\; \mathrm{Term}_\Sigma(Z)_s,$$

i.e. the image of $R$ under the underlying sorted map of the homomorphism $\mathrm{interp}\,\Sigma\,Z$ at sort $s$. Concretely this is the set of $\Sigma$-terms of sort $s$ over $Z$ obtained by recursively interpreting $R$ as in interp: singletons $\{\mathrm{var}(z)\}$ for variables, elementwise application for $\mathrm{base}$ symbols, $\varnothing$ for $\mathrm{empty}$, set union for $\mathrm{plus}$, the iterate-union $\bigcup_{i \in \mathbb{N}} G_i$ for $\mathrm{iter}$, and the substitution operator $\mathrm{substP}$ for $\mathrm{subst}$, applied bottom-up over the structure of $R$.