View source for Signature (Computer Science)


{{MSC|68P05}} 

{{TEX|done}}


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. 

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

*  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$.
* 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===

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

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