Namespaces
Variants
Actions

Difference between revisions of "Signature (Computer Science)"

From Encyclopedia of Mathematics
Jump to: navigation, search
m
 
(2 intermediate revisions by the same user not shown)
Line 5: Line 5:
  
  
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.  
+
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 signature operations. 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.
 
Signatures  are used for the inductive definition of two important formal languages by compositions of signature operations. 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.
Line 11: Line 11:
 
===Definition of Signatures===
 
===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>.
+
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.  
 
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.  
Line 17: Line 17:
 
===Signatures with Special Properties===
 
===Signatures with Special Properties===
  
*  A signature $\Sigma=(S,F)$ is called <i> sensible </i> if  it exists a [[Term (Formalized Language)|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> sensible </i> if  it exists a [[Term (Formalized Language)#Ground Terms and Morphisms|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=(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$.
 
*  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$.
Line 24: Line 24:
  
 
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 form a category  {{Cite|W90}}.
 
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 form a category  {{Cite|W90}}.
 +
 +
===An Example===
 +
 +
We will consider the signature $\Sigma_{\mathbb{B}}=(S_{\mathbb{B}}, F_{\mathbb{B}})$ of propositional logics. The set $S_{\mathbb{B}} = \{s_{\mathbb{B}}\}$ of sorts consists only of the sort $\mathbb{B}$ of truth values. The set $F_{\mathbb{B}}=\{\top,\bot,\neg,\wedge,\vee\}$ of function symbols has the elements
 +
* The symbols $\top,\bot$ representing the truth values 'true' and 'false', written as constant functions $\top\colon \,\,\rightarrow \mathbb{B}$ and $\bot\colon \,\,\rightarrow \mathbb{B}$.
 +
* The symbol $\neg$ of the negation with type $\neg \colon \mathbb{B} \longrightarrow \mathbb{B}$.
 +
* The symbols $\wedge,\vee$ of the two binary operations 'and' and 'or' with type $\wedge \colon \mathbb{B}\times\mathbb{B} \longrightarrow \mathbb{B}$ and $\vee \colon \mathbb{B}\times\mathbb{B} \longrightarrow \mathbb{B}$
 +
Written in the pseudocode of a specification language, $\Sigma_{\mathbb{B}}$ has the form
 +
 +
 +
<tt> signature </tt> $\Sigma_{\mbox{BOOL}}$
 +
:: <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===
 
===References===

Latest revision as of 17:31, 7 February 2013

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


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 signature. 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 signature operations. 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 sorts and a set $F$ of function symbols with $S\cap F=\emptyset$. Every function symbol $f\in F$ is assigned an arity 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 constant symbol. Every function symbol $f\in F$ is assigned a function type 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 overloaded.

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 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 sensible if it exists a 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 finite 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 form a category [W90].

An Example

We will consider the signature $\Sigma_{\mathbb{B}}=(S_{\mathbb{B}}, F_{\mathbb{B}})$ of propositional logics. The set $S_{\mathbb{B}} = \{s_{\mathbb{B}}\}$ of sorts consists only of the sort $\mathbb{B}$ of truth values. The set $F_{\mathbb{B}}=\{\top,\bot,\neg,\wedge,\vee\}$ of function symbols has the elements

  • The symbols $\top,\bot$ representing the truth values 'true' and 'false', written as constant functions $\top\colon \,\,\rightarrow \mathbb{B}$ and $\bot\colon \,\,\rightarrow \mathbb{B}$.
  • The symbol $\neg$ of the negation with type $\neg \colon \mathbb{B} \longrightarrow \mathbb{B}$.
  • The symbols $\wedge,\vee$ of the two binary operations 'and' and 'or' with type $\wedge \colon \mathbb{B}\times\mathbb{B} \longrightarrow \mathbb{B}$ and $\vee \colon \mathbb{B}\times\mathbb{B} \longrightarrow \mathbb{B}$

Written in the pseudocode of a specification language, $\Sigma_{\mathbb{B}}$ has the form


signature $\Sigma_{\mbox{BOOL}}$

sort BOOL
functions
true : $\longrightarrow$ BOOL
false : $\longrightarrow$ BOOL
NOT : BOOL $\longrightarrow$ BOOL
AND : BOOL $\times$ BOOL $\longrightarrow$ BOOL
OR : BOOL $\times$ BOOL $\longrightarrow$ BOOL

endsignature

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:
Signature (Computer Science). Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Signature_(Computer_Science)&oldid=29325