(CoFI) New overloading relation

[Till Mossakowski <till@informatik.uni-bremen.de>]

Dear friends,

the current definition of the overloading relation <_F 
in section 3.1 of the CASL language summary is as follows:

f_1:w_1->s_1 <_F f_2:w_2->s_2

iff

w_1 < w_2 and there exists s' with s_1,s_2 < s'.

Now Andrzej suggested to me in Tarquinia to make this relation
a bit more symmetric wrt to arguments and results:

f_1:w_1->s_1 ~_F f_2:w_2->s_2

iff

there exists w' with w' < w_1,w_2    and 
there exists s' with s_1,s_2 < s'.

(The overloading relation <_P should stay as it is.)

Note that I have chosen the symbol ~_F because the relation
is symmetric now (and even the former <_F was not transitive).

For example, if we have

sorts  NeList < List
opns   ++ : NeList x List -> NeList
       ++ : List x NeList -> NeList

then
	forall x,y,z:NeList . (x++y)++z = x++(y++z)

would be well-formed now, since both versions of ++
have to coincide on NeList x NeList (while it is
ill-formed under the current interpretation).

The modification of the semantics is straightforward.

The overload resolution algorithm could stay as I
presented it in Tarquinia, with the following exception:
The check for equivalence of expansions becomes
more complicated than I originally thought,
-- but this holds also for the original version of the
overloading relation! (So the original algorithm has a bug
-- I have the only excuse that I was just missing the CASL 
tools to develop it from a CASL specification :-).

In fact, for testing if two expansions of an atomic formula 
are equivalent, it does not suffice to just strip off the 
injections and look if all corresponding operation and predicate
symbols are in the equivalence closure of <_F or <_P, resp.
Counterexample:
					      v
sorts s s1 s2 t1 t2 u1 u2 u3 v		   f/ | \f
      s1, s2 < s  		  	  u1  |f  u2
      s1 < u1				 |  \ | /  |
      s2 < u2		   		 |    u    |
      u < u1, u2			 |         |
opns c:->s1			   	 |    s    |
     c:->s2			   	 |   / \   |
     f:u->v 		  		 c:s1     c:s2
     f:u1->v
     f:u2->v

f(c)=f(c) is ill-formed, because there are two non-equivalent
expansions f:u1->v(inj:s1->u1(c:s1)) and f:u2->v(inj:s2->u2(c:s2))
though both expansions have their corresponding operation symbols
in the equivalence closure of <_F.


I have modified the overload resultion algorithm accordingly,
and hope that there are no more bugs (though I still have prove
its correctness).

Greetings,
Till