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
 
(2 intermediate revisions by the same user not shown)
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 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)= \,\,\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)$
 
*  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.
 
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 {{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.
+
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===
 
===References===

Latest revision as of 17:09, 8 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 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 [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 term-algebra in contrast to the ground term algebra $T(\Sigma)$.

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