[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[CoFI] Re: Revised concrete syntax for CASL basic specs
Below are my comments on some Remaining Issues, marked by [BKB] in PDMs
comments below, to get the context.
pdmosses@brics.dk wrote:
>
> > Date: Mon, 6 Oct 1997 18:12:17 +0200 (MET DST)
...
>
> 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
>
...
>
> > 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 "."?
[BKB] I would prefer the raised dot, but no strong feeling.
BTW: should tools accept the html ISO characters as alternative input?
[This question applies to ¬ (logical negation) and · (raised dot). --PDM]
> ---------------------------
> > 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;
[BKB] The compact syntax with just one item has the definite advantage,
that each can be interpreted as a kind of parametrised type (or type
class a la Haskell or Spectrum). I do not like the long list of special
abbreviations either and have previously proposed to cut down to those
most likely to be needed; note that one can always have more than one
such attribute declaration, if necessary. I also would prefer more
suggestive and longer names, such as "monoid"; anyway, monoid instead of
"au", i.e. with left and right neutral element. Any other better names ?
or e.g. assoccomm (one word)? Thus my proposal is:
ATTRIBUTION ::= FUN-SYMB,...,FUN-SYMB:FUN-ATTRS
FUN-ATTRS ::= assoc | comm | idem | unit FUN-SYMB
| ac | aci | aciu FUN-SYMB | acu FUN-SYMB
| monoid FUN-SYMB
Are any other combination really needed? Please give convincing
examples!
> ---------------------------
> > 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 :-).
[BKB] so would I! The reason is easier extendability to Higher-Order.
Note that we are not introducing another kind of function here, but
"->truth" as a special notation for predicates.
> ---------------------------
> > 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).
[BKB] I object to (even overlodadable) anonymous operators, on the
grounds of problems with tools and HO application, but also of
readability of specs (I heard, and may be wrong, that this is something
many users of OBJ have problems with)
The issue of generality of mixfix notation is still open until we have
more experience with implementing tools (and I do not mean just one).
> ---------------------------
> > 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.
[BKB] As you all konw, I feel very strongly about having the usual
mathematical precedences for arithmetic; a separate issue is extension
to derived operator symbols (e.g. ++, ** inheriting those). A language
about algebra (in many ways) should not step backwards here!
I find it even worse and very error prone, that expressions are now
allowable (always grouping to the left!) that are WRONG in arithmetic,
e.g. a+b*c, where parentheses are recommended, but not required.
[One could adapt Peter's proposal by removing the rule that infixes
group to the left, so that the user would have to write a+(b*c) or
(a+b)*c. But then to avoid having to write also a+(b+c) or (a+b)+c,
the "assoc" attribute should presumably affect parsing! --PDM]
My previous proposal: very few (less than 5) predefined levels of
precedence (e.g. for *, + and ^ [exponentiation, binding to the
right!]), and inheritance to operators having these as first character,
e.g. ++, **.
> ---------------------------
> NEW ISSUES
>
...
>
> > 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.)
[BKB] I agree with Peter (anyway, this was my original proposal, more or
less ...)
...
>
> That's all...
>
> Peter
More comments on Remaining Issues later.
[Later today, I hope you mean! --PDM]
Bernd