User:Joachim Draeger/sandbox

$\Sigma$-Algebra

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

$\Sigma$-Algebras are the semantical counterpart to the signatures, which are pure syntactical objects. In order to give the function symbols $f\in F$ of a signature $\Sigma=(S,F)$ a meaning, a (total) $\Sigma$-algebra provides an object with the same structure as $\Sigma$ but consisting of concrete elements and concrete functions operating on these elements. The elements and functions of a $\Sigma$-algebra are the counterparts to the sorts and function symbols of the signature $\Sigma$.

Definition of $\Sigma$-Algebras

Formally, a $\Sigma$-algebra $A=((s^A)_{s\in S},(f^A)_{f\in F})$ consists of a family $(s^A)_{s\in S}$ of carrier sets $s^A$ corresponding to the sorts $s\in S$ and a family $(f^A)_{f\in F}$ of functions on these carrier sets corresponding to the function symbols $f\in F$. The compatibility requirement is that for a function symbol $f$ of type$(f)= s_1\times\cdots\times s_n \longrightarrow s$, the function $f^A$ must have the form $f^A\colon s_1^A\times\cdots\times s_n^A \longrightarrow s^A$.

Category of $\Sigma$-Algebras

Let $\Sigma=(S,F)$ be a signature and let $A,B$ be $\Sigma$-algebras. A $\Sigma$-algebra-morphism $m\colon A\longrightarrow B$ is a family $(m_s\colon s^A \longrightarrow s^B)_{s\in S}$ of mappings between the carrier sets of $A,B$ fulfilling the following compatibility properties

• $m_s(f^A)= f^B$ for $f\in F$ with ar$(f)=0$ and $\mathrm{type}(f)=\,\, \rightarrow s\}$
• $m_s(f^A(a_1,\ldots,a_n))=f^B(m_{s_1}(a_1),\ldots,m_{s_n}(a_n))$ for $f\in F$ with $\mathrm{type}(f)= s_1\times\cdots\times s_n \longrightarrow s$ and for $a_i\in s_i^A$.

The class of $\Sigma$-algebras together with the $\Sigma$-algebra-morphisms forms a category [W90].

The option to use partially defined functions complicates the situation considerably and leads to refined versions of the definition. Though this does not belong to the scope of this entry, a short remarks seems to be appropriate. For example it is possible under this generalization that $m_s(f^A(a_1,\ldots,a_n))$ is undefined though $f^A(a_1,\ldots,a_n)$ is defined. This can be caused by an undefinedness of a term $m_{s_j}(a_j)$ or of $f^B(m_{s_1}(a_1),\ldots,m_{s_n}(a_n))$ [M89].

$\Sigma$-Subalgebras

One can easily imagine that typically many different $\Sigma$-algebras exist for the same signature $\Sigma$. This holds even in the case of algebraic specifications, which can restrict the set of admissable $\Sigma$-algebras by additional axioms. In effect, this means that an abstract signature $\Sigma$ can be 'implemented' by concrete $\Sigma$-algebras with different semantics. This leads to an interest in the relationships between these $\Sigma$-algebras. One method to discuss the relationships is to use $\Sigma$-algebra-morphisms, another is the notion of $\Sigma$-subalgebras.

$\Sigma$-Subalgebras of $\Sigma$-algebras are defined in the usual way. A $\Sigma$-Algebra $A$ is called a $\Sigma$-subalgebra of a $\Sigma$-Algebra $B$, if $\forall s\in S\colon s^A\subseteq s^B$ and if $f^A(a_1,\ldots,a_n) = f^B(a_1,\ldots,a_n)$ for $f\in F$ with $\mathrm{type}(f)= s_1\times\cdots\times s_n \longrightarrow s$ and for $a_i\in s_i^A$. The subalgebra-property is written as $A\subseteq B$.

Another way to characterize the subalgebra-property is the existence of a $\Sigma$-algebra-morphism $m\colon A\longrightarrow B$, which is the identity on each carrier set of $A$, i.e. $m=(\mathrm{id}_{s^A})_{s\in S}$.

(Carriers of) $\Sigma$-Subalgebras are closed under intersection. For a family $((s^{A_i})_{s\in S},(f^{A_i})_{f\in F})_{i\in I}$ of $\Sigma$-subalgebras $A_i$, their intersection $A=((s^{A})_{s\in S}, (f^{A})_{f\in F})$ is a $\Sigma$-subalgebra given by carrier sets $s^A:= \bigcap\limits_{i\in I} s^{A_i}$ for all $s\in S$ and functions $f^A:= f^{A_k}|_{s^A}$ for all $f\in F$ for an arbitrarily chosen $k\in I$. The declaration $f^A$ is well-defined, because according to the definition of a $\Sigma$-subalgebra the functions $f^{A_i}$ must behave in the same way on $s^A$.

The closedness of the set of $\Sigma$-subalgebras under intersections has an important consequence. For a $\Sigma$-algebra $A=((s^A)_{s\in S}, (f^A)_{f\in F})$ and an $S$-sorted set $X=(\bar s)_{s\in S}$ with $\bar s\subseteq s^A$ for all $s\in S$, it assures the existence of a smallest $\Sigma$-subalgebra $A'\subseteq A$ of $A$ containing $X$, i.e. $\bar s\subseteq s^{A'}$. The $\Sigma$-algebra $A'$ is called the $\Sigma$-subalgebra of $A$ generated by $X$ [ST99].

The subalgebra-property is compatible with $\Sigma$-algebra-morphisms. Let $A,B$ be $\Sigma$-algebras and let $m=(m_s)_{s\in S}\colon A \longrightarrow B$ be a $\Sigma$-algebra-morphism. For a $\Sigma$-subalgebra $A'\subseteq A$ of $A$, its image $m(A')\subseteq B$ is a $\Sigma$-subalgebra of $B$. The expression $B':=m(A')$ is defined in the obvious way, i.e. for $A'=((s^{A'})_{s\in S},(f^{A'})_{f\in F})$ the $\Sigma$-subalgebra $B'=((s^{B'})_{s\in S},(f^{B'})_{f\in F})$ is given by $s^{B'}:=\{m_s(a)|a\in s^{A'}\}$ for all $s\in S$ and $f_{B'}(m_{s_1}(a_1),\ldots,m_{s_n}(a_n)) = m_s(f_{A'}(a_1,\ldots,a_n))$ for all function symbols $f \colon s_1 \times \ldots\times s_n \longrightarrow s$ with $f\in F$ and $a_i \in s_i^{A'}$. The coimage of a $\Sigma$-subalgebra $B'\subseteq B$ of $B$ under $m$ is a $\Sigma$-subalgebra $m^{-1}(B')\subseteq A$ of $A$. The expression $m^{-1}(B')$ can be defined analogously to $m(A')$ and is omitted here [ST99].

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