Dear friends,
I have now got time to think about the overloading relation proposed by
Andrzej and supported Till, and also on how the overloading relation can be
extended to higher-order functions and predicates. I am really in favour of
using Andrzej's relation instead of the current one as it fits perfectly with
my ideas for an overloading relation for higher-order functions.
So unless Till finds any problems concerning an overloading resolution
algorithm, I vote for the new relation.
Definition 1
------------
Andrzej's overloading relation, ~, for functions is defined as follows:
f1:w1->s1 ~ f2:w2->s2
iff
there exists w' with w' < w1,w2 and
there exists s' with s1,s2 < s'.
Definition 2
------------
I have (in another context) used the following overloading relation for
higher-order functions:
f1:t1 ~~ f2:t2
iff
there exists an upper bound t' of t1 and t2 wrt. <+-
where <+- is the contravariant subsort relation on function types
induced by the subsort relation < on (basic) sorts, i.e.
w1->s1 <+- w'->s' iff w' <+- w1 and s1 <+- s'
s <+- s' iff s < s' for (basic) sorts s and s'
Fact
----
For the first order case ~ and ~~ are the same.
Proof:
f1:w1->s1 ~ f2:w2->s2
<=>
there exists w' with w' < w1,w2 and
there exists s' with s1,s2 < s'.
<=>
there exists an upper bound w'->s' of w1->s1 and w2->s2 wrt. <+-
<=>
there exists an upper bound of w1->s1 and w2->s2 wrt. <+-
Cheers,
Anne
PS I will be away from my mail the rest of this month.