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. Equivalence between fully-qualified terms t, t' is the least congruence including the following cases:

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

• 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 embedding.

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 well-formed term of a subsort s be regarded as a well-sorted term of a supersort s' as well, which provides implicit embedding. 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 Document: LanguageSummary --DRAFT, Version 0.96-- 30 April 1997.
Comments to cofi-language@brics.dk