The regular signature $\mathrm{Reg}(S,\Sigma,Z)$

RegSym

RegSym is an inductive family of types. Its ambient data are: an implicit sort type $S$ in universe $u$; an explicit sig : Signature S, where Signature S unfolds by definition to $\mathrm{List}\,S \to S \to \mathrm{Type}\,u$ (so sig assigns to each arity $w$ — a finite list of sorts — and each result sort $s$ a type $sig\;w\;s$ of operation symbols); and an explicit Z : SSet S, where SSet S unfolds to $S \to \mathrm{Type}\,u$ (so $Z$ assigns a type $Z_s$ to each sort $s$). For fixed sig and Z, the family RegSym sig Z has type $\mathrm{List}\,S \to S \to \mathrm{Type}\,u$, i.e. it is itself a signature over $S$; for an arity $w$ and result sort $s$ the type RegSym sig Z w s is generated by exactly the following constructors:

• base: from an implicit $w : \mathrm{List}\,S$, an implicit $s : S$, and an element of $sig\;w\;s$, produces an element of RegSym sig Z w s — same arity $w$, same result sort $s$.
• empty: for every explicit $s : S$, an element of RegSym sig Z [] s — arity the empty list $[\,]$, result sort $s$.
• iter: for every explicit $s : S$ and every element of $Z_s$, an element of RegSym sig Z [s] s — arity the one-element list $[s]$, result sort $s$.
• plus: for every explicit $s : S$, an element of RegSym sig Z [s, s] s — arity the two-element list $[s,s]$, result sort $s$.
• subst: for every pair of explicit sorts $t, s : S$ and every element of $Z_t$, an element of RegSym sig Z [t, s] s — arity the two-element list $[t,s]$, result sort $s$.

There are no other constructors. Note the edge behavior: empty and plus produce a symbol for every sort unconditionally; iter at sort $s$ produces symbols only insofar as $Z_s$ has elements (none if $Z_s$ is empty); subst with argument sorts $(t,s)$ produces symbols only insofar as $Z_t$ has elements; and base embeds the symbols of sig at every arity and result sort, one base-symbol per sig-symbol.

regSig

regSig takes an implicit sort type $S$, an explicit sig : Signature S (assigning a type of operation symbols to each arity $w$ and result sort $s$), and an explicit Z : SSet S (assigning a type $Z_s$ to each sort $s$), and returns a term of type Signature S, namely the family $\mathrm{RegSym}\;sig\;Z$. Thus $\mathrm{regSig}\;sig\;Z$ is the signature whose symbols of arity $w$ and result sort $s$ are precisely the elements of RegSym sig Z w s as described above (the base copies of sig's symbols together with the empty, iter, plus, and subst symbols). This is a purely definitional repackaging: no data is added or removed.

RegExpr

RegExpr is an abbreviation. Given an implicit sort type $S$, an explicit sig : Signature S, an explicit Z : SSet S, and an explicit sort s : S, the type RegExpr sig Z s (in $\mathrm{Type}\,u$) unfolds to Term (regSig sig Z) Z s. Here Term σ X is the mutually-inductive family of terms over a signature $\sigma$ with variables drawn from a sorted set $X$: a value at sort $s$ is either a variable var x with $x \in X_s$, or an application app f ts of a symbol $f$ of $\sigma$ of arity $w$ and result sort $s$ to a vector ts of subterms whose sorts match the list $w$. Therefore a RegExpr sig Z s is a term of result sort $s$ whose variables are elements of the $Z_s$ families and whose operation nodes are labelled by regular symbols of $\mathrm{regSig}\;sig\;Z = \mathrm{RegSym}\;sig\;Z$ (i.e. base σ, empty, iter, plus, or subst).

Term.relabel

Term.relabel is one of two functions defined together by mutual structural recursion (with TermVec.relabel). It takes an implicit sort type $S$, an implicit sig : Signature S, two implicit sorted sets X Y : SSet S, and an explicit ι : SMap X Y, where SMap X Y unfolds to $(s : S) \to X_s \to Y_s$ — a family of functions $\iota_s : X_s \to Y_s$, one per sort. It then takes an implicit sort $s : S$ and a value of Term sig X s, and returns a value of Term sig Y s (same signature sig, same result sort $s$, but with variables now taken from $Y$). It is defined by cases on the input term:

• on a variable var x with $x \in X_s$, it returns var (ι s x), the variable $\iota_s(x) \in Y_s$;
• on an application app σ ts, where $\sigma$ is a symbol of sig of arity $w$ and result sort $s$ and ts is of type TermVec sig X w, it returns app σ (TermVec.relabel ι ts) — the same symbol $\sigma$ applied to the argument vector obtained by recursively relabelling ts.

TermVec.relabel

TermVec.relabel is the companion of Term.relabel in the same mutual block. With the same implicit data (sort type $S$, sig : Signature S, sorted sets X Y : SSet S) and the same explicit ι : SMap X Y (the family $\iota_s : X_s \to Y_s$), it takes an implicit arity w : List S and a value of TermVec sig X w, and returns a value of TermVec sig Y w. Here TermVec sig X w is the type of finite tuples of terms indexed by the list of sorts $w$: the constructor nil gives the empty tuple at arity $[\,]$, and cons t ts gives, at arity $s :: w$, a tuple whose head t has type Term sig X s and whose tail ts has type TermVec sig X w. The definition:

• on nil, it returns nil;
• on cons t ts, it returns cons (Term.relabel ι t) (TermVec.relabel ι ts) — relabel the head term via Term.relabel and recursively relabel the tail vector.

Term.toReg

Term.toReg is one of two functions defined together by mutual structural recursion (with TermVec.toReg). It takes an implicit sort type $S$, an implicit sig : Signature S, and an implicit Z : SSet S; then an implicit sort $s : S$ and a value of Term sig Z s — a term over the signature sig whose variables are elements of the $Z_s$ families, of result sort $s$. It returns a value of RegExpr sig Z s, which unfolds to Term (regSig sig Z) Z s — a term over the signature $\mathrm{regSig}\;sig\;Z = \mathrm{RegSym}\;sig\;Z$, with the same variable family $Z$ and the same result sort $s$. It is defined by cases:

• on a variable var x with $x \in Z_s$, it returns var x — the same variable, now regarded as a variable in the term family over $\mathrm{regSig}\;sig\;Z$;
• on an application app σ ts, where $\sigma$ is a symbol of sig of arity $w$ and result sort $s$ and ts is of type TermVec sig Z w, it returns app (RegSym.base σ) (TermVec.toReg ts) — the symbol $\sigma$ re-tagged through the base constructor as a symbol of RegSym sig Z w s, applied to the argument vector obtained by recursively converting ts.

TermVec.toReg

TermVec.toReg is the companion of Term.toReg in the same mutual block. With implicit sort type $S$, implicit sig : Signature S, and implicit Z : SSet S, it takes an implicit arity w : List S and a value of TermVec sig Z w, and returns a value of TermVec (regSig sig Z) Z w — the argument-vector type over the regular signature $\mathrm{regSig}\;sig\;Z$, with the same list of sorts $w$ and the same variable family $Z$. It is defined by cases:

• on nil, it returns nil;
• on cons t ts, it returns cons (Term.toReg t) (TermVec.toReg ts) — convert the head term via Term.toReg and recursively convert the tail vector.