The $z$-substitution operators

substAssign

Fix a universe level, a type $S$ whose elements are called sorts, a signature $\Sigma$ over $S$ (for every list $w$ of argument sorts and every result sort $s$, $\Sigma_{w,s}$ is the type of operation symbols of that profile), and an $S$-indexed family of types $X=(X_s)_{s\in S}$ playing the role of typed variables ($X_s$ is the type of variables of sort $s$). Write $\mathrm{Term}_{\Sigma,X}(s)$ for the type of well-sorted terms of sort $s$: a term is either $\mathrm{var}(y)$ for some $y\in X_s$, or $\mathrm{app}(\sigma;\,t_1,\dots,t_k)$ where $\sigma\in\Sigma_{w,s}$ with $w=[w_1,\dots,w_k]$ and each $t_i$ is a term of sort $w_i$. The data $S$, $\Sigma$, $X$ and a further sort $v\in S$ are implicit arguments; the explicit arguments are a variable $z\in X_v$ and an arbitrary set $L$ of terms of sort $v$ (no restriction: $L$ may be empty, may contain $\mathrm{var}(z)$, etc.). The declaration substAssign z L is a sort-indexed function that assigns, to every sort $t\in S$ and every variable $y\in X_t$, a set of terms of sort $t$, namely

The two comparisons involved (the sort equality $t=v$, and after identifying $t$ with $v$ the variable equality $y=z$) are decided using classical logic, and the definition is marked noncomputable. Its stated codomain is the carrier, at sort $t$, of the power algebra of the free term algebra, which is definitionally $\mathrm{Set}\big(\mathrm{Term}_{\Sigma,X}(t)\big)$.

substHom

With the same implicit data $S,\Sigma,X,v$ and the same explicit arguments $z\in X_v$ and $L\subseteq\mathrm{Term}_{\Sigma,X}(v)$, this declaration produces a homomorphism of $\Sigma$-algebras

where $\mathrm{Free}(\Sigma,X)$ is the free term algebra (carrier $s\mapsto\mathrm{Term}_{\Sigma,X}(s)$, with operation $\mathrm{op}(\sigma;\,t_1,\dots,t_k)=\mathrm{app}(\sigma;\,t_1,\dots,t_k)$), and $\mathcal P\big(\mathrm{Free}(\Sigma,X)\big)$ is the power algebra over it: its carrier at sort $s$ is $\mathrm{Set}\big(\mathrm{Term}_{\Sigma,X}(s)\big)$, and for $\sigma\in\Sigma_{w,s}$ with $w=[w_1,\dots,w_k]$ and a tuple of sets $(M_1,\dots,M_k)$ with $M_i\subseteq\mathrm{Term}_{\Sigma,X}(w_i)$ its operation is the complex product

The homomorphism is defined as the canonical evaluation homomorphism out of the free algebra induced by the assignment $\operatorname{substAssign}(z,L)$. It bundles two pieces of data. First, an underlying sort-indexed function $\Phi_s:\mathrm{Term}_{\Sigma,X}(s)\to\mathrm{Set}\big(\mathrm{Term}_{\Sigma,X}(s)\big)$, characterized by structural recursion:

• $\Phi_s(\mathrm{var}(y))=\operatorname{substAssign}(z,L)_s(y)$, i.e. $L$ when $s=v$ and $y=z$, and $\{\mathrm{var}(y)\}$ otherwise;
• $\displaystyle\Phi_s\big(\mathrm{app}(\sigma;\,t_1,\dots,t_k)\big)=\big\{\,u \ \big|\ \exists\, x_1\in\Phi_{w_1}(t_1),\dots,\exists\, x_k\in\Phi_{w_k}(t_k),\ \ u=\mathrm{app}(\sigma;\,x_1,\dots,x_k)\,\big\}$ for $\sigma\in\Sigma_{w,s}$, $w=[w_1,\dots,w_k]$.

Second, a proof of the homomorphism law: for every operation symbol $\sigma\in\Sigma_{w,s}$ and every tuple of argument terms $(t_1,\dots,t_k)$, $\Phi_s\big(\mathrm{app}(\sigma;\,t_1,\dots,t_k)\big)$ equals the power-algebra operation applied to the tuple of images $(\Phi_{w_1}(t_1),\dots,\Phi_{w_k}(t_k))$. The construction is noncomputable and uses classical logic (inherited from $\operatorname{substAssign}$).

substP

With the same implicit data $S,\Sigma,X,v$, the explicit arguments are a variable $z\in X_v$, a set $L\subseteq\mathrm{Term}_{\Sigma,X}(v)$, a sort $s\in S$, and a set $K\subseteq\mathrm{Term}_{\Sigma,X}(s)$. The result substP z L s K is the set of terms of sort $s$ obtained as the indexed union, over all terms $P$ lying in $K$, of the sets produced by the map $\Phi_s$ from substHom:

where $(\operatorname{substHom}(z,L)).\mathrm{toFun}_s=\Phi_s$ is the recursively-defined function described above. In particular, if $K=\emptyset$ the union is the empty set. No hypotheses beyond the stated typing are imposed on any argument, and the definition is noncomputable.