**Go up to** 1 Basic Concepts

**Go forward to** 1.2 Models

## 1.1 Signatures

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

- a set
*S* of *sorts*;
- sets
*TF*_{w,s}, *PF*_{w,s}, of *total function symbols*,
respectively *partial function symbols*, such that
*TF*_{w,s} **n*** **PF*_{w,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
*P*_{w} of *predicate* symbols, for each *predicate
profile* consisting of a sequence of argument sorts *w ***e*** S*^{*}.

Constants and functions are also referred to as
*operations*, following the traditions of algebraic
specification.
Note that symbols used to identify sorts, operations, and predicates
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, function symbols *f* and predicate symbols *p* are
always *qualified* by profiles when used, written *f*_{w,s}
and *p*_{w} respectively. (The language considered in
Chapter 2 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
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk