[CoFI] Overloading relations

[Anne Haxthausen <ah@it.dtu.dk>]

[This message has also been submitted to cofi-semantics, so some
subscribers may receive two copies - apologies. --PDM]

Dear friends,

I have now got time to think about the overloading relation proposed
by Andrzej and supported by Till [see the message "New overloading
relation" by Till that appeared on cofi-language on 20 June --PDM],
and also on how the overloading relation can be extended to
higher-order functions and predicates.  [The extension to predicates
is already being considered by Till; see the appended message. --PDM]

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.

[I'm taking the liberty of appending a message that Till sent just to
those working on the semantics of subsorts, in reply to a comment of
mine concerning an objection raised by Maura Cerioli:

  Date: Thu, 3 Jul 1997 14:30:01 +0200 (MET DST)
  From: Till Mossakowski <till@Informatik.Uni-Bremen.DE>

  Dear all,

  MC> Moreover, I think that it is quite strange the difformity between functions
  MC> and predicates.

  PDM>There I'm inclined to agree with you.  Till, why not change to ~_P
  PDM>accordingly? 

  At first glance I see no problem here, and it would indeed make
  things more uniform. I.e.

  p_1:w_1 ~_P p_2:w_2

  iff

  there exists w' with w' < w_1,w_2.

  I will revise the overloading resolution algorithm accordingly,
  and tell you if there are any problems.

  [So no news is indeed good news :-) but please tell us also if there
  are no problems! --PDM]

  Greetings,
  Till

--PDM]