Re: Comments on CASL concrete syntax

[cerioli@disi.unige.it (Maura Cerioli)]

First of all a heartful thanks to the concrete syntax task group for the
great work (and the huge amount of time they have spent doing it).
[I'm not so sure you should thank us for taking so many months! --PDM]
I may be not fully agreeing with each single proposal, but in the complex I
find the compromise more than acceptable (and if I *would* find each point
perfect it wouldn't be much of a compromise for people with different
opinions, would it? ;-)

Just a few comments and doubts.

Basic Spec
----------
I don't understand why the constructs for declaring (defining) functions
and predicates have been grouped together and I strongly dislike this
solution.
Indeed, functions and predicates are different categories of symbols, with
different semantics and different methodological applications and I
personally find very misleading to have them confused in one syntactic bag.
Moreover, in the current proposal, for all the other categories of symbols
we have a "prefix" syntax (first we know the category, then the name of the
specific symbol comes, then the attributes...), while for predicates we
have a sort of "postfix": first (the imho misleading op keyword, then) the
predicate name and then the keyword pred, stating the nature of the symbol.

[See also the discussion in App. A, top of page 14. --PDM]

A second point of disagreement, though less strong, is the definition
of axioms.  I don't see the need for a special treatment of the
quantified axioms. Indeed, I would prefer to drop the last production of 
AXIOM-S and to have QUANTIFICATION::= QUANTIFIER VAR-DECL;...  .FORMULA 
(no alternative notation for conjunction). A close effect to the
current proposal from the end user point of view may be already
obtained (in the case of universal quantification that is the most
common) by a VAR-ITEMS followed by a list of (unquantified) axioms
(the difference is the lack of the bullet between formulae and the
keywords "axiom" and "var" instead of the quantifiers).  However, I
don't judge this a major issue, because it is something "extra" that
can be ignored, though I cannot imagine how to motivate to my users
the preference given to the quantified formulae.

[Also Bernd would argue (I suppose) for uniformity, allowing "." to be
used to introduce an unquantified axiom too.  But if "." can also be
used in function symbols such as "<__.__>" and "__..__", parsers would
have lookahead problems if "." could also separate axioms.  These
problems might disappear if axioms were always terminated by ";", or
if one used a different input syntax for what appears as a bullet when
formatted. --PDM]

Some minor points are
- the appearence of the arrow for partial functions is not suggestive,
  to me, of partiality, more of a latex error ;-). I would suggest a (stacked,
  in display format) P, or a broken arrow (this was, I think, the first
  suggestion by BKB), or the same arrow as for total function, but with a
  different keyword at the beginning (the last is my preferred)
  [The last presumably would not extend nicely to higher-order? --PDM]
- the keyword "defined" is too long and makes difficult to read the axioms.
  I would suggest to keep to the (standard?) D or Def
  [We are insisting on lowercase spelling for reserved words.  
  "d" could get confused with a variable in the presence of mixfix.
  "def" would be consistent with abbreviating other longer keywords,
  but perhaps suggests definition more than definedness? --PDM]
- the symbol for existential equality is not completely satisfactory
  Indeed, the dot tends to disappear when copying (and even in the original
  is not eye catching) [As suggested in App A, the symbol could be
  made bolder (use \boldmath). --PDM]
  and, moreover, it is not suggestive of existence.
  [It could be pronounced "dot equal", which is reasonably mnemonic
  for "defined and equal", perhaps? --PDM]
  I would prefer a solution involving an "e", if possible.
- Typo on page 5 (?)
  I think that the first production for AXIOM-ITEMS is
  AXIOM-S;AXIOM;... instead of AXIOM-S;ATOM;...
  (at least looking at the examples)
  [Right - Bernd pointed this out in his message earlier today. --PDM]
- Typo on page 2 of the examples in spec 1.3 (?)
  not defined  pre(zero)
  is not well formed, because pre expects a Pos argument
  It should be omitted or pre should be declared with profile
  Nat ->? Nat as well.
  [Right - or an explicit projection to Pos inserted. --PDM]

Structured Spec
---------------
I experimented less on this part, but I find the infix notation for
extension difficult to parse for human reader and (going in the opposite
direction from BKB last suggestion on the matter, sorry), I would prefer to
have a starting keyword like "use". I know that I can always prefix a
"use", regarding the specification to be extended as a unary union (at
least I hope that this is allowed), but this is, imho, quite tortuous.
However, I'm afraid that the preference to one or the other form strongly
depends on the expected form of the "standard" specification (depending in
turn on the methodology).
Indeed, I expect to use extensions as subterms in any kind of term and
hence I would prefer to "bracket" extensions, so to speak.
[You can always do that using "{...}". --PDM]
While I suppose (please correct me if I'm wrong) that some others expect to
have basically only many nested extensions and hence dislike the idea of
"standard" terms of the form
           use use use....then...then...then..
with a starting line of "use".
[Especially so since extension is associative, and the grouping above
irrelevant! --PDM]

Ciao
Maura

[Next time, we'll conscript you into the task of designing the
concrete syntax!  You can't imagine all the fun you missed... :-)
--PDM]