View source for Term-Algebra

{{MSC|68P05}} 

{{TEX|done}}

The  formal description of a computer program consists of two components.   First, a [[Signature (Computer Science)|signature]] $\Sigma=(S,F)$  defining its syntactical (input/output) behaviour, and second, a  corresponding [[Sigma-algebra (Computer Science)|$\Sigma$-algebra]] $A$  describing the [[Semantics|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 [[Signature (Computer Science)#Signatures with Special  Properties|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 <i>[[Term  (Formalized Language)#Ground Terms and Morphisms|(ground) term]]  algebra</i> $T(\Sigma)$ having the following structure  {{Cite|M89}}:

The carrier sets $s^{T(\Sigma)}$ of the  ground term $T(\Sigma)$ are defined as $s^{T(\Sigma)} := T_s(\Sigma)$.  The functions 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. One alternative consists of including an $S$-sorted set $X$ 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 {{Cite|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. $T(\Sigma,X)$ is sometimes called <i>term-algebra</i> in contrast to the ground term algebra $T(\Sigma)$.

===References===

{|
|-
|valign="top"|{{Ref|EM85}}||valign="top"| H. Ehrig, B. Mahr: "Fundamentals of Algebraic Specifications", Volume 1, Springer 1985
|-
|valign="top"|{{Ref|EM90}}||valign="top"| H. Ehrig, B. Mahr: "Fundamentals of Algebraic Specifications", Volume 2, Springer 1990
|-
|valign="top"|{{Ref|M89}}||valign="top"|  B. Möller: "Algorithmische Sprachen und Methodik des Programmierens I",  lecture notes, Technical University Munich 1989
|-
|valign="top"|{{Ref|W90}}||valign="top"|  M. Wirsing: "Algebraic Specification", in J. van Leeuwen: "Handbook of  Theoretical Computer Science", Elsevier 1990
|-
|}