Re: Comments on CASL v0.95 FINAL DRAFT

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

[As comments are still coming in, the deadline has now been relaxed a
couple of days: to WEDNESDAY 11 December.  After that, we shall have
to try and finalize the Tentative Design, leaving any remaining
problems to study by the various groups over the next months. 
So this current flood of messages won't last long... --PDM]

Dear Peter, dear all,

>I do not like the exclusion of non-empty carriers, mainly because
>this means that other existing frameworks cannot be embedded directly
>in CASL. The only embeddings of empty-carrier frameworks
>into non-empty carrier frameworks I know do not preserve
>the conditional fragment, which is bad since the conditional
>fragment allows easier theorem proving.
>
>[It's a pity that this argument wasn't raised - as far as I recall -
>when we discussed the issues related to variables in Edinburgh. --PDM]

Sorry, but the disucssion was very quick. I raised some argument in
favour of inclusion of empty carriers, but it was not accepted. And indeed,
there seems to be little argument except that other frameworks should
be embeddable. Actually, Hans-Joerg made this argument when I was back
in Bremen.

>[Perhaps there is a third problem: users may prefer to ignore the
>possibility of empty models altogether...  From the fact that empty
>models are allowed in the *theory* of (all?) existing frameworks, it
>need not follow that they are A Good Thing!   But of course we would
>like to have faithful embeddings of as many specs in existing
>frameworks as possible.  --PDM]

If the user wants to ignore empty carriers, she/he can just state
exists x:s . true for each sort s. Perhaps there should be
an abbreviation of this (e.g. 
     nonemptysort s
stands for
     sort s
     axiom exists x:s . true
).

[Or perhaps "sort s" should be the default, with the possibility of
writing "possibly-empty sort s" if one really wants it?  --PDM]

>"A type-definition group TYPE-DEFN-GROUP determines both part of
>a signature and some sentences."
>... but that is not the whole story, because it also determines
>some freeness requirement! So either freeness constraints should
>be added to the institution (which does not imply that they become
>accessible directly in the language), or TYPE-DEFN-GROUPs should be
>considered as SPECs.
>
>[Agreed.  But which is better?  --PDM]

I think the latter, because freeness really is an "in-the=large" feature. 
I support the compromise you suggested within Andrzej's comments.

>Note that <=F is no longer transitive (counterexample:
>sorts s,t,u,v,w
>      s,u < t
>      u,w < v
>const c:s
>      c:u
>      c:w
>Then c:s <=F c:u and c:u <=F c:w, but not c:s <=F c:w).
>All we can say that <=F is reflexive. So the symbol <= perhaps 
>is a bit misleading here?
>
>[Agreed.  Kindly propose a better symbol. --PDM]

For example, ~_F and ~_P - even if this is often used for equivalence relations.
Actually, my intuition is more that the two profiles are considered
to be equivalent than that one is less than the other.

>A way to make <=F transitive would be to replace the relation
>"s and s' have a common supersort" by its equivalence closure
>(=transitive closure, in this case).
>This would complicate the semantical definitions a bit (a coercion
>function between equivalent pairs of sorts has to be defined)
>but not much.
>
>[We have generalized <=F from requiring identical result sorts to
>allowing result sorts with common supersorts.  This was to make more
>terms that look identical - and have the same sort - also have the
>same value, when argument sorts in profiles are related by subsort
>embeddings; then the ambiguity of their parsing is deemed harmless.
>In the above example, the only harmlessly-ambiguous terms are c:t and
>c:v, both of which include only one of c:s, c:w as possible parsings.
>If the user writes c:u in a context that allows both sorts t and v,
>this seems to be simply ambiguous, and should be regarded as
>ill-formed, I think. If transitivity of <=F would make c:u
>well-formed, please clarify how the proposed coercion would work. --PDM]

Actually, D(c) (and a fortiori D(c:u)) is already well-formed in the present 
proposal,
since D(c:s), D(c:u) and D(c:w) are equivalent expansions of D(c).
This is because the relation "is an equivalent expansion of" is
an equivalence relation (since it was designed to capture semantical
equivalence) and hence transitive.
But if c:u is used in another context, say f:t->s and f:v->s
and we write f(c:u), then this is ill-formed. But this ill-formedness
has nothing to do with the transitivity discussion above: even
f(x:u) would be ill-formed.

So the conclusion is that coercions are not needed.

Greetings,
Till