Re: Two proposals for additions to CASL

[Till Mossakowski <till@informatik.uni-bremen.de>]

Dear friends,

Andrzej wrote:
>i) are projections necessary in the above?
>
>I have not checked all the details, but I believe the answer is
>negative: any sort-generation constraint with a projection seems to be
>equivalent to the same sort-generation constraint with this projection
>and its target (sub-sort) removed. Can somebody from the subsorting
>group check that this is in fact true? Then the PROJECTION case for
>the GENERATORs might be removed.

Unfortunately this is not true.
Consider the following example:

NAT =
 sorts nat
 preds iseven:nat
 0:nat
 succ:nat->nat
 sort even = {x:nat | iseven(x)}
 iseven(0)
 iseven(succ(x)) <=> not(iseven(x))

Then for the standard model N of natural numbers, we have

(1) N satisfies ({nat},{succ,inj:even->nat})
   (because (pr:nat->even)(0) is an even-value)
but
(2) N does not satisfy ({nat,even},{succ,inj:even->nat,pr:nat->even})
   (because 0 is not generated by any term now)

One could now have the idea not to drop the target subsort and
argue that
(3) N does not satisfy ({nat,even},{succ,inj:even->nat})
and so (2) and (3) are in correspondence, which might be
evidence for "any sort-generation constraint with a projection seems to be
equivalent to the same sort-generation constraint with this projection
*removed* and its target (sub-sort) *not* removed".

But consider
(4) N does not satisfy ({nat,even},{0,succ})
     (because no even-value is generated)
(5) N satisfies ({nat,even},{0,succ,pr:nat->even})

So there is no (well, no obvious) hope to throw out projections by providing
an equivalent generating constraint.

Greetings,
Till