Re: Semantics of free datatype in presence of subsorting

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

Dear Maura,

> 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.

Indeed, the local environment is something different. It is the context
signature for the datatype declaration. It usually appears as the first
item in the semantic rules.
The signature of the datatype itself does not belong to the local
environment.

I think this misunderstanding causes all the problems you describe
in the rest of your mail. So I would still agree to Peter's proposal.

Greetings,
Till