Re: Semantics of free datatype in presence of subsortingPeter D. Mosses wrote:

[Maura Cerioli <cerioli@disi.unige.it>]

....
>   The alternatives of a free datatype must have no ground terms in
>   common with each other, nor with the local environment.
> 
> and then add:
> 
>   When the datatype declaration uses sorts from the local environment,
>   the terms considered allow also variables over these sorts.
> 
Dear Peter (and all),
I'm trying to verify if Till's proposal and yours are different wording of the
same intuition, but I'm afraid that I'm missing the very basic.
Sender: owner-cofi-semantics@brics.dk
Precedence: bulk
Reply-To: cofi-semantics@brics.dk

Indeed, I'm not sure if I understand correctly what the "local environment"
is. 
If it is (as I expect by the use of the word "local") the environment built by
the declaration local to the free data type construct, then the first
statement seems to rule out subsorts as alternatives, because the term of that
alternative are of course terms of the data type, that is a sort in
the local environment. 
Moreover, if we modify the statement into
	The alternatives of a free data type must have no ground terms in
	common with each other, nor with any sort in the local environment but 
	the data type they are alternatives of.
Then, I think that examples like (sorry for the syntax, that's probably wrong)
free data types
LIST  = nil | cons(hd:?Elem;tl:?List);
LIST2 = nil | LIST | append(LIST2;LIST2);
are to be considered correct, while from an intuitive point of view this
should be rejected, as the overloading of the constant nil identifies the
empty list of sort LIST2 and the list with one element that's the empty list
of sort LIST.
Till's formulation detect this problem, as the overloading relation is
modified (there is a new relation between the two nil's).

Finally, it seems to me that cases where one data type has two constructors
with the same name and different argument sorts, but the argument sorts have a
common subsort, are not detected as well (nor clashes between constructors and
already defined functions).

I hope that all these problems are not simply due to my poor
understanding of English. 

I'm currently in the process of incorporating Till's suggestions and comments
to produce a new (final, hopefully) draft. Thus, I would greatly appreciate if
we fix this point soon.

Ciao
Maura