Axioms and Terms

As for many-sorted specifications, an atomic formula is well-formed (with respect to the current declarations) if it is well-sorted and expands to a unique atomic formula for constructing sentences of the underlying institution--but now for subsorted specifications, uniqueness is required only up to an  equivalence on atomic formulae and terms. Two expansions t, t' of the same term are regarded as equivalent in the following cases:

• t' is the application of an embedding of t into a supersort of its sort;
• t and t' are the applications of different compositions of embeddings of the same term into the same sort;
• t' is the same as t up to profiles of function symbols in the overloading relation < _F and embeddings.

• the formulae are identical, up to replacement of equivalent terms; or
• the formulae are the same up to the profiles of predicate symbols in the overloading relation < _P and embeddings.

The notions of when an atomic formula or term is well-sorted and of its expansion are indicated below for the various subsorting constructs. Due not only to overloading of predicate and/or function symbols, but also to implicit embeddings from subsorts into supersorts, a well-sorted atomic formula or term may have several expansions, preventing it from being well-formed. Qualifications on function and predicate symbols, or explicit sorts on terms, may be used to determine the intended expansion (up to the equivalence indicated above) and make it well-formed.

ATOM            ::=   ... | MEMBERSHIP
MEMBERSHIP      ::=   membership TERM SORT

Atomic formulae ATOM are extended with a construct for testing membership in subsorts. A membership formula is well-sorted if the specified TERM is well-sorted for a supersort s' of the specified SORT s. It expands to an application of the pre-declared predicate symbol for testing s' values for membership in the embedding of s.

TERM            ::=   ... | CAST
CAST            ::=   cast TERM SORT

Term formation is extended too, by providing a casting construct CAST for projections (there are no implicit casts). The cast of the specified TERM to a SORT s is well-sorted if the term is well-sorted for a supersort s' of s. It expands to an application of the pre-declared function symbol for projecting from s' to s.

Term formation is also extended by letting a term of a subsort s be regarded as a well-sorted term of a supersort s' as well, which provides implicit embeddings. It expands to the explicit application of the pre-declared function symbol for embedding s into s'. Also a SORTED-TERM expands to an explicit application of an embedding, provided that the apparent sort of the component TERM is a subsort of the specified SORT.

---

CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk