Go up to Subsorting Constructs
Go forward to Predicative Subsort Definitions

Subsort Declarations

SIG-DECL        ::=   ... | SUBSORT-DECL
SUBSORT-DECL    ::=   EMBEDDING-DECL | ISO-DECL
EMBEDDING-DECL  ::=   embedding-decl SORT-LAYER+
SORT-LAYER      ::=   sort-layer SORT+
ISO-DECL        ::=   SORT-LAYER
The sorts in a subsort declaration SUBSORT-DECL have to be already declared separately in the local environment, as such a construct merely determines a contribution to the subsort embedding pre-order of a subsorted signature. The same sort may not occur more than once in each SUBSORT-DECL.

By specifying an EMBEDDING-DECL, each sort in a SORT-LAYER is embedded in all the sorts in each SORT-LAYER on its right. Thus, an embedding declaration of the form:

embedding-decl...(sort-layer...s...)...(sort-layer...s'...)...
provides the embedding relation s < s'. An EMBEDDING-DECL is well-formed only when it has at least two SORT-LAYER components.

By specifying an ISO-DECL, each sort in its single SORT-LAYER is embedded in all the other sorts in that SORT-LAYER, thus allowing mutual and cyclic embeddings, which correspond to isomorphisms between carrier sets. An ISO-DECL is well-formed only when there are at least two SORT components in the SORT-LAYER.

Introducing an embedding relation between two sorts may cause function symbols to become related by the overloading relation, so that values of terms become equated when they are identical up to embeddings.

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