Signature (Computer Science)

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