Term-Algebra

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

The formal description of a computer program consists of two components. First, a signature $\Sigma=(S,F)$ defining its syntactical (input/output) behaviour, and second, a corresponding $\Sigma$-algebra $A$ describing the semantics of the program. Whereas $\Sigma$ is typically quite obvious, the task of finding an appropriate $A$ is nontrivial due to the necessary compatibility with $\Sigma$. In the case of sensible signatures $\Sigma$, it exists a canonical construction for such an $A$, however, using only the elements of $\Sigma$. This construction leads to the so-called (ground) term algebra $T(\Sigma)$ having the following structure [M89]:

The carrier sets $s^{T(\Sigma)}$ of the ground term $T(\Sigma)$ are defined as $s^{T(\Sigma)} := T_s(\Sigma)$. The function are given by:

• For $f\in F$ with type$(f)= \,\,\rightarrow s$, it holds $f^{T(\Sigma)}:= f$
• For $f\in F$ with type$(f)= s_1\times\cdots\times s_n \longrightarrow s$ and for $t_i\in s^{T(\Sigma)}_i = T_{s_i}(\Sigma)$, it holds $f^{T(\Sigma)}(t_1,\ldots,t_n):= f(t_1,\ldots,t_n)$

In this way, the (ground) term algebra consists of the terms generated from the constants functions.

Typically, many other $\Sigma$-Algebras non-isomorphic to $T(\Sigma)$ exist. Let $X$ be an $S$-sorted set of variables. If $T_s(\Sigma,X)\neq\emptyset$ for each $s\in S$, the set $T(\Sigma,X)$ forms a $\Sigma$-algebra as well [W90]. This type of $\Sigma$-algebra becomes essential, if $\Sigma$ is not sensible due to missing constants for some sort $s\in S$. In such a case, a variable $x\in X_s$ can take over the role of the missing constant in a term. It is always possible to make the set $X$ large enough for this purpose.

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
[W90]	M. Wirsing: "Algebraic Specification", in J. van Leeuwen: "Handbook of Theoretical Computer Science", Elsevier 1990