comments on v.0.96

[Tarlecki <tarlecki@lsv.ens-cachan.fr>]

Dear All,

Guess what Michel and me are mainly doing during my visit to Paris...

[Just as well the deadline is quite soon now!  :-) 
--PDM]

Here are some comments on the CASL summary v.0.96, in addition to a
message I sent earlier with two specific proposals for changes.

First, a few comments that in my (our --- let me use the formulae form
the previous message: good things here are from Michel and me, but
mistakes and bad ideas are mine!) view deserve some attention and
perhaps further changes. Then, perhaps just to Peter as the editor of
the summary, a bunch of specific editorial comment which seemed
obvious to me.

[N.B. Andrzej is asking for REACTIONS to the comments below!
 I'm forwarding the editorial comments as a separate message.
 --PDM]

**********************************************************************
More serious comments
**********************************************************************
1. p. 6, just before sect. 2.1.1:

We permit overloading of identifiers across various kinds of entities:
fine. But what about variables, which are not mentioned here?
Overloading variables and constants might lead to strange ambiguities
in the syntax of terms, so maybe they should be kept separate.

2. sect. 2.1.2 and elsewhere.

I must admit, i do not like too much the changes related to the
introduction of constants as separate things. I think that what was
here before, forcing the application of a zero-ary function to the
empty list of arguments, was okay and was quite readable (and any
potential inconveniences might be resolved at the level of a concrete
syntax then). Moreover, this was quite uniform throughout the
language, and everything (e.g. partiality) was nicely symmetric.

Okay: I also buy some of Bernd's arguments about the
possible future interaction with a higher-order extension.

However, if constants are to be treated separately in the language,
differently than functions, then I think we should do this
systematically throughout the entire formalism in a "proper" way.
Otherwise we loose some sense of uniformity of the language.

For instance:

a) I would expect a full symmetry in the treatment of partiality here,
with no ad hoc simplifications:

   FUN-TYPE ::= TOTAL-CON-TYPE | PARTIAL-CON-TYPE |
                TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE

   TOTAL-CON-TYPE ::= total-con-type SORT

b) I would introduce the constants as such throughout the language,
with their own category of identifiers, symbols, declarations etc.

c) It seems inappropriate that the language departs from the
presentation of the underlying institution: so, we should start
talking about constants there as well.

d) the separation of (closed) SPECs, their definitions and their use,
from the GENERIC-SPECs, their definitions and their use (via
instantiation) was done in accordance with this --- okay.

e) Similar changes are required in architectural specifications, where
we should consequently separate parameterless units and the references
to them in result terms from parameterised units and their
applications in result terms. Actually, this would be getting quite
tedious:

 UNIT-DECL-DEFN	    ::= UNIT-DECL | UNIT-DEFN |
		        PARAM-UNIT-DECL | PARAM-UNIT-DEFN
 UNIT-DECL 	    ::= ...
 UNIT-DEFN	    ::= ...
 PARAM-UNIT-DECL    ::= param-unit-decl PARAM-UNIT-NAME PARAM-UNIT-SPEC
 PARAM-UNIT-DEFN    ::= param-unit-defn PARAM-UNIT-NAME PARAM-UNIT-TERM
 PARAM-UNIT-NAME    ::= SIMPLE-ID

 ... etc, etc, etc ...
(Peter: please let me know if you really want me to write all this in
detail --- maybe I would withdraw this comment then :-)

Can we please consider going back to what was there before, with
constants as a special case of functions?

I think Michel shares the feeling, anybody else?

3) sect. 2.5, last sentence:

In the case of open datatypes, it makes little sense to presume that a
selector is total if there is only one clause in a datatype
declaration --- after all, further constructors may be added later,
and moreover, there may be values of a datatype which are not built
using any constructor at all...

4) sect.2.6:

As it is now: ATTRIBUTIONs are treated just as certain abbreviations
for axioms -- and I like this. However, as far as i can see, there is
then no decent way to allow them to influence the possible syntax of
terms: stating that a binary "plus" is associative does not introduce
to the abstract syntax legal applications like "application plus
TERM+" (with arbitrarily long list of argument terms). If the
intention was to allow such syntactic consequences to be drawn, then I
believe attributions would have to be attached directly to function
declarations.

5) sect.4.1, p. 13:

It is stated here that an embedding declaration cannot lead to
implicit (other than imposed by ISO-DECLs) cycles in the sort
ordering. I believe that in Paris/Lille we were discussing a stronger
requirement: that in no context a new cycle can appear, except for an
explicit declaration in ISO-DECL. I do not think this is ever
mentioned now in the summary.

However, i think now that perhaps this was a suggestion which goes a
bit contrary to the overall language design. If I recall right, the
only reason for this was that "if a new cycle is introduced
implicitly then this is probably an error". In other similar cases
(e.g. name clashes, notably in instantiations of generic specs) we
have taken the opposite view: "okay, this might have been an error, so
perhaps a tool should warn the user, but since this makes perfect
semantic sense, we do not throw this out as a possibility for the
user".

Perhaps the similar philosophy should be applied here, and we should
allow cycles to be introduced by language constructs?

6) This is more a question to the subsorting group than a comment: do
we have a decent "type-checking" algorithm to type terms and formulae
and check if they are well-formed? (sorry if this was written
somewhere and I missed this among the tones of CoFI material).

7) sect. 6.1.1.

I must say that again, i do not like the simplification of the
abstract syntax for SYMB-MAP, which now pushed some of the
requirements previously given in the grammar in a context free way
(that things of the same categories are mapped to the things of the
same category) to the semantics (context checking...).

Also, this introduces here some questions about what happens when a
symbol overloaded between various categories (say, identifier that is
both a function and a sort) is used? Do we need a way to indicate that
an identifier is used as a sort, or is it implicit in the abstract
syntax already?

8) sect. 6.1.2.

EXTENSIONs should have at least two SPECs in the chain, right?

In fact, since the role of the first SPEC is different (at least
w.r.t. CONSERVATISM), we should perhaps separate it out, so:

   EXTENSION ::= extension SPEC CONSERVATISM? SPEC+

Aha: just above: maybe we should require that there are at least two
SPECs in a union (just as we did for some reason --- mysterious to me
--- for disjunctions and conjunctions).

9) p.20, sect. 6.2:

Just a tiny complaint: we have removed multiple SPECs as things to be
extended in EXTENSIONs, but we have retained this possibility for
generic specs. This is a bit un-uniform: I think I understand the
reason for the latter, without fully appreciating the reason for the
former.

Anyway: one nice side-effect is that conservatism is now always
required uniformly on all the extended SPECs. A nice semantic
consequence of this is that in the cases when an instantiation of
generic specs leads to a pushout signature (no unintended name clashes
between the body and the actual parameter) then both persistency and
freeness of the body over the formal parameter are preserved (I think).

10) p.27, sect.9, 2nd paragraph:

I'm afraid this is not "quite true": if my understanding of things is
correct, we do not have referential transparency now (see trivial
examples below).

The point is that, as rightly explained in sect.6.2, p.20, just after
the first group of clauses, naming a specification is a semantically
meaningful operation, which fixes the "local environment" for the
specification expression to be empty. Consequently, the structure of
the expression is not "visible" anymore.

Overall though I do not think that this is so terrible, and we can
live with this --- just dropping this paragraph...

11) I am running out of steam, so the last one will be sketchy :-)

can somebody re-raise the issue of linear vs. non-linear visibility of
declarations within lists of basic item, please...

If the proposal from my earlier message would be accepted, and
consequently type-declaration groups would be back, then any real need
for non-linear visibility would disappear. As far as I can see, in all
other cases we can (and in my view, we should) write basic specs so
that linear visibility is maintained.

And a related issue: once linear visibility would be restored then
perhaps we could go back to the idea of local declarations (SIG-DECLs)
within basic specs only, rather than locality introduced only at the
level of structured specs?

[See separate message for "Editorial comments".  --PDM]

**********************************************************************
Examples of the lack of referential transparency
**********************************************************************

For instance (sorry for awkward concrete syntax),

 SP1 = [sort s, const a: s] translated by {s |-> s'}

is a legal declaration, yielding a spec with a single sort s' and a
constant a: s'.

Then also:

  SP2 = extend [sort s] by SP1

yields a legal specification with two sorts s and s' and a constant
a:s'.

However, the expression

  extend [sort s] by
	( [sort s, const a: s] translated by {s |-> s'} )

is not legal.

Moreover, even if everything is well-formed, we may loose equivalence
of the specifications involved.

For instance:

 SP3 = free [sort s, const a: s]

yields a specification with a unique (up to iso) one-element model.
Then:

 SP4 = extend [sort s, const a:s] by SP3

is equivalent to SP3.

But

SP5 = extend [sort s, const a:s] by free [sort s, const a:s]

admits any algebra as a model!
**********************************************************************

That's all, more than enough I'm afraid: apologies for too much of
text and for reviving some of the issues again, but I just want to be
sure I like what we submit to WG1.3...

Best regards,

Andrzej