Re: [CoFI] CASL Concrete Syntax

[Till Mossakowski <till@informatik.uni-bremen.de>]

Here are my comments to the new version.

[A couple more messages will be forwarded shortly.  N.B. TODAY is the
 FINAL DEADLINE for comments before the concrete syntax for basic and
 structured specifications is FROZEN.  The concrete syntax for
 architectural specifications and views is however still tentative,
 pending the appearance of the promised examples...  --PDM]

I refer to page 14, Remaining issues for discussion:

Precedence in terms and mixfix notation:

The offside rule does allow not only the omission of grouping parentheses,
but also the omission of separating semicolons between items.
This is quite imporant, since it helps to save writing
(I have written some larger functional programs using the offside rule,
 and I much more appreciated the saving of semicolons than that
 of parentheses).

Concerning the degree of mixfix notation:
I think it is useful to have user-defined mixfix syntax,
with disambiguation done at the parsing level using precedences
(but not using typing information).
Parsers have to make some two-pass processing, first collecting
the mixfix declarations, adding them to the grammar, and then
parsing the specification.
[In fact it may be only the atomic formulae that need (re)parsing in
 the second pass. --PDM]
So it would add no complexity to have user-defined precedence
rules as well.
[That may depend on the implementation technique being used.  --PDM]

I would vote 

[Just in case someone might get the wrong impression: we are not
 currently "voting" on the various issues, merely gathering opinions.
 However, after the deadline expires TONIGHT, decisions will have to
 be taken, and only "voiced" opinions will be taken account of... 
--PDM]

against the inclusion of anonymous mixfix operators
into first-order CASL, because I would like to reserve it for
application in higher-order CASL. I.e. you can write

	f a b c

instead of

        f(a)(b)(c)

in higher-order CASL. Now if the (binary) anonymous mixfix
operator is present in first-order CASL, then a first-order
specification using it cannot be taken literally to be
a higher-order specification, because the anonymous operator
now is overloaded (some first-order operation AND higher-order
application) which leads to ambiguities. (The only way out
would be to use typing information for disambiguation.
which I do not like.)

[There seems to be agreement that disambiguation of grouping should be
 independent of typing.  However, another way out might be to rename
 `__ __' to some non-anonymous symbol such as `__++__' whenever
 referencing the specification from a higher-order specification.
 Doesn't this solve the problem?  Presumably those writing higher-order
 CASL specifications don't themselves want to write/parse first-order
 specifications that involve `__ __', merely to refer to them.  --PDM]

Optional terminators:

"... there is a choice between always and never terminating such lists
with semicolons."
In case that we have to choose between "always" and "never" I strongly vote
for always.  
The central point is uniformity (note that also the offside
rule allowing to omit semicolons altogether has such a uniformity).
I have typed in a number of specifications in CASL and fed them into
our parser requiring "never" at that time. I produced a lot of syntax
errors because of this "never". It is tedious to always have to think
about the position of the current line you are writing: is it before
a keyword starting a new section of basic item, or is it in the
middle of such a section? This becomes even worse when moving lines
to a different section (of the same kind): you have to add (or delete)
the semicolon, if the line was at the end and now is in the middle
(or the other way round).


Some minor points.

page 4: OP-SYMB in OP-ATTR has to be changed to TERM to get agreement
with abstract syntax.

page 5:
I do not understand the syntax of TERMs and MIXED-TERMs.
It seems that much more than wanted is allowed by the grammar.

[Moreover, it is desirable to reinstate the usual productions for
 function and predicate application---and insist that they have higher
 precedence that the sequence of MIXED-TERMs, so that when a
 specification makes no use at all of mixfix applications, the
 recognized grouping of terms and atomic formulae is correct straight
 away.  This should facilitate obtaining the concrete syntax of
 sublanguages that do not allow mixfix notation.  I'll send the details
 in a separate message, later today.  --PDM]

page 7:
ID in ARCH-SPEC-NAME etc. has to be changed to SIMPLE-ID, I think.

page 7, conjunction and disjunction:
Isn't it common to give conjunction a higher precedence than disjunction?
[Among logicians, certainly.  But some of us have argued that software
 engineers do not have such a strong tradition for this. --PDM]

page 7, implication:
It is quite standard that implication associates to the right,
i.e. A => B => C is parsed as A => (B => C)
(see eg. Shoenfield, Mathematical logic, 1967).
[Ditto.  --PDM]

page 8, precedence of mixfix:
Is there a precedence for TOKEN __ ... __ TOKEN?
[What would you suggest?  --PDM]

page 9, 2nd last item:
I think =e= also has to be forbidden as a TOKEN.
[It was never allowed, since it mixes characters from WORDS and
 SIGNS.  --PDM]

page 10:
defined ==> def

page 12: 
I do not understand 6.2.1. The syntax of IDs is different.
[Sorry, the grammar has changed but not the text: the proposal is
 simply to allow `%[ID,...,ID]' as a label annotation.  Moreover, as
 pointed out by Christine Choppy, BASIC-ITEM no longer is used, and
 should now be read as "a component of a BASIC-ITEMS".  --PDM]

Greetings,
Till