Let Numbers be the signature whose sort is
with
operations which we will call
, defined over these sets. At this point we must remind
ourselves that a signature is a syntactic structure; as yet we have
assigned no meaning to it. Our intuition is already several steps
ahead; we know what we mean by
, and so on, and it is,
of course, this intuition which motivates the whole subject.
Nevertheless, whilst this helps us in our understanding of what we are
doing and why, we must keep a tight rein on it; we must, for the time
being, pretend we do not yet have a notion of meaning. We
could just as easily have named the sorts in S, X and Y and the
operations in
etc. This would retain the strictly
`meaningless' quality of the syntax until we were ready to talk about
semantics; it might also make it easier to accept the somewhat less
obvious semantic possibilities which we shall see later on.
We can think of the operations in our signature as a family of sets
indexed by arity, w, and sort, s. Informally,
the arity of an operation refers to the number and sorts of the
operands and the sort refers to the result. So, for instance, we may
define the operation add to be of arity
and sort Nat;
in OBJ-style notation,
The pair w,s is called the rank of the operation. There may well be other
operations in
of the same rank as add: mult, for example. So
then add and mult will belong to the same member of
the family, namely
. We can write
Similarly, we may have
This covers all the operations named above. However, it is usual to
regard the constants of each sort as operations; they are, in a sense,
results without operands, so their arity is denoted by
`
' or
`
' to indicate this. So, for instance, should we decide to
name the constants of Bool T and F, and the constant in Nat
zero, we have
At this point we might be tempted to think we had finished, since we
seem to have covered everything, but in fact the family
is an
infinite set of sets
. Some more examples are
, and so
on. We have not named any operations of these ranks, however, so
these sets are empty. We can now put the whole signature together as
follows:
A friendlier version of the same signature is:
The constant zero together with the operation succ are called the constructors of the sort Nat; similarly, T and F are constructors of Bool.