View source for Term (Formalized Language)


{{MSC|68P05}} 

{{TEX|done}}

This  entry discusses terms as syntactically correct expressions in a  [[Formalized language|formalized language]] defined over a [[Signature (Computer Science)|signature]] $\Sigma =(S,F)$ and  a set of variables. For terms as informal objects in mathematical  expressions, see the entry [[term]]. For expressions similar to terms but representing a truth value instead of a type $s\in S$, see the entry [[Formula|formulas]].

===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 of sort $s$</i> 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)$

The set $T(\Sigma,X)$ of <i>terms</i> is defined as $T(\Sigma,X):= \bigcup\limits_{s\in S} T_s(\Sigma,X)$.

The terms $t\in T(\Sigma,X)$ are the elements of the formalized language given by the signature $\Sigma$ and the set $X$ of variables.  Supplementing the function symbols $F$ of the signature $\Sigma$ by variables serves several purposes.
* Using variables $X$, it is possible to construct well-defined language elements even if no constants belong to the signature.  Representing terms as trees, only constants and variables can serve as leafs.
* A single term $t\in T(\Sigma,X)$ containing a variable $x\in X_s$ of sort $s\in S$ can be used for representing the infinite collection of terms resulting from the substitution (see below) of $x$ by terms $t'\in T_s(\Sigma,X)$ of sort $s$.
* Sometimes, a subterm  $t_1\in T_s(\Sigma,X)$, $s\in S$ of a term $t\in T(\Sigma,X)$ is replaced by a term $t_2$ equivalent to $t_1$ (e.g. in the case of formula manipulation). In this case, the term $t$ with subterm $t_1$ replaced by a variable $x\in X_s$ not contained in $t$ defines the so-called context of the manipulation.

===Identifying and Manipulating Free Variables===

For the purposes listed above, it may be necessary to identify the [[Free variable|free variables]] of a term. This is done  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)$. A term $t\in T(\Sigma,X)$ is called <i>closed</i>, if $V(t)= \emptyset$. It is closed, iff it is a ground term (i.e. $t\in T(\Sigma)$).

Every  signature morphism $m\colon \Sigma_1\longrightarrow \Sigma_2$ for signatures $\Sigma_1=(S_1,F_1), \Sigma_2=(S_2,F_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. Such an extension is called a <i>translation</i>. It replaces every function symbol $f\in F_1$ by the corresponding function symbol $\sigma(f)\in F_2$.

===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
|-
|}