Disambiguation of formulae

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

Dear friends,

Markus Roggenbach at Bremen has used the following lines within
some CASL specification:

     sort
           Irred= { x: Elem . not x in U /\
                              forall y, z: Elem . x = y * z => (y in U
                              \/ z in U) }

Now both the Paris and the Bremen parser reject this line
and require the quantification to be brackted (I would like
also to know what the Amsterdam parser says, but the web
interface does not respond at the moment).

I am not entirely sure if this bevahiour is in accordance with
page C-7 of the CASL summary. I see two different interpretations
of page C-7:
1. Quantifications have a lower precedence than conjunctions,
   hence, any quantification ocurring in a conjunction must
   be brackted. (In fact, this kind of reasoning is supported
   by the way the precedence rules are implemented in a grammar,
   but it does not directly follow from the description
   in the text on pace C-7.)
   This would support the bevaviour of the parsers.
2. The FORMULA in a quantification extends as far to the right
   as possible, and using this principle, there is only one
   possibility to parse the above line.
   The parsers do not support this view, and I do not know
   how to rearrange the grammar to implement such a view.
   
Anyway, the summary should perhaps be a bit more explicit
here.

Greetings,
Till

P.S.

Markus came up with the following line

    vars
          x: Elem; u,v: RUnit; i,j: Irred; S,T :FinSet[Irred]
          %% product of a finite set of irreducible elements:

          %% equivalence of irreducible elements:
          . equiv(i,j) <=> exists u: RUnit . i= u * j

Here, as he says, it is not very asthetic to require to bracket
the formula as         

          . equiv(i,j) <=> (exists u: RUnit . i= u * j)
          
- but this is currently required by the parsers (and by the first
interpretation of page C-7, but not by the second one).

Greetings,
Till


=====================================================================

From: Frederic Voisin <Frederic.Voisin@lri.fr>


The Concrete syntax document says that the quantification has the lowest
precedence, hence no extra bracket should be needed. If Christophe's
parser requests some extra parentheses, it is a bug...

Frederic