Prev Up Next
Go backward to 2 Basic Constructs
Go up to Top
Go forward to 4 Subsorting Constructs

3 Subsorting Concepts

This section introduces the signatures, models, and sentences characterizing basic specifications with subsorts, extending a preceding section. The notions of satisfaction and proof system for subsorted specifications are essentially as for many-sorted specifications.

The intuition behind the treatment of subsorts adopted here is to represent subsorting by embeddings (which are not required to be identities), commuting with overloaded function symbols, as usual in order-sorted approaches. However, in the language described in the next section, instead of imposing conditions such as `regularity' on signatures, terms and sentences that can be given different parses (up to the commutativity between embeddings and overloaded symbols) are simply rejected as ill-formed.

While well-formedness of terms of the language can be checked statically, the question whether the value of a well-formed term is actually defined or not may depend on the specified axioms (and it is not decidable in general).

  • 3.1 Signatures
  • 3.2 Models
  • 3.3 Subsorted Sentences

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

    Prev Up Next