[CoFI] Re: Revised concrete syntax for CASL basic specs

[pdmosses@brics.dk]

> Date: Mon, 6 Oct 1997 18:12:17 +0200 (MET DST)
 
> A revised proposal for the concrete syntax of basic specifications in
> CASL has been installed:
> 
>   http://www.brics.dk/Projects/CoFI/Documents/CASL/SyntaxIssues/
>   ftp://ftp.brics.dk/Projects/CoFI/Documents/CASL/SyntaxIssues/
> ...
>      Appendix A lists the remaining points to be resolved by discussion
>      on the CoFI Language Design mailing list, cofi-language@brics.dk.
> 
>      Deadline for comments: Monday 20 October 1997!

[No comments have yet been received.  But perhaps some are in the
pipeline?  --PDM]

In general, the following comments reflect my personal opinions and
prejudices, and should not be construed as a summary of a consensus!
However, most of the points are matters of minor detail, and do not
challenge the general look-and-feel of the current proposal.

Topics:
* SUBSORT-DEFN
* Display of "."
* Function attributes
* Predicate types
* Mixfix notation
* Precedence in terms
* SORT-GEN-ITEMS
* AXIOM-ITEMS
* IMPLICATION


>                        Concrete Syntax for CASL
>                           Basic Specifications
>                              6 October 1997


>  2 Input Syntax
>    SUBSORT-DEFN     ::=  SORT=VAR:SORT.FORMULA

This should have been:
     SUBSORT-DEFN     ::=  SORT={VAR:SORT.FORMULA}


> 3 Display Format, Symbols:

Also the input "." is to be displayed as a bullet, when possible.
HTML has no bullet: should the display there be a raised dot "·"
or the input "."?


> REMAINING ISSUES FOR DISCUSSION
> ...

> FUNCTION ATTRIBUTES:

Concerning the rather extreme proposal for attributes:
>    ATTRIBUTION      ::=  FUN-SYMB,...,FUN-SYMB:FUN-ATTRS
>    FUN-ATTRS        ::=  assoc  |  comm  |  idem  |  unit FUN-SYMB
>                       |  ac  |  aci  |  aciu FUN-SYMB  |  acu FUN-SYMB  
>                       |  ai  |  aiu FUN-SYMB  |  au FUN-SYMB
>                       |  ci  |  ciu FUN-SYMB  |  cu FUN-SYMB  |  iu FUN-SYMB

I find the abbreviations ac, aci, etc., far too cryptic.  They may be
familiar to those using term rewriting systems, but to the uninitiated
they would surely be just as puzzling as e.g. \P for powerset.

I would prefer the following syntax:
     ATTRIBUTION      ::=  FUN-SYMB,...,FUN-SYMB:FUN-ATTRS...
     FUN-ATTRS        ::=  assoc  |  comm  |  idem  |  unit FUN-SYMB
E.g.,
     __+__ , __*__ : assoc;
     (__+__:Nat*Nat->Nat) : assoc comm unit 0;


> PREDICATE TYPES:
>   A syntax such as `S*...*S->truth' was (briefly) discussed in Amsterdam;
>   would it be preferable to the `pred(S*...*S)' syntax? ...

I would indeed prefer `S*...*S->truth' (as you might have guessed :-).


> MIXFIX NOTATION:
>   How general should this be? ...

We may allow CASL parsers that reject some alternative ways of
inputting the same abstract syntax.  So we could allow full mixfix
notation (as in e.g. OBJ) in CASL but some parsers might insist on
ordinary functional application, thus requiring applications of 
`__ __' to be input as (__ __)(x,y).


> PRECEDENCE IN TERMS:

Concerning the proposed uniform relative precedence for infix, prefix,
and postfix operations: my own experience with this (in Action
Semantics) was that many grouping parentheses may indeed be needed -
but only when using large terms in a notation primarily based on infix
operations.  Does one in fact often write large terms in (e.g.)
arithmetic notation, when specifying software algebraically?  If so,
it would be good to see some practical examples!  If not, the current
proposal may indeed be adequate.


NEW ISSUES

>   SORT-GEN-ITEMS   ::=  generated SIG-DECL-ITEMS;...end

The keyword "end" may also be needed to indicate the end of a
specification definition in the full concrete syntax for structured
specifications.  It might look clumsy to have several adjacent "end"s.
If the notation for EXTENSION is light enough, one might simply omit
the "end" above, or even make the whole construct an alternative for
BASIC-SPEC (rather than BASIC-ITEMS), using EXTENSION to insert it
between other BASIC-SPECs.  I suggest to leave this issue open until
we've discussed the forthcoming proposal for structured
specifications.


>   AXIOM-ITEMS      ::=  AXIOM-S;ATOM;...;ATOM  |  AXIOM-S
>   AXIOM-S          ::=  axiom AXIOM  |  axioms AXIOM  |  .AXIOM  |  NON-ATOM
>   AXIOM            ::=  FORMULA
>   FORMULA          ::=  NON-ATOM  |  ATOM
>   NON-ATOM         ::=  QUANTIFICATION  |  CONJUNCTION  |  DISJUNCTION 
>                      |  IMPLICATION  |  EQUIVALENCE  |  NEGATION

The idea here was apparently twofold: to allow the use of a bullet
(input as a ".") to replace the keyword "axioms"; and to allow the
omission of both "axioms" and "." when the axiom cannot be confused
with a declaration.  However, CONJUNCTION, DISJUNCTION, IMPLICATION,
and EQUIVALENCE can all *start* with an ATOM, so perhaps it would be
better for parsers (human and machine) to require "axioms" or "."
before such axioms.  For uniformity, this should apply to negation as
well, leaving only QUANTIFICATION (as originally proposed by Bernd).
The corresponding concrete syntax could then be essentially:

    AXIOM-ITEMS      ::=  AXIOM-S AXIOM;...;AXIOM |
                       |  QUANTIFICATION;AXIOM;...;AXIOM  |  QUANTIFICATION
    AXIOM-S          ::=  axiom  |  axioms  |  .
    AXIOM            ::=  FORMULA
    FORMULA          ::=  QUANTIFICATION  |  CONJUNCTION  |  DISJUNCTION 
                       |  IMPLICATION  |  EQUIVALENCE  |  NEGATION  |  ATOM
                       |  (FORMULA)
(Some production-splitting may be used to avoid ambiguity, if needed.)


>   IMPLICATION      ::=  FORMULA=>FORMULA  |  FORMULA if FORMULA

I'd prefer 
    IMPLICATION      ::=  FORMULA=>FORMULA  |  FORMULA<=FORMULA
for uniformity.


That's all...

Peter