Comments on CASL v0.95 FINAL DRAFT

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

Comments to CASL Language Summary 0.95 Final Draft

[The moderator has not had much time to ponder the technical issues
below, but has inserted some immediate reactions anyway... --PDM]

page 2, section 1.2 
-------------------
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]

There were two problems with empty carriers which can be solved
as follows:
1. The (part of a) specification
      x:elem, s:stack
      not is-empty(push(x,s))
      is-empty(empty)
does not give what we want if is-empty(empty) is universally
quanitifed wrt x:elem, s:stack, so just take those variables
which occur freely.

2. From the axioms
       x:s
       a=f(x)  
       b=f(x)
we are not allowed to infer
       a=b
but only
       forall x:s . a=b
which is counter-intuitive.
This can be solved in two ways (I prefer b):
a) Following Goguen and Meseguer, add a list of variables 
to each axiom:
AXIOM   ::=  VAR-DECL+ FORMULA
Then a global VAR-DECL would just contribute to the local
VAR-DECL+ of each axiom where the variable occurs freely. Then
       x:s
       a=f(x)  
       b=f(x)
means the same as
       x:s . a=f(x)
       x:s . b=f(x) 
from which we can infer
       x:s . a=b
but not
       a=b

b) Leave
AXIOM   ::= FORMULA
as it stands, but change the rules of the proof system in such
a way that it deals with closed and open sentences differently,
following D. Scott, "Identity and existence in intuitionistic
logic", Lect. Notes Math. 753.
Then
       x:s
       a=f(x)  
       b=f(x)
stands for
       forall x:s . a=f(x)
       forall x:s . b=f(x) 
from which we can infer
       D(x) => a=f(x)
       D(x) => b=f(x)
and then
       D(x) => a=b
and
       forall x:s. a=b
but not
       a=b

Note that Scott's proof rules are only sound if open variables
may be undefined (this fits better with both empty carriers
and substitution), but if we only consider derivations
of closed sentences from closed sentences, this is also sound
for the CASL semantics (i.e. only intermediate open formulas
have to be interpreted differently). See also my comments
on version 0.92 (or 0.93?).
I also can promise to design a proof system for the "in-the-small"
part of CASL along these lines.

[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]

page 6, section 2.2:
--------------------
The treatment of VAR-DECLs was discussed differently
in Edinburgh: a VAR-DECL just declares the sorts of free variables
in the axioms. This is be semantically equivalent to the universal
closure wrt the free variables (but only if empty carriers are forbidden,
also equivalent to the universal closure wrt all declared variables).

[Right, that is a better way of explaining it. --PDM]

page 5, above 2.1:
------------------
"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]

page 7, 2.3.1 Quantifiers
The overriding property of nested quantifications over the same
variable is a property of satisfaction in the institution, and
not of a language construct. So it should be moved to 1.4 (where
it already occurs implicitly by refering to "as usual in first-
order logic").

page 10, 3.1 Signatures, 2nd para
---------------------------------
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]

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]


page 18, last para:
------------------
So the semantics of a GEN-SPEC is a textual, macro-expansion
semantics and not a model-theoretic semantics?

[The informal explanation exploits an analogy; this does not have
implications for the formal semantics, which is indeed to be
model-theoretic. --PDM]

page 19, 6th para:
------------------
The semantics of a SPEC-INST has to be defined not through a
UNION, but through an EXTENSION, because a UNION cannot deal
with PERSISTENT-SPECs and the freeness declarations
wouldn't have the intended effect. 

Section 8, Architectural Constructs:
------------------------------------
The former ARC-SPEC-REF, allowing to re-use arc specs within
other arc specs, is missing now. Can the same effect be achieved
by supplying for the UNIT-SPEC which is needed within a UNIT-DECL 
just a SPEC-NAME which is bound to an ARCH-SPEC?

[If I followed the discussion in Edinburgh well enough, Andrzej's
point was that such a reference would be misleading, not giving the
intended effect.  ANDRZEJ: please clarify this!  --PDM]

Some minor comments/typos:
--------------------------
page vi: Zhenyu Qian attended the subsort meeting in Bremen, but is not
an author of [MC++-1].

page 2, 2nd line: typo before "Section 2"

page 4, 1.5 Proof System:
The fact that satisfaction is 2-valued should be moved to 
section 1.4 Satisfaction.

page 5, 2.1 Signature Declarations:
typo SORT-DEC --> SORT-DECL

page 10, last line should read:
... s <=S s' by a total embedding function (from s into s'), a partial
projection ...

page 13, last item in both enumerations:
... profiles which are in the overloading relation ...

Till

[Many thanks for all the comments!  --PDM]