Up Next
Go up to 4 Subsorting Constructs
Go forward to 4.2 Predicative Subsort Definitions

4.1 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.
[TM] Is an EMBEDDING-DECL well-formed only if it does not lead to mutual or cyclic embeddings, since these should be specified with ISO-DECLs? (Yes)
Discharged: Only ISO-DECLs are permitted to lead to cycles. This has to be checked here as well as in renaming, union, instantiation of generics and enrichments.

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

Up Next