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):

• Embeddings are 1-1 functions.
• The embedding of a sort into itself is the identity function.
• All compositions of embeddings between the same two sorts are equal functions.
• Projections are the partial inverses of embeddings.

  [AT] Is this really unambiguous? I am not sure what a "partial inverse" is, but with a bit of bad will it might be defined so that the composition of a partial function and its partial inverse in both directions is a subset of identity. Here of course the point is that one of these compositions is the identity, and the other is a subset of identity.

  Discharged: Adjust wording.

• Membership in a subsort holds just when the projection to the subsort is defined.
• Embeddings commute with those functions and predicates that are in the overloading relations.

  [DTS,AT] Unclear. I do not like the verb "commute" here: with the current definition of overloading of functions, what we mean here need not be commutativity as such. Perhaps "are compatible" would be better?

  Discharged: Adjust wording.

---

CoFI Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk