Go up to Basic Concepts
Go forward to Models

Signatures

A  many-sorted signature Sigma= (S,TF,PF,P) consists of:

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