next up previous
Next: The Algebra Up: The Signature Previous: The Signature

Let Numbers be the signature whose sort is tex2html_wrap_inline374 with operations which we will call tex2html_wrap_inline376 , 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 tex2html_wrap_inline378 , 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 tex2html_wrap_inline384 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 tex2html_wrap_inline392 and sort Nat; in OBJ-style notation,

displaymath360

The pair w,s is called the rank of the operation. There may well be other operations in tex2html_wrap_inline358 of the same rank as add: mult, for example. So then add and mult will belong to the same member of the family, namely tex2html_wrap_inline408 . We can write

displaymath361

Similarly, we may have

displaymath362

displaymath363

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 ` tex2html_wrap_inline410 ' or ` tex2html_wrap_inline412 ' 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

displaymath364

displaymath365

At this point we might be tempted to think we had finished, since we seem to have covered everything, but in fact the family tex2html_wrap_inline354 is an infinite set of sets tex2html_wrap_inline426 . Some more examples are tex2html_wrap_inline428 , 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:

displaymath37

A friendlier version of the same signature is:

displaymath49

The constant zero together with the operation succ are called the constructors of the sort Nat; similarly, T and F are constructors of Bool.


next up previous
Next: The Algebra Up: The Signature Previous: The Signature

Jean Baillie
Thu May 23 16:30:42 BST 1996