Re: Two proposals for additions to CASL

[Michel.Bidoit@lsv.ens-cachan.fr (Michel Bidoit)]

[APOLOGIES to all those subscribers to cofi-language who don't have
the time or energy to keep up with all this.  Anyway, the current
flood of messages on this list today should subside after I go home
this evening... even more so after the DEADLINE FOR v0.96 COMMENTS ON
MONDAY! --PDM]

Dear All,

A few immediate reactions to Peter's proposal:

>> COUNTER-PROPOSAL: Combine sort generation with arbitrary groups of
>> declarations.

1) It seems that indeed this would allow to achieve in a reasonably concise
way everything which we had so far in CASL, including our proposal for the
generated datatype definitions.

Two small technical limitations:
  (i) one restriction would be that you cannot use a subsort
embedding and projection separately: each time you want to use a subsort
embedding as a generator, you have to throw in the corresponding subsort
declaration, which also throws in the corresponding subsort projection, and
vice versa; we agree that (looking at Till's example indicating when this
might matter) this should not be treated as a major problem.

[Rather: the semantics decides whether to throw in projections or not,
uniformly. --Peter]

  (ii) When a bunch a data type declarations is constrained in the way
Peter proposes, the induced sort generation constraint lists unnecessarily
selectors as generators, which may be misleading at least for tools,
induction schemata, etc.

[Rather: the semantics decides whether to throw in selectors or not,
uniformly. --Peter]

2) Nevertheless, we still think that the extra generality Peter's proposal
provides is somewhat illusory, since in most (if not all) practical
situations, generating groups one would write could be naturally reduced to
generated datatype declarations or would require a lot of repetitive
declarations which would make them close to a sort generation constraint as
we have so far in CASL.

[We have two different ways of declaring a constructor function: using
a FUN-DECL and using a DATATYPE-DECL.  Unless these could somehow be
combined, different users might use the one or the other, and I don't
see a reason to favour just one of the styles concerning generation. 
--Peter] 

3) Very informally, we feel that Peter's proposal introduces a kind of
intermediate level between basic items and structured specs, which we don't
like very much, but since this intermediate level expands semantically to
lists of basic items [i.e. signature, sentences --PDM] anyway, this is
acceptable. 

4) Another small informal complaint: so far in CASL we have allowed multiple
declarations of the same thing, where at least our intuition was that
subsequent redeclarations are superfluous and can be omitted, and perhaps
even should cause some warnings from tools...
Peter's proposal breaks this informal understanding, since redeclaration of
a thing in a sort generation group is of course semantically meaningful.

[Up to and including v0.95, re-declaration was illegal.  In Paris (on
the basis of feedback from Semantics, I think, but also so that UNION
and EXTENSION would become more similar) we decided to allow it.
Tools could presumably suppress warnings about re-declaration that
originate from inside a SORT-GEN construct. --Peter]

OUR CONCLUSION:
Overall we think that Peter's proposal is acceptable, and if people (or the
summary editor :-) find it attractive, we accept it as well. 

[Those who don't like it are asked to provide alternative solutions to
the problem of concise sort generation - or to express support for
Andrzej and Michel's original proposal, which appears to be its only
competitor at the moment. --PDM]

However, we would like to suggest some small changes:

IMPORTANT: Yes, we would prefer VAR-DECLs and AXIOMs moved out of
SORT-GENs. Thus the syntax would be something like that:

>> ! BASIC-SPEC       ::=  basic-spec BASIC-GROUP*
>> ! BASIC-GROUP      ::=  BASIC-ITEM | SORT-GEN
>> ! BASIC-ITEM       ::=  SIG-DECL | VAR-DECL | AXIOM
>> !!!                  |  ATTRIBUTION
>> 
>> !!! SORT-GEN       ::=  sort-gen SIG-DECL+
>> 
   !!! SIG-DECL	      ::= ... | DATATYPE-DECL

SIG-DECLs are now the only declarations which introduce new stuff to the
signature. We may also consider moving predicate declarations out of
SORT-GENs, but this seems intuitively less crucial than moving AXIOMs and
VAR-DECLs out.

[OK, I agree it seems nicer that way. --Peter]

And two minor points:
a) Yes, we might need some special form of simplified redeclarations in
SORT-GENs, which would at the same time indicate that the redeclaration is
intended for these generation constraints. 

b) Perhaps there should be something special done in the expansion of
SORT-GENs for data type selectors...

Best regards,
Andrzej and Michel

PS: Without getting into any discussion of the specific comments on our
generalization of sort generation constraints, just one main point: yes, we
wanted to be able to express in CASL whatever the institution offers; hence
the need for generalization.

[I thought the institution allowed one to separate embeddings from
projections.  But perhaps if one only considers the results of
reducing from the subsorted institution, that's not expressible. --Peter]