Difference between revisions of "Term-Algebra"
(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 ( | + | 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 | + | 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. | + | 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 |
Term-Algebra. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Term-Algebra&oldid=29383