Go up to Subsorting Constructs
Go forward to Axioms and Terms

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         ::=  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, and when it does not lead to mutual or cyclic embedding.

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

CoFI Document: LanguageSummary --DRAFT, Version 0.96-- 30 April 1997.
Comments to cofi-language@brics.dk