Functions (and predicates) may be overloaded, the same symbol being declared for more than one sequence of argument sorts. Argument sorts are related by subsort inclusions, but no `regularity' conditions are imposed on declarations.Here, the design of CASL found itself in a dilemma: it was recognized as highly desirable to provide support for the concept of subsorts and overloading (e.g., to allow the specification of natural numbers as a subsort of the integers, with the usual functions on natural numbers being extended to integers), but the notion of `regularity' of signatures, as adopted in order-sorted algebras [GM92], was found to have some drawbacks. Finally, it was decided to put no conditions at all on the declarations of overloaded functions, but instead to require that any uses of overloaded functions in terms should be sufficiently disambiguated, ensuring that different parses of the same term (involving different overloadings) always have the same semantics. The consequences for parsing efficiency of this decision are currently being investigated.
Subsort inclusions are represented by embedding functions, whose insertion in terms may be left implicit. The corresponding inverse projection functions from supersorts to subsorts are partial.In order-sorted algebra, subsort inclusions are modelled as actual set-theoretic inclusions between the corresponding carriers, whereas in CASL, they are more general, being arbitrary embeddings. This extra generality allows one to specify e.g. that integers are to be a subsort of the approximate real numbers, without requiring all models to use the same representation of each integer as for the corresponding approximate real.
Thanks to the possibility of partial functions in CASL, the projection functions from supersorts to subsorts can be given a straightforward algebraic semantics.
Subsort definitions allow the concise specification of subsorts that are determined by the values for which particular formulae hold.It was realized, during the design of subsorting in CASL, that one may distinguish two different uses of subsorts: (i) in the extension of a subalgebra, e.g., from natural numbers to integers, and (ii) to indicate the domain of definition of a partial function, e.g., the even numbers for integer division by 2. In (i) the values of the subsort(s) are generated implicitly by the declarations of operations of the subalgebra, whereas in (ii) it may be more convenient to characterize them explicitly by some predicate or formula. To cater for the latter, CASL provides a construct called a subsort definition. This declares a new sort, consisting of those values of another sort for which a particular formula holds--this might be written {x:s | P[x]}, where P[x] is some formula involving the variable x ranging over the sort s. (More precisely, the values of the new sort are the projections of values of sort s.)