Re: Semantics of free datatype in presence of subsorting

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

Dear Peter,

> Regarding the following:
> 
> 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.
> 
> I'm afraid that the above would seem overly complicated in the CASL
> Summary...  Wouldn't it be enough to extend my proposal above with
> something like:
> 
>   For each sort, the terms must also be distinct from those
>   expressible using operations from the local environment (with
>   variables ranging over the sorts declared in the latter).

I like this proposal, because it is more user-friendly.
Note, however, that it is a bit more restrictive, because it rules
out some ad-hoc overloading, like

free type bit_term ::= 0 | 1
free type byte_term ::= 0 | 1 | 2 | 3 | 4 | 5 | ... | 255
free type add_term ::= __+__(bit_term,bit_term) |
__+__(byte_term,byte_term)

... but I do not care so much about this example.

In any case, the semantics should include a proof that the restriction
does the job (i.e. the semantics of free type xxx is the same as
that of free (type xxx)).

> The motivation for these formulations is that most users may prefer to
> regard the values of free datatypes as terms, and it may be helpful to
> formulate conditions on this basis.  In fact it might be even gentler
> to say first:
> 
>   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.

With this formulation, it is unclear whetherDoes "these sorts" refers
to all sorts in the local environment, or only those which are used
in the datatype declaration.

The following is more precise:

  When the datatype declaration uses some sorts from the local
environment,
  the terms considered allow also variables over all the sorts from the
  local environment.

Greetings,
Till