Go up to Top
Go forward to 2 Implicit subsort cycles

1 Overloading relations

Recall that the overloading relations are relations between function and predicate profiles which are automatically derived from a signature. Two profiles of one and the same function symbol are in the overloading relation < _F, if the argument sorts of the first profile are less than or equal to than those of the second one, and both result sorts have a common supersort. (A similar relation < _P is defined for predicates.) In the semantics, two profiles of an overloaded function symbol which are in the overloading relation < _F have to be interpreted in the same way (i.e., the interpretation of the "smaller" profile is a restriction of the interpretation of the "bigger" profile).

Now the overloading relation is not conservative w. r. t. unions or extensions. This may lead to unexpected identifications of operation or predicate symbols. For instance, if we have the specifications

SP =   sorts nat
       opns / : nat nat -> nat

SP1 =  SP + sorts nat < real
       opns / : real real --> real

SP2 =  SP +
       sorts nat < int
       opns / : int int --> int

using _/_ both for real and for integer division, then, putting together SP1 and SP2, the two operations / have to be identified on natural arguments. This problem can introduce serious misunderstanding in large specifications, if their parts are developed independently. Moreover, it may seem awkward that extending a signature by some new symbols implicitly introduces semantical identifications, as for instance in the following case:

enrich
   Sorts list, bool
   TFun  empty-tail: list --> list
         empty-tail: list --> bool
by Sorts values>list, bool

where the originally unrelated empty-tail: list -> list (with the intention of a function yielding an atomic list built from the head of the argument list) and empty-tail: list -> bool (with the intention of a test to see whether a list is atomic) get identified. Note that this also causes the extension not to be persistent.

The subsorting group was aware of this effect when chosing to automatically infer the overloading relations from the signatures. The argument for taking the name clashes not so seriously is that it may be more important for OBJ users not to get too many surprises when using familiar-looking subsorts, than for many-sorted users not to get too many surprises when importing a library module using subsorting.

These problems can be solved with the help of tools, which identify possible name clashes, and suggest appropriate renamings. W.r.t. subsorting, the following conditions should be checked:

In an SUBSORT-DECL, check that the overloading relations < _F and < _P are not affected by the newly introduced subsort relations. Due to the structure of the semantics this also covers extensions.

In a UNION, check if each pair of profiles in the overloading relations is already present in a component.

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

Note that these checks only concern methodology, and are not needed for the semantics: there is a semantics also for specifications which violate any of the above conditions.

Further note that since the union operator on modules also uses the "same name, same meaning" principle (ASL-style of sharing), strange things may happen in unions even without use of subtypes and overloading. The formulation of conditions (if any conditions are desirable here at all) which ensure that unions are used in a methodological proper way is beyond the scope of this note.

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