Difference between revisions of "User:Joachim Draeger/sandbox"

Revision as of 19:30, 16 January 2013

Term (Formal Language)

2020 Mathematics Subject Classification: Primary: 68P05 [MSN][ZBL]

This entry discusses terms as syntactically correct expressions in a 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. 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 terms 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 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 substitution $t[x\leftarrow w]$ of $x$ with $W$ is inductively defined as follows:

$x[x\leftarrow w]:= w$
$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 ground terms. 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 including sets $X = \bigcup_{s\in S_1} X_s$, $X'= \bigcup_{s\in S_2} X_s'$ of variables 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

[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:
Joachim Draeger/sandbox. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Joachim_Draeger/sandbox&oldid=29309

@@ Line 1: / Line 1: @@
-Signature (computer science)
+Term (Formal Language)
 {{MSC|68P05}}
@@ Line 6: / Line 7: @@
 {{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]].
-If the behaviour of a computer program should be described formally --- this is necessary for e.g. the verification of programs --- two basic components (syntax and semantics) are required. Here, we discuss the syntactical component determined by the so-called <i> signature </i>.  Informally, the signature gives the available data formats (i.e.  sorts) and the available operations defined on them.
+===Definition of Terms===
-Signatures are used for the inductive definition of two important formal languages by compositions of the operations contained in the signature. The first such language is the formal language of terms, consisting of the operations of the signature only. The second language gives the set of formulas based on non-logical operations provided by the signature and the logical operations provided by the logics under consideration.
-===Definition of Signatures===
-A signature $\Sigma =(S,F)$ consists of a set $S$ of <i> sorts </i> and a set $F$ of <i> function symbols </i> with $S\cap F=\emptyset$.  Every function symbol $f\in F$ is assigned an <i> arity </i> ar$\colon F\longrightarrow \mathbb{N}_0$ giving the number of arguments of $f$. In the case ar$(f)=0$ for a function symbol $f\in F$, the symbol $f$ is called a <i> constant </i> symbol.  Every function symbol $f\in F$ is assigned a <i> function type </i> type$\colon s_1\times\cdots\times s_{ar(f)} \longrightarrow s$.  The function type makes the set $F$ an $S^\ast \times S$-sorted set.  Thus, $F$ may contain different function symbols designated in the same way and distinguished only by the function type. An example is the addition symbol $+$ used both for integer and real resp. float numbers. Such function symbols are called <i> overloaded </i>.
-If the admissable function types are limited to $S^+\rightarrow S$, constant symbols must be considered separately. This leads to signatures of the form $(S,C,F)$ with $C$ as set of constant symbols with $S\cap C =\emptyset$ and with $F\cap C =\emptyset$. If only signatures $\Sigma$ as part of [[Algebraic Specification|algebraic specifications]] $D=(\Sigma,E)$ are considered, constants can be avoided alltogether under the assumption that the algebras used as models of $D$ are nonempty.  In this case, a constant symbol $c\in C$ can be replaced by a unary function symbol $f\in F$ and a law $e\in E$ that $f$ has the same value for all values of its argument.
-===Signatures with Special Properties===
+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)$
-* A signature $\Sigma=(S,F)$ is called <i> sensible </i> if it exists a [[Term|ground term]] for each sort $s\in S$, i.e. if $\forall s\in S\colon T_s(\Sigma)\neq \emptyset$.
+===Identifying and Manipulating Free Variables===
-* A signature $\Sigma=(S,F)$ is called <i> finite </i> if $|S|\in\mathbb{N}$ and $|F|\in\mathbb{N}$.
-* A signature $\Sigma_1=(S_1,F_1)$ is called a subsignature of $\Sigma_2=(S_2,F_2)$ --- formally written $\Sigma_1\subseteq \Sigma_2$ --- if $S_1\subseteq S_2$ and $F_1\subseteq F_2$.
-===The Category of Signatures===
+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$
+* $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)$
-A signature morphism $m\colon \Sigma_1\longrightarrow \Sigma_2$ from the signature $\Sigma_1=(S_1,F_1)$ to the signature $\Sigma_2=(S_2,F_2)$ is a pair $m=(m_S,m_F)$ consisting of a mapping $m_S\colon S_1 \longrightarrow S_2$ between the sorts and of a mapping $m_F\colon F_1 \longrightarrow F_2$ between the function symbols such that the function type is preserved under $m$ according to $\forall f\in F_1\colon \mbox{type}(m_F(f)) = m_S(\mbox{type}(f)) := m_S(s_1)\times\cdots\times m_S(s_{ar(f)}) \longrightarrow m_S(s)$ for functions $f\in F_1$ with type$(f)= s_1\times\cdots\times s_{ar(f)} \longrightarrow s$. The class of all signatures together with the signature morphisms forms a category {{Cite|W90}}.
+===Ground Terms and Morphisms===
-===An Example===
+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)$.
-<tt> signature </tt> $\Sigma_{\mbox{BOOL}}$
+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 including sets $X = \bigcup_{s\in S_1} X_s$, $X'= \bigcup_{s\in S_2} X_s'$ of variables 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.
-: <tt> sort </tt> BOOL
-: <tt> functions </tt>
-:: true  : $\longrightarrow$ BOOL
-:: false : $\longrightarrow$ BOOL
-:: NOT : BOOL $\longrightarrow$ BOOL
-:: AND : BOOL $\times$ BOOL $\longrightarrow$ BOOL
-:: OR : BOOL $\times$ BOOL $\longrightarrow$ BOOL
-<tt> endsignature </tt>
+===References===
 {|

Navigation

Tools

Namespaces

Variants

Views

Actions