Towards a more flexible and accurate model for grammar levels and associativity

[herbelin]

Rendered: https://github.com/herbelin/ceps/blob/camlp5-associativity/text/camlp5-associativity.md

[silene]

So that it does not get lost, here is an LL(1) grammar I posted on Zulip that supports having multiple (non) associative operators at the same level, but causes a parsing error if the user tries to mix them in ambiguous way in a single expression, e.g., x opR y opL z. (L, N, R respectively stand for left-, non-, right-associative.)

term42:
  [ x = term41; y = term42_no_left -> y x
  | x = term41; y = term42_no_right -> y x
  | x = term41; "opN"; y = term41 -> OpN(x,y)
  | x = term41 -> x ]
term42_no_left:
  [ "opR";  x' = term41; y = term42_no_left -> fun x => OpR (x, y x') ]
term42_no_right:
  [ "opL";  x' = term41; y = term42_no_right -> fun x => y (opL  (x, x'))
  | "opL'"; x' = term41; y = term42_no_right -> fun x => y (opL' (x, x')) ]

[silene]

Parsing 2 ^ - x * y as 2 ^ (- (x * y)) seems to be quite surprising. I would expect the consensus among mathematicians to be (2 ^ (- x)) * y.

In other words, there is no reason for the argument of prefix "-" to be at level 40. It should be at the current level (i.e., 35 if the argument of infix "^". In fact, the notion of levels for a notation that starts with a terminal and ends with a non-terminal does not make sense in the first place. It should not have an intrinsic level, it should always use the ambient level.

[herbelin]

I got confused by the idea that - x * y was - (x * y) by default in mathematics, but that's the same as (- x) * y, so it does not have to be the former. And actually, most programming languages seem to make prefix - binding tightly (so morally at 10 for Coq).

For the example I mentioned, the level of x in - x do not matter. The whole notation could be at 10 with x at 10 too.

What do you mean by "It should not have an intrinsic level, it should always use the ambient level.". That is, in the following examples, how would you associate (or fail):

• x * - y
• x ^ - y
• x + - y
• f x - y
• - f * x
• - f ^ x
• - f + x
• - f x

Adding a link: https://en.wikipedia.org/wiki/Order_of_operations#Unary_minus_sign

[silene]

And actually, most programming languages seem to make prefix - binding tightly (so morally at 10 for Coq).

That does not mean that it is a good idea. In fact, the very first sentence of the Wikipedia page you cite says that - 3 ^ 2 is interpreted as -9 in mathematics. And the only "languages" it mentions as binding tightly are Excel, PlanMaker, and bc.

So, having unary minus at level 10 would be awful. And having it at level 35 is already painful. I hate having to write - (x * y). It should have been at level 45.

• x * - y
• x ^ - y
• x + - y

All three of them associate as x ! (- y).

• f x - y

Do you have an infix minus in the context? If not, then parsing can be recovered as f x (- y).

But the interesting case is actually f x - y z, which would be parsed as f x (- y) z (assuming again that there is no infix minus, otherwise the point is moot).

• - f * x
• - f ^ x
• - f + x
• - f x

You did not say what the ambient level is, so it depends. Let us assume that those expressions all look like y + - f ! x (so, ambient level is 50 left associative). Then they would respectively parse as

• y + (- (f * x))
• y + (- (f ^ x))
• (y + (- f)) + x
• y + (- (f x))

[herbelin]

(I'm tired, the first 3 questions were pointless. I meant the minus sign in the front)

I don't see what conclusion to draw otherwise. And we are somehow constrained by what is currently done, which is:

Require Import ZArith. Context (x y :Z) (f : Z -> Z) (g : Z). Set Printing Parentheses. Open Scope Z_scope.
Check  x * - f y. (* x * (- (f y)) *) (* due to recovery *)
Check  x ^ - f y. (* x ^ (- (f y)) *) (* due to recovery *)
Check  x + - f y. (* x + (- (f  y) *) (* due to recovery *)
Check  f x - y.   (* (f  x) - y *)
Check  - g * x.   (* (- g) * x *)
Check  - g ^ x.   (* - (g ^  x) *)
Check  - g + x.   (* (- g) ^  x *)
Check  - f x.     (* - (f x) *)
Check  - x * y.   (* (- x) * y *)
Check  - x ^ y.   (* - (x ^ y) *)
Check  - x + y.   (* (- x) + y *)

[herbelin]

For the record, experimenting changing associativity of:

• - x * y from (- x) * y to - (x * y) and
• - x / y from (- x) / y to - (x / y)

requires several changes in stdlib, starting with:

• Ring_theory.Ropp_mul_l : -(x * y) == -x * y (also in Ncring.v) and Ring_theory.ARopp_mul_l : -(x * y) == (-x) * y
• BinInt.Zopp_mult_distr_l : - (n * m) = - n * m
• Zdivfloor.div_opp_opp : b~=0 -> -a/-b == a/b
• Field_theory.rdiv5 : - (a / b) == - a / b
• Uint63.opp_spec : φ (- x) = - φ x mod wB
• -a÷b in Zquote.v
• - Qnum x * Zpos (Qden y) in QArith_base.v
• non exhaustive list...