Transitive overloading relations?

[Till Mossakowski <till@Informatik.Uni-Bremen.DE>]

Dear friends,

in a discussion with Andrzej about the interaction of subsorting
and architectural specifications, we came to the following point:

AT>My intuition, however informal, is that the overloading relation plays
AT>a similar role as identity of (fully qualified) names in CASL, and if
AT>a union results in such an overloading then this is quite similar to
AT>the overlapping of names --- it is the responasability of the user to
AT>avoid uninteded clashes and take advantage of the intended ones. Of
AT>course, as in the case of identical names, there is room for tools to
AT>issue some warnings etc.

In particular, instantiations of generics and architectural specifications
refer to sharing of names within certain well-definedness conditions.
This sharing relation turns out to be the overloading relation.

My question is now:
Shouldn't the sharing relation be an equivalence relation?

Currently, the overloading relation is only reflexive and symmetric.

It would therefore be consequent to transitively close the overloading 
relation.

However, this would lead to more complex axioms in the reduction
semantics. Namely, we would now have to use zigzag ways of injections
and projections in order to describe the semantic effect.
And I am not sure if we would gain anything from that.
At least for constants, we do not gain anything, because
if c:t \sim_F c:u and c:u \sim_F c:v, it is clear
that c:t and c:v have to interpreted "in the same way"
(meaning up to a zigzag way of injections and projections) anyway,
even if not c:t \sim_F c:v.
And I think it is the same situation for functions and predicates.

So perhaps we should use the original overloading for the model
semantics, but use its transitive closure for sharing issues?

Greetings,
Till