Re: Semantics of free datatype in presence of subsorting (NEW VERSION)

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

Dear Maura and Anne
> 
> [For the moderator: Anne let me had her comments, so this is a new improved
> version of the message sent on Friday, please forward this version only.
> Thanks
> Maura]
> 
> [Sorry, I have forwarded the previous version to the list before this
> one has reached me. EVERYBODY, please disregard the previous message
> from Maura and read this one only, if it's not too late --- AT]
> 

Sorry, I have read the old version, but a glimpse at the new version
lets me think that my comments apply without modification also to
the new version.

>A first attempt at producing a rule for the free datatype, is to modify the
>rule by Don adding
>- the condition about no common subsorts
>- the axioms requiring images of distinct embedding (or embedding 
>  and constructors) to be disjoint:

>With this semantics, that is the immediate adaptation of the "flat" case, we
>can see 3 problematic cases, producing syntactically correct, but 
unexpectedly
>inconsistent (or simply weird), specifications:
>(do not mind the concrete syntax, that's probably incorrect, but hopefully 
understandable)
>
>1 Overloaded constructors
>  
>  free datatype s = f(s1)|f(s2)
>
>  where s1 and s2 have a common subsort s0

This is clearly ruled out as ill-formed by the condition about 
no common subsorts, so I do not see a problem here.

>2 Interaction between embedding
>
>   free datatype s = s1 | s2
>
>   where s1 and s2 have no common subsort, but for which a term t
>   exists with both sorts. The simplest (and most useless) case
>   is if a constant k exists for both sorts (but in general it applies
>   to functions f:w --> s1, f: w' --> s2 with a common w0<w and w0<w')

This is consistent! But if there is a constant k:s1, k:s2, then
the term k is ambigous. If there is also a constructor k, i.e.

   free datatype s = s1 | s2 | k

then there is a problematic overloading, comparable to 3.

>3 Interaction of embedding and constructor
>
>   free datatype s = f(s1) | s2
>
>   where there is also the declaration
>   
>   total function f: s1 --> s2;
>
>   (or f:s0 --> s3 with s0<s1 and s3<s2....)

I would rule out 3. (and the modified 2. with an overloaded constructor)
as ill-formed by adding something like:
"All the constructors of the free datatype must neither be
in the overloading relation with each other nor with functions
in the local environment".

>In all the above cases the disjointness axioms together with the implicit
>axioms for overloading, make the specification inconsistent (or introduces
>unexected identifications, see the example below).
>In our opinion this is not intended. 

Right, inconsistency is not intended. I would suggest to let these
cases be ill-formed by the above rule. After all, the main guidelines
for free datatypes were the following:

1. The semantics should be the same as for free specs.
2. All cases where 1. causes complications (i.e. when there are
   explicit or implicit axioms) should be excluded, i.e. be ill-formed

Now following 2., it was discussed to exclude subsorts
from free datatypes completely. But Bernd has argued with examples like

free types Zero ::= zero
           Pos ::= succ(Nat)
           Nat ::= Zero | Pos

to allow subsorts in free datatypes.
So we tried to inlcude all cases with subsorts that are still
compatible with 2. Therefore, we have excluded common subsorts, 
but we forgot to take into account the implicit overloading axioms. 
They should be excluded here as well. I hope this now suffices.
Everything else (for example, all your work on "disjoint-as-much-
as-possible") would be far too complex, I fear.

[Just a word from AT: I think I share Till's view here, and hope that
this settles the issue. --- AT]

I have asked Bernd, and he agrees that overloading of constructors 
is not needed in free datatypes. If you need this, use free specs.

Greetings,
Till