**Go backward to** 3.1 Signatures

**Go up to** 3 Subsorting Concepts

**Go forward to** 3.3 Sentences

## 3.2 Models

For a subsorted signature *Sigma* the *subsorted models*
are ordinary many-sorted models for *Sigma*^{#} that satisfy the
following properties (which can be formalized as a set of conditional
axioms):

- Embedding operations are total and 1-1; projection operations are
partial, and 1-1 when defined.
- The embedding of a sort into itself is the identity function.
- All compositions of embedding operations between the same two sorts are
equal functions.
- Embedding followed by projection is identity; projection followed
by embedding is included in identity.
- Membership in a subsort holds just when the projection to the subsort
is defined.
- Embedding is compatible with those operations and predicates that are
in the overloading relations.

CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk