Sigma-Congruence

2020 Mathematics Subject Classification: Primary: 68P05 [MSN][ZBL]

A $\Sigma$-congruence is a congruence relation defined on a $\Sigma$-algebra. They provide a method to represent term-generated $\Sigma$-algebras using quotient algebras of the ground term algebra $T(\Sigma)$. Such methods are important for getting an overview of the (isomorphism classes of) possibly existing term-generated $\Sigma$-algebras, and thus for getting an overview of the possible semantical behaviours associated with the signature $\Sigma=(S,F)$.

Definition of $\Sigma$-congruences

Let $A$ be a $\Sigma$-algebra defined over a signature $\Sigma=(S,F)$. A $\Sigma$-congruence is an $S$-sorted equivalence relation $(\sim_s)_{s\in S}$ defined on $A$ with $\sim_s\subseteq s^A\times s^A$, which is compatible with the operations $f^A$, $f\in F$ of $A$. Compatibility means in this case that for each $f\in F$ with $\mathrm{type}(f)= s_1\times\cdots\times s_n \longrightarrow s$ and for each $x_i,y_i\in A_{s_i}$ with $x_i \sim_{s_i} y_i$ it holds $f^A(x_1,\ldots,x_n) \sim_s f^A(y_1,\ldots,y_n)$. If no reference to a specific $\Sigma$-algebra $A$ is made, the ground term algebra $T(\Sigma)$ is considered (under the assumption of a sensible signature $\Sigma$). The relation $\sim_s$ designates the restriction of $\sim$ to the sort $s\in S$.

For a $\Sigma$-algebra $A$, the set $C(A)$ of all $\Sigma$-congruences for $A$ forms a complete lattice w.r.t. set-theoretic inclusion [EM85][W90]. Its least element is the identity congruence $\sim^{T(A)} := \{(a,a)\mid a\in A\}$ over $A$. Its greatest element is the universal congruence $\sim^{U(A)} := \{(a,a')\mid a,a'\in s^A, s\in S\}$ over $A$. The least element $\sim^{T(A)}$ corresponds to the initial algebra $T(\Sigma)$ (i.e. the ground term algebra) of $\mathrm{Alg}(\Sigma)$ and $\mathrm{Gen}(\Sigma)$. The greatest element $\sim^{U(A)}$ corresponds to the terminal algebra $U(\Sigma)$ of $\mathrm{Alg}(\Sigma)$ and $\mathrm{Gen}(\Sigma)$ [W90].

For a $\Sigma$-algebra $A$ and a family $K=(\sim_i)_{i\in I}\subseteq C(A)$ of $\Sigma$-congruences defined on $A$, the infimum of $K$ coincides with the set-theoretic intersection, i.e. $(\bigcap\limits_{i\in I} (\sim_i)_s)_{s\in S} =\inf_{i\in I} \sim_i$ [EM85]. As an immediate consequence, the set-theoretic intersection of a family $(\sim_i)_{i\in I}$ of $\Sigma$-congruences is again a $\Sigma$-congruence defined on $A$. Furthermore, for an $S$-sorted binary relation $\approx\subseteq A\times A$ defined on $A$ there exists a least (with respect to $\subseteq$) $\Sigma$-congruence $\sim \in C(A)$ defined on $A$ whith $\approx\subseteq\sim$ [ST99].

Construction of $\Sigma$-Congruences

$\Sigma$-Congruences are directly related to $\Sigma$-algebra-morphism. It is possible to construct a $\Sigma$-congruence $\sim^m$ on a $\Sigma$-algebra $A$ using a $\Sigma$-algebra-morphism $m\colon A\longrightarrow B$ between $A$ and another $\Sigma$-algebra $B$. The $\Sigma$-congruence $\sim^m = (\sim^m_s)_{s\in S}$ is defined via $x\sim^m_s y :\Longleftrightarrow m_s(x)=m_s(y)$ for $x,y\in A$. It is called the $\Sigma$-congruence induced by $m$ [W90].

In the following, we consider a sensible signature $\Sigma$ for assuring the existence of the corresponding ground term algebra $T(\Sigma)$. For a $\Sigma$-algebra $A$, one can define an associated $\Sigma$-congruence $\sim^A\in C(T(\Sigma))$ by $t_1\sim^A t_2 \colon\Longleftrightarrow t_1^A = t_2^A$ for $t_1,t_2\in T_s(\Sigma)$, $s\in S$. In particular, any $\Sigma$-congruence $\sim\in C(X)$ is associated with $T(\Sigma)/\sim$ [W90].

Application I: Quotient Algebras

The identification of terms $t,t'\in T(\Sigma)$ related to each other by a $\Sigma$-congruence leads to so-called quotient $\Sigma$-algebras of the ground term algebra $T(\Sigma)$. Each term-generated $\Sigma$-algebra can be represented in this way. Formally, a quotient algebra is defined ion the following way.

Let $\sim \in C(A)$ be a $\Sigma$-congruence defined on a $\Sigma$-algebra $A$. Then the quotient $\Sigma$-algebra $A/\sim$ is defined as follows [M89].

• $s^{A/\sim} :=\{[a]_\sim\mid a\in s^A\}$
• $f^{A/\sim} := [f^A]_\sim$ for $f\in F$ with $\mathrm{type}(f)=\,\,\rightarrow s\}$
• $f^{A/\sim}([a_1],\ldots,[a_n]) := [f^A(a_1,\ldots,a_n)]$, $f\in F$, with $\mathrm{type}(f)= s_1\times\cdots\times s_n \longrightarrow s$ and for $a_i\in s_i^A$.

$A/\sim \in \mathrm{Alg}(\Sigma)$ is a $\Sigma$-algebra. Its definition is well-defined because of the congruence property of $\sim$ [EM85]. Corresponding to $A/\sim$, one can define mappings $m_s\colon s^A \longrightarrow s^A/\sim_s; a \mapsto [a]_{\sim_s}$ for $s \in S$. Then $m=(m_s)_{s\in S} \colon A \longrightarrow A/\sim$ is a surjective $\Sigma$-algebra-morphism [M89]. It has the following universal property: Let $B$ be a $\Sigma$-algebra and $f\colon A\longrightarrow B$ be a $\Sigma$-algebra-morphism with $\sim \subseteq \sim_f$. Then there is a unique $\Sigma$-algebra-morphism $\bar f \colon A/\sim\longrightarrow B$ such that $f_s(a) = \bar f_s([a]_{\sim_s})$ for all $s \in S$ and $a \in s^A$. If $\sim = \sim_f$ then $\bar f$ is injective [EM85]. If $f$ is surjective, then $B\cong A/\sim^m$ [M89].

The above property characterizes quotient algebras up to isomorphism. It follows in particular that for any $\Sigma$-algebra-morphism $m\colon A \longrightarrow B$, $A/\sim_m$ is isomorphic to the image $m(A)$ of $A$ under $m$ [ST99].

Application II: Term-generated $\Sigma$-Algebras

An application of $\Sigma$-congruences is the representation of a term-generated $\Sigma$-algebra using the ground term algebra $T(\Sigma)$ in the case of a sensible signature $\Sigma$. Together with $\Sigma$-algebra-morphism, one has two different options to describe a term-generated $\Sigma$-algebra $A$ in this way. More precisely, we can state that a $\Sigma$-algebra $A$ is term-generated iff it is isomorphic to a quotient algebra $T(\Sigma)/\sim$ of the ground term algebra $T(\Sigma)$ with $\sim=\sim^A$ [W90]. This is the case, in turn, iff it is the image of $T(\Sigma)$ under a $\Sigma$-algebra-morphism.

It follows that there is a one-to-one correspondence between isomorphism classes of term-generated $\Sigma$-algebras and congruences on $T(\Sigma)$ [ST99]. Especially, for term-generated $\Sigma$-algebras $A,B$ it holds $A\cong B$ iff $\sim^A= \sim^B$ [W90]. For a term-generated $\Sigma$-algebra $A$ and for a $\Sigma$-algebra $B$, it exists a $\Sigma$-morphism $m\colon A\longrightarrow B$ iff $\sim^A\subseteq \sim^B$ [W90].

References

[EM85]	H. Ehrig, B. Mahr: "Fundamentals of Algebraic Specifications", Volume 1, Springer 1985
[EM90]	H. Ehrig, B. Mahr: "Fundamentals of Algebraic Specifications", Volume 2, Springer 1990
[M89]	B. Möller: "Algorithmische Sprachen und Methodik des Programmierens I", lecture notes, Technical University Munich 1989
[ST99]	D. Sannella, A. Tarlecki, "Algebraic Preliminaries", in Egidio Astesiano, Hans-Joerg Kreowski, Bernd Krieg-Brueckner, "Algebraic Foundations of System Specification", Springer 1999
[W90]	M. Wirsing: "Algebraic Specification", in J. van Leeuwen: "Handbook of Theoretical Computer Science", Elsevier 1990