Go backward to 3.1 Signatures
Go up to 3 Subsorting Concepts
Go forward to 3.3 Sentences
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
- 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
- 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
- Embedding is compatible with those operations and predicates that are
in the overloading relations.
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to email@example.com