This section introduces the signatures, models, and sentences characterizing basic specifications with subsorts, extending a preceding section. The notion of satisfaction for subsorted specifications is essentially as for many-sorted specifications.
The intuition behind the treatment of subsorts adopted here is to represent subsort inclusion by embedding (which is not required to be identity), 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 embedding 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).