Comments on CASL 0.97 semantics

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

General comment:

The semantics uses operations on signatures and signature
morphisms. Some of them are defined in section 5,
but are used earlier (e.g. union of signature extensions
is used on p. 19). Moreover, it is assumed that
all rules of section 2 generalize to the more complex
concepts added later (subsorting, section 4, compound IDs,
section 6).
All this becomes nicer if we have a semantics 
parameterized by an arbitrary "institution with syntax"
(where an "institution with syntax" should provide
all the operations on signatures and signature
morphisms that we need), where only sections 2, 4,
and 6.1.1 contain institution-specific material.

SECTIONs 1&2 (BASIC SPECIFICATIONS)

p.2, Doubt 1.1:
The treatment of total functions f:A->B as
partial functions f:A'-o->B with A\subseteq Dom(f=
is a bit funny. Total functions contain some superflous
hidden information.
In particular, two total functions f,g:A->B
with f(a)=g(a) for all a\in A may still be
different because f:A'-o->B and g:A''-o->B
and A' =/= A'' and/or f and g have different
values outside A.
Thus two model may be different just because
of different hidden information of their
total functions. And equality of models
is used heavily in the semantics.
Moreover, composition of these total functions
is not clear to me. 
Therefore, I would stick to the standard
definition of total functions.
I think this is independent of subsorting.

p.3, Doubt 1.2:
Compound IDs are treated in section 6.2 and need not
be introduced here.

p.4, Doubt 1.3:
I think we want to have the signatures to be finite,
and get finite cocompleteness of the signature category.
This suffices for the semantics of CASL.
If a CASL extension happens to allow infinite signatures
presented in some finite (recursive) way, then the
semantics can be extended to infinite signatures easily.

p.4, Doubt 1.4:
OK, why not use dependent types here?

p.6, Prop. 2:
Perhaps the proposition should be moved to section 3
(or at least be restated there).
I have proved the proposition for the subsorted case, 
see a frothcoming study note. The proof is not entirely
straightforward: the treatment of the name space is a bit 
tricky due to overloading and preservation of overloading 
relations by signature morphisms.

p.7, "Unisverse = the set of all data values"
I am not sure if the assumption of such a universe
has advantages. At least, it may cause some foundational
problems: If we want to keep the usual set-theoretic
operations on elements of Universe, then Universe is a class,
not a set, and models become classes, too. Thus model
categories are only quasi-categories.
This is all doable, but is it worth it?
I would instead propose
	Carrier = the class of all sets
which gives the usual notions of model etc-

p.9, Prop. 7:
A sketch of the proof may be found in the abovementioned
study note.

p. 16, Doubt 1.8:
I think it should be stated that theory morphisms between
theories of a suitably restricted form (i.e. signatures
having a ground term for each sort, and axioms being universal
Horn formulae without strong equations in the premises)
admit free extensions.

p. 25:
Why is there no semantics for ALTERNATIVEs (even
if this is trivial here)?

p. 26, first rule:
"s'=s_i for some i (where w=s_1,...,s_n)"
has to be added to the premises.

p. 26, second rule:
s'=s_m
has to be added to the premises.

SECTIONs 3-8

I communicated my comments orally to the authors.

SECTIONs 9&10 (LIBRARIES)

p. 93:
Don't forget that there is a compatibility relation
between static and model global environments
(which should be defined in the relevant sections,
but has to be mentioned here as well).

p. 95, Doubt 10.1:
This is a good idea!

p. 96, first two rules:
The URL? does not appear in the abstract syntax.
Perhaps the abstract syntax for LIBRARY is
a bit misleading: if we put the two rules
for LIBRARY (given in 10.1 and 10.2 resp.)
together, we get
LIBRARY ::= library LIBRARY-ITEM* | library URL? LIBRARY-ITEM*
but what is meant surely is
LIBRARY ::= library URL? LIBRARY-ITEM*

p. 97, first two rules (and subsequent rules):
What is the exact meaning of \uplus here?
In section 6, we have used \cup for a union of
partial functions which is only defined if
the domains are disjoint. Here, because
of the last rule on p. 98, one should allow
that domains are not disjoint, but on the
intersection of the domains, both partial
functions must coincide. (So this means
taking a union of graphs and then looking
if the result is a function).


Greetings,
Till