S-1 -- 4.3 Axioms and Terms

Go backward to 4.2 Predicative Subsort Definitions
Go up to 4 Subsorting Constructs

4.3 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:

[AT] Do we really define here only equivalence between expansions of the same term, or in fact between any two fully-qualified terms?

Discharged: The latter.

t' is the application of an embedding of t into a supersort of its sort;
[DTS,AT] This is not quite clear. I guess what is meant is that t' = embedding(t), but this is not literally stated here. How about: "t' is the application to the term t of an embedding from its sort to a supersort"?

Discharged: Adjust wording.
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.

Two expansions of the same atomic formula are regarded as equivalent in the following cases:

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.

[AT] Some hint is needed that the closure of the cases as listed under the equivalence and congruence rules is used to get the equivalence we mean. For formulae, the closure under congruence rules seems built-in, but transitivity should be stated separately.

Discharged: Adjust wording.

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.

[AT] We should indicate somewhere that well-formedness of a term (formula etc.) might depend on its position in the sequence of basic items: basic items that come later may introduce extra ambiguities and make a well-formed term ill-formed.

Discharged: No, because of non-linear visibility.

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

[TM] well-formed

Discharged: Adjust wording.

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 Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk