On Wed, Nov 6, 2019 at 3:33 PM Giovanni Mascellani <[email protected]>
wrote:
> Hi everybody (especially Mario, given the subject!),
>
> I am working on another MM0 implementation, and I have a few doubts
> about the secondary parser (parsing in general is not my strong point).
> It is said that, in order to have uniqueness, an infixy constant should
> have a unique precedence. Does this mean that it is unique among the
> infixy constants' precedences, or among all the precedences?
>
Neither; it means that any time a particular infixy constant appears, it
must have the same precedence. That is, if you have a notation x $e.$ A and
another notation ${$ x $e.$ A $|$ ph $}$, then $e.$ must be given the same
precedence in both appearances.
set.mm0 suggests the former, because both $es.$ (infixl) and $~$ (not
> infixy) have precedence 40. However, it seems to me that this is enough
> to lose uniqueness of parsing tree: for example, $~ x es. y$ can be
> parsed both as $~ (x es. y)$ and as $(~ x) es. y$, according to the
> grammar in mm0.md. The latter had wrong types, but I believe this is not
> something the parser should care about (or should it?).
>
You are right, this is a problem. I think the issue is that precedences are
*not* required to be unique in the sense that you had guessed. Here is
another variation on that: suppose A -> B is infixr 1 and A <- B is infixl
1 (so the generated rules say ((A:2) -> (B:1) : 1) and ((A:1) <- (B:2) :
1)); then
A -> B <- C
has two parses (because A -> B has prec 1 which fits as the left argument
of _ <- C, and B <- C also has prec 1 so it fits as the right argument in A
-> _).
I think the solution is to enforce, as you will see in precedence tables
for languages like C, that "associativity" is uniquely assigned to
precedence levels, not operators. This example would be rejected because
precedence level 1 has both a right associative and a left associative
operator. Prefix operators should be treated as right-associative for this
purpose, because something like (~ (A:1) : 1) has a subterm that is
trailing (on the right) with the same precedence as itself, like a right
assoc operator would.
The algorithm is to keep a mapping from precedence levels to their
associativities (or nothing). Every time a left assoc operator is found,
the precedence is marked left assoc, and similarly for right assoc; prefix
operators mark their precedence as right assoc, and a general notation
marks the precedence of the leading constant as right assoc if it ends with
a variable (otherwise it has no effect on the precedence table). An attempt
to assign a precedence as both left and right assoc is an error.
Mario
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSvUTVseYYMCWe8rNSmAxmQND8ErjV94CuTfBgpLVEv-NQ%40mail.gmail.com.
