Go backward to 1 Overloading relations
Go up to Top
Go forward to 3 Compound identifiers

2 Implicit subsort cycles

There is a special construct ISO-DECL for introducing subsort cycles, which has the effect that all mentioned sorts are made isomorphic. There is a methodological argument in favour of forbidding the implicit introduction of such cycles, by writing for example

   Sorts s < s'
         s' < s

Since the user has the chance to specify the cycle explicitly with an ISO-DECL, an implicit cycle probably is caused by a name clash in extension or a union. Thus it should be forbidden. Note that it is still allowed to made to previously-related sorts isomorphic with an ISO-DECL.

The check for implicit cycles has to be done at the following places:

In an SUBSORT-DECL, check that s₂/ < s₁ for each newly declared s₁ < s₂. Due to the structure of the semantics this also covers extensions.

In a translation, check that the identification of sorts does not lead to a new cycle. Alternatively, require signature morphisms in a TRANSLATION to be injective.

In a UNION, check if each cycle is already present in a component.

In an instantiation of a generic specification, do the same check as for extensions.

These checks are currently done in the semantics (although there seems to be no strong argument why they shouldn't be treated in the same way as the checks of the previous section).

CoFI Note: S-3 --1.0-- 26 March 1997.
Comments to till@informatik.uni-bremen.de