Namespaces
Variants
Actions

Difference between revisions of "Term-Algebra"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Created page with "{{MSC|68P05}} {{TEX|done}} The formal description of a computer program consists of two components. First, a signature $\Sigma=(S,F)$ d...")
 
m
Line 3: Line 3:
 
{{TEX|done}}
 
{{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 (Compuetr 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  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 function are given by:
 
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:

Revision as of 14:50, 3 February 2013

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
How to Cite This Entry:
Term-Algebra. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Term-Algebra&oldid=29383