Global substitution operator

substGlobalHom

Fix a universe level, a type $S$ whose elements are called sorts, a signature $sig$ over $S$ (implicitly), and an $S$-indexed family of variable types $X$ (implicitly); here $sig$ assigns to each list of sorts $w$ and each sort $s$ a type $sig\;w\;s$ of operation symbols with input profile $w$ and output sort $s$, and $X_s$ is the type of variables of sort $s$. Recall that $\mathrm{Term}(sig,X)_s$ is the type of well-sorted terms of sort $s$: every variable $x \in X_s$ gives a term $\mathrm{var}(x)$, and every symbol $\sigma \in sig\;w\;s$ together with a sort-indexed tuple of subterms whose sorts spell out $w$ gives a term $\mathrm{app}(\sigma,\dots)$. Let $F = \mathrm{freeAlgebra}(sig,X)$ be the term algebra, whose carrier at sort $s$ is $\mathrm{Term}(sig,X)_s$ and whose interpretation of a symbol $\sigma$ on an argument tuple is the term $\mathrm{app}(\sigma,\text{that tuple})$. Let $\mathcal{P}(F) = \mathrm{powerAlgebra}(F)$ be its power algebra, whose carrier at sort $s$ is the set of all subsets $L \subseteq \mathrm{Term}(sig,X)_s$ and whose interpretation of a symbol $\sigma \in sig\;w\;s$ on a tuple of sets $(L_1,\dots,L_k)$ (indexed by $w = [s_1,\dots,s_k]$) is

which for empty $w$ reduces to the singleton $\{\mathrm{app}(\sigma,())\}$ (the membership condition being vacuous). The definition takes one explicit argument $\rho$ that, for every sort $s$ and every variable $x \in X_s$, selects a set of terms $\rho_s(x) \subseteq \mathrm{Term}(sig,X)_s$. It returns the algebra homomorphism $F \to \mathcal{P}(F)$ given by the evaluation homomorphism into $\mathcal{P}(F)$ determined by $\rho$; write it $\Phi_\rho$. Its underlying sort-indexed map sends a term $t$ of sort $s$ to a subset $\Phi_{\rho,s}(t) \subseteq \mathrm{Term}(sig,X)_s$ defined by structural recursion: $\Phi_{\rho,s}(\mathrm{var}(x)) = \rho_s(x)$, and $\Phi_{\rho,s}(\mathrm{app}(\sigma,(t_1,\dots,t_k))) = \mathrm{powerOp}_F(\sigma)\big(\Phi_{\rho,s_1}(t_1),\dots,\Phi_{\rho,s_k}(t_k)\big)$, i.e. the set of all terms $\mathrm{app}(\sigma,(u_1,\dots,u_k))$ with each $u_i$ ranging over the recursively computed set $\Phi_{\rho,s_i}(t_i)$. As a homomorphism, $\Phi_\rho$ also carries the proof that for every symbol $\sigma \in sig\;w\;s$ and every tuple of term arguments $\bar t$, $\Phi_{\rho,s}(\mathrm{app}(\sigma,\bar t))$ equals $\mathrm{powerOp}_F(\sigma)$ applied to the tuple obtained by applying $\Phi_\rho$ componentwise to $\bar t$. The definition is marked noncomputable and has no further hypotheses.

substGlobalP

With the same implicitly fixed data (universe level, sort type $S$, signature $sig$, variable family $X$), this definition takes three explicit arguments: an assignment $\rho$ that for every sort $s$ and every variable $x \in X_s$ gives a set of terms $\rho_s(x) \subseteq \mathrm{Term}(sig,X)_s$ (the same argument as for $\mathrm{substGlobalHom}$), a sort $s \in S$, and a set $K \subseteq \mathrm{Term}(sig,X)_s$ of terms of sort $s$. It returns the set of terms of sort $s$

where $\Phi_\rho = \mathrm{substGlobalHom}(\rho)$ is the homomorphism described above and $\Phi_{\rho,s}$ is its component function at sort $s$. Equivalently, a term $y$ of sort $s$ belongs to $\mathrm{substGlobalP}(\rho,s,K)$ if and only if there exists a term $P$ with $P \in K$ and $y \in \Phi_{\rho,s}(P)$, where $\Phi_{\rho,s}(P)$ is the value that $\mathrm{substGlobalHom}(\rho)$ assigns to $P$, namely the evaluation of $P$ in the power algebra $\mathcal{P}(F)$ under $\rho$. In particular, when $K$ is empty the result is the empty set. The definition is marked noncomputable and carries no additional hypotheses.