Go up to Basic Concepts
Go forward to Models
Signatures
A many-sorted signature Sigma= (S,TF,PF,P) consists of:
- a set S of sorts;
- sets TFw,s, PFw,s, of total function resp.
partial function symbols, such that TFw,s n PFw,s = Ø, for each function profile (w,s)
consisting of a sequence of argument sorts w e S* and a
result sort s e S ( constants are treated as functions
with no arguments);
- sets Pw of predicate symbols, for each predicate
profile consisting of a sequence of argument sorts w e S*.
Note that symbols may be overloaded, occurring in more than one
of the above sets. To ensure that there is no ambiguity in sentences
at this level, however, symbols are always qualified by profiles when
used (the language considered in a later
section allows the omission of
such qualifications when these are unambiguously determined by the
context).
A many-sorted signature morphism sigma: (S,TF,PF,P) -> (S',TF',PF',P') consists of a mapping from S to S',
and for each w e S*, s e S, a mapping between the
corresponding sets of function, resp. predicate symbols. A partial
function symbol may be mapped also to a total function symbol, but not
vice versa.
CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk