|
|
| Line 1: |
Line 1: |
| | | | |
| − |
| |
| − | Term (Formal Language)
| |
| − |
| |
| − | {{MSC|68P05}}
| |
| − |
| |
| − | {{TEX|done}}
| |
| − |
| |
| − | This entry discusses terms as syntactically correct expressions in a [[Formalized language|formalized language]] defined over a signature and a set of variables. For terms as informal objects in mathematical expressions, see the entry [[term]].
| |
| − |
| |
| − | ===Definition of Terms===
| |
| − |
| |
| − | Let $\Sigma =(S,F)$ be a [[Signature (Computer Science)|signature]]. Let $X_s$ be a set of variables of sort $s\in S$ with $X_s\cap F=\emptyset$ and $X_s\cap S=\emptyset$. Furthermore, let the set of variables be defined as disjoint union $X:= \bigcup_{s\in S} X_s$. Then the set $T_s(\Sigma,X)$ of <i>terms</i> of sort $s$ is defined inductively as the smallest set containing all
| |
| − | * $x\in X_s$
| |
| − | * $f\in F$ being constants with range $s$ (i.e. type($f$) $=\,\, \rightarrow s$)
| |
| − | * $f(t_1,\ldots,t_n)$ for $f\in F$ with type$(f)= s_1\times\cdots\times s_{ar(f)} \longrightarrow s$ and $t_i\in T_{s_i}(\Sigma,X)$
| |
| − |
| |
| − |
| |
| − | ===Identifying and Manipulating Free Variables===
| |
| − |
| |
| − | The [[Free variable|free variables]] of a term are identified using a mapping $V\colon T(\Sigma,X) \longrightarrow 2^X$, which is inductively defined as follows:
| |
| − | * For $x\in X$, it holds $V(x)=\{x\}$
| |
| − | * For constants, i.e. $c\in F$ with ar($c$) $=0$, it holds $V(c)=\emptyset$
| |
| − | * For a term $f(t_1,\ldots,t_n)$ with $f\in F$ of type$(f)= s_1\times\cdots\times s_{ar(f)} \longrightarrow s$ and terms $t_i\in T_{s_i}(\Sigma,X)$, it holds $V(f(t_1,\ldots,t_n)) := V(t_1)\cup\cdots\cup V(t_n)$
| |
| − | Let $t,w\in T(\Sigma,X)$ be terms and $x\in X$ be a variable. The <i> substitution</i> $t[x\leftarrow w]$ of $x$ with $w$ is inductively defined as follows:
| |
| − | * $x[x\leftarrow w]:= w$
| |
| − | * $y[x\leftarrow w]:= y$ for $y\in X$ with $x\neq y$
| |
| − | * $c[x\leftarrow w]:= c$ for $c\in F$ with ar($c$) $=0$
| |
| − | * $f(t_1,\ldots,t_n)[x\leftarrow w] := f(t_1[x\leftarrow w],\ldots,t_n[x\leftarrow w])$ for a term $f(t_1,\ldots,t_n)$ with $f\in F$ of type$(f)= s_1\times\cdots\times s_{ar(f)} \longrightarrow s$ and terms $t_i\in T_{s_i}(\Sigma,X)$
| |
| − |
| |
| − | ===Ground Terms and Morphisms===
| |
| − |
| |
| − | Terms $t$ without variables, i.e. $t\in T(\Sigma,\emptyset)=:T(\Sigma)$, are called <i> ground terms</i>. The ground terms $t$ of sort $s\in S$ are designated as $T_s(\Sigma):= t\in T_s(\Sigma,\emptyset)$ For all sets $X$ of variables and for all sorts $s\in S$, it holds $T_s(\Sigma) \subseteq T_s(\Sigma,X)$. For all sets $X$ of variables, it holds $T(\Sigma) \subseteq T(\Sigma,X)$.
| |
| − |
| |
| − | Every signature morphism $m\colon \Sigma_1\longrightarrow \Sigma_2$ can be extended to a morphism $m'\colon T(\Sigma_1)\longrightarrow T(\Sigma_2)$ between ground terms. If the morphism $m$ can be extended to a mapping, which is defined for sets $X = \bigcup_{s\in S_1} X_s$, $X'= \bigcup_{s\in S_2} X_s'$ of variables as well with $m(x)\in X'_{m(s)}$ for $x\in X_s$, $s\in S_1$, the signature morphism $m$ can also be extended to a morphism $m^\ast\colon T(\Sigma_1,X)\longrightarrow T(\Sigma_2,X')$ between terms.
| |
| − |
| |
| − | ===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
| |
| − | |-
| |
| − | |}
| |