Re: Semantics of free datatype in presence of subsorting

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

[Dear Sematicists,

It seems that the problem with overloading caused by free data types
in the context of order-sorted signatures found some solution,
accepted at least by the people directly involved in the work on this
topic. Here is the remaining correspondence, following the earlier
messages indicating the problem. Please note that towards the end,
Till's proposal in fact contains a small adjustment to the language
design. Any further comments welcome, also perhaps to the language
design list.

Below:  AH = Anne Haxthausen (in consultation with Maura Cerioli, I understand)
	TM = Till Mossakowski

AT]

AH> 
AH> Dear Till,
AH> 
AH> Thank you very much for your quick reply. We (Maura and I) have
AH> the following comments/questions:
AH> 
AH> >>1 Overloaded constructors
AH> >>
AH> >>  free datatype s = f(s1)|f(s2)
AH> >>
AH> >>  where s1 and s2 have a common subsort s0
AH> >This is clearly ruled out as ill-formed by the condition about
AH> >no common subsorts, so I do not see a problem here.
AH> 
AH> The language summary only says "all the sorts that are embedded in
AH> the declared sort by the alternatives must have no common
AH> subsorts". It does not say that the domains of overloaded
AH> constructors must not have no common subsorts.
AH> So this case is not ruled out as far as we can see.

TM> Oh yes, you are right.
TM> So this example has to be ruled out as well (and indeed it is ruled
TM> out by my suggestion).

AH> >>2 Interaction between embedding
AH> >>
AH> >>   free datatype s = s1 | s2
AH> >>
AH> >>   where s1 and s2 have no common subsort, but for which a term t
AH> >>   exists with both sorts. The simplest (and most useless) case
AH> >>   is if a constant k exists for both sorts (but in general it applies
AH> >>   to functions f:w --> s1, f: w' --> s2 with a common w0<w and w0<w')
AH> >
AH> >This is consistent!
AH> 
AH> We get the following inconsistent axioms:
AH> 
AH> 1. overloading axiom :
AH>    forall z : w0 :- Emb(s1->s)(f(Emb(w0->w)(z))) = Emb(s2->s)(f(Emb(w0->w')(z)))
AH> 2. disjointness axiom :
AH>    forall x : s1, y : s2 :- ~ (Emb(s1->s)(x) = Emb(s2->s)(y))
AH> 
AH> >But if there is a constant k:s1, k:s2, then the term k is ambigous.
AH> 
AH> We don't see why it should be ambigous.
AH> Indeed, after the introduction of a common supersort for s1 and s2, the
AH> expansions em(s1->s)(k:s1) and em(s2->s)(k:s2) are equivalent.
AH> In any case the point is, that the interpretation of
AH> em(s1->s)(k:s1) and  em(s2->s)(k:s2) should result in the same element,
AH> while the disjointness axiom says:
AH>    ~ (Emb(s1->s)(x) = Emb(s2->s)(y))
>

TM> You are right again. Sorry, I had in mind an old version of the
TM> overloading axioms, without the common supersort.

AH> >"All the constructors of the free datatype must neither be
AH> >in the overloading relation with each other nor with functions
AH> >in the local environment".
AH> 
AH> This restriction gives a more simple solution than the one we proposed
AH> and we prefer it in that respect. However, we can only see that it is
AH> a solution for case 1 and 3, but not for case 2.
AH> For instance, it does not make the following specification
AH> statically incorrect:
AH>   sorts s1, s2
AH>   const k: s1; k:s2
AH>   free datatype t= s1| s2
AH> 
AH> As for our solution the restriction can apply only to the
AH> symbols defined so far, so that
AH> 
AH>   sorts s1, s2
AH>   value f : s1 -> s2
AH>   free datatype s = f(s1)| s2
AH> is statically incorrect, but
AH> 
AH>   sorts s1, s2
AH>   free datatype s = f(s1) | s2
AH>   value f : s1 -> s2
AH> is correct but inconsistent, which we find weird.

TM> OK.
TM> So let me try again:

TM> "A free datatype must not contribute in any way to the
TM> overloading relation. In particular, this means that all the 
TM> constructors of the free datatype must neither be
TM> in the overloading relation with each other nor with functions
TM> in the local environment. Further, the introduction of new
TM> subsort relationships through the free datatype must not
TM> lead to the addition of profiles from the local environment 
TM> to the overloading relation."

AH> I like the suggestion by Till.  

==============================================================================