Re: Two proposals for additions to CASL

[pdmosses@brics.dk]

Dear All,

[Peter is speaking as himself, not as the Summary editor, in this message.
 --PDM]

For those who are too busy (e.g. working on concrete syntax :-) to
read to the bottom, let me reveal the punch-line straight away:

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

Here's the motivation and details.

Andrzej (and Michel) wrote:

> **********************************************************************
> PROPOSAL 1. Add to the current data type declarations a possibility to
> require reachability (generation by constructors) of the sorts
> introduced.
> **********************************************************************
> ...
> However, a very typical situation is also when we want to indicate
> that the data type declared is generated by the constructors provided,
> without necessarily imposing freeness. There are many typical examples
> around where one defines constructors of a data type without fixing
> (perhaps: without fixing yet) the details of their mutual relationship
> imposing at once the generation requirement.  To indicate what I mean,
> I add a trivial example of this situation at the end of this message
> in appendix A :-); further examples, indicating other sources of such
> a need as well, may be found for instance in Michel's thesis.

OK: if this situation is so typical (for a popular methodology) we
should definitely make it possible to express the generation
requirement concisely in CASL.

In PLUSS (see the Catalogue) and Michel's thesis, however, the
generation requirement is expressed by separating declarations of
"operations" from those of "generators":

  sort: S  generated by: ...  operations: ...

Now in CASL v0.96 we have 2 ways of declaring (sorts and) functions:
by ordinary declarations, and by DATATYPE-DECLs.  It seems to me that
the natural generalization would be to allow "generatedness" to be
added concisely in *both* cases, not only in the latter case (unless
we insist that everyone uses DATATYPE-DECL, and remove FUN-DECL from
CASL altogether - but I guess that Andrzej isn't advocating that... :-)

> To sum up, here is a possible way to realise the above idea:
> 
>   BASIC-ITEM     ::= ... | DATATYPE-GROUP
> 
> (removing DATATYPE-DECL as a case for BASIC-ITEM)
> 
>   DATATYPE-GROUP ::= datatype-group OPENNESS? DATATYPE-DECL+
>   OPENNESS       ::= open
> 
> and leaving DATATYPE-DECLs as they were. 
> ...
> Of course the abstract syntax chosen and the names used above are a
> bit ad hoc, so any better proposals would be welcome.

See below.

> NB: It is perhaps worth noting that in the context of first-order
> logic axioms, freeness does not in general impose reachability, see
> appendix B.

Thanks, I hadn't realized that...  So in general, for induction to be
sound, it is *not* sufficient to impose freeness?!  Perhaps in some
later message you might indicate the restrictions on the sentences
that are necessary for freeness to guarantee soundness of induction.

> **********************************************************************
> PROPOSAL 2. Generalise sort-generating constraints as now given in CASL.
> **********************************************************************
> 
> This is somewhat related to the previous proposal: I cheated a bit
> above, since in fact the sort-generation constraint that is expected
> from a datatype definition group in general cannot be now expressed in
> the CASL language. The problem is that in the presence of subsorts,
> and hence subsort embeddings and projections, we are not able to name
> in CASL all the operations that occur in the many-sorted signature to
> which an order-sorted signature expands: subsort embeddings and
> projections remain anonymous.

Is that really a problem?  A datatype definition group doesn't have to
expand into something in (the rest of) CASL, only into signature and
sentences of the underlying institution, where we do have the required
names to express the intended constraint - just as you do for the new
construct that you propose:

> ...
> The most general form such a new sort-generation constraints might
> have therefore is:
> 
>    SORT-GEN    ::= sort-gen SORT+ GENERATOR*
>    GENERATOR   ::= EMBEDDING | PROJECTION | FUN-SYMB
>    EMBEDDING   ::= embedding SORT SORT
>    PROJECTION  ::= projection SORT SORT

Frankly, I find the ingredients of this construct far too close to
ordinary SIG-DECLs to justify keeping them separate.  (They would
probably get similar symbols in concrete syntax too, adding to the
confusion.)

Moreover, I find it confusing to separate the embedding and projection
functions of a subsort inclusion - and seeing Till's examples, where
this makes a difference, only reinforced this feeling.

> I hope that the meaning is clear: a SORT-GEN as above expands to a
> sort-generation constraint in the many-sorted institution with the
> corresponding function symbols given either by their names or as
> implicitly named subsort projections and embeddings.
> 
> I believe that some generalisation in this direction is necessary, so
> I put the above forward.

It's not clear to me whether you really want something more general
than can be expressed by a generated datatype definition group, or
simply "equal rights" concerning expressiveness of generatedness for
sorts, subsorts, and functions declared by SIG-DECLs?

Anyway, let me make a counter-proposal which, I believe, gives the
required generality and conciseness without burdening the syntax
unduly.

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

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

! SORT-GEN         ::=  sort-gen BASIC-ITEM+

The distinction between BASIC-GROUP and BASIC-ITEM is to avoid
multi-level nesting of groups; it doesn't affect the explanation of
BASIC-SPEC.  One might prefer to restrict BASIC-ITEM further, putting
e.g. VAR-DECL and AXIOM in BASIC-GROUP instead.
 
For the new SORT-GEN proposed above, the Summary might run as follows:

  A sort generation SORT-GEN determines the same elements of signature
  and sentences as its list of BASIC-ITEMS, together with a
  corresponding sort generation constraint as a sentence of the
  underlying institution: all the sorts declared by the BASIC-ITEMs are
  generated by all the functions declared by the same.  Note that this
  includes the embedding and projection functions associated with any
  declared subsort inclusions.  Any VAR-DECLs, AXIOMs, or ATTRIBUTIONs
  in a SORT-GEN do not affect the sort-generation constraint.
  A SORT-GEN is ill-formed if it does not declare any sorts.

Note that this proposal does *not* involve treating generation
constraints at the level of structured specifications (in contrast to
the situation with free extensions, it would be semantically
complicated, they tell me).

This proposal is an instance of a general design principle for CASL,
which I've had in the back of my mind all the time, but perhaps it's
not been stated explicitly before:

**********************************************************************
PRINCIPLE: Do not require the user to repeat things unnecessarily.
**********************************************************************

Thus we allow lists of symbols (of the same kind) to be declared
together with the same type; we allow multiple variables in the same
quantification; we allow declarations of symbols to be made local
(partly) to avoid having to list them again in an explicit hiding.

In my view, such "factorization" of specifications is pragmatically
very beneficial.  (It could be achieved at the level of concrete
syntax, but then one would always have to deal with the expanded
version in tools, which might be bothersome.)  I guess the design of
PLUSS was consistent with this principle?

The problem with SORT-GEN in v0.96, as observed by Andrzej and Michel,
was precisely that it required one to spell out lists of symbols that
had already been declared (in contrast to the free extension
construct). 

One might object that when one in fact wants to specify the sort
generation in an extension, separately from the original declarations
of the sorts and functions concerned, my proposal would force one to
write out the complete declarations of the functions again, instead of
just their names.  If this case arises often enough to justify it, one
might provide an abbreviated form of FUN-DECL, used only when
re-declaring a (non-overloaded) FUN-NAME for use in a SORT-GEN.  Note
that in the case of overloaded functions, the FUN-SYMBs are
essentially FUN-DECLs already.

More later...

Peter