Uniqueness of MM0 secondary parsing

[Giovanni Mascellani]

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?

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?).

Thanks for explaining!

Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[Mario Carneiro]

On Wed, Nov 6, 2019 at 3:33 PM Giovanni Mascellani <g.masc...@gmail.com> 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

[Giovanni Mascellani]

Hi,

Il 07/11/19 03:18, Mario Carneiro ha scritto:

> 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.

Ok, so the reason for this is that when you found a constant while
parsing at a certain minimum precedence level, you immediately know if
you have to branch out or not, without having to know if the surrounding
constructor is an infix or a notation? Or is there something deeper?

> 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.

I agree. In a C parsers I wrote some time ago I would treat prefix
operators as infix operators with an empty left argument (and the
opposite thing for suffix operators, since in C we have those as well).

[Mario Carneiro]

On Thu, Nov 7, 2019 at 2:44 AM Giovanni Mascellani <g.masc...@gmail.com> wrote:

Hi,

Il 07/11/19 03:18, Mario Carneiro ha scritto:
> 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.

Ok, so the reason for this is that when you found a constant while
parsing at a certain minimum precedence level, you immediately know if
you have to branch out or not, without having to know if the surrounding
constructor is an infix or a notation? Or is there something deeper?

You can't actually tell during parsing (without backtracking) if you have actually found the notation constant or the infix constant when you see this; that is, if you have { x e. A | ph } it might actually be { (x e. A) | ph } and you won't notice that this doesn't parse until you get to the "|". (And besides the fact that they are slower, we don't want to backtrack because then we lose all claim of unambiguity.) The typing prevents this in the case of { x e. A | ph } (since x can only be a single token) but that's not available during parsing.

The trick that is used to prevent this is to force the user to put precedences on *constants* (and check consistency of a given constant across all its uses), but then use precedences on *variables* for the actual parsing process. That is, you write

(${$:max) x ($e.$:20) A ($|$:25) ph ($}$:0)

but the parser actually uses

 

(${$ (x:21) $e.$ (A:26) $|$ (ph:1) $}$ : max)

where the numbers indicate the precedence level associated to the CFG nonterminal. Notice that the precedences are increased by 1 (I think you could also do this with a special n+epsilon precedence); this is to ensure that when parsing (x:21), the operator "infixl $e.$ prec 20", which contributes the CFG rule ((x:20) $e.$ (A:21) : 20), is not applicable at the location of the x in the set abstraction, so { (x e. A) e. A | ph } will never be considered a valid parse.

Mario

[Benoit]

What do the colons and digits mean in " ((A:2) -> (B:1) : 1) " ?

To have unambiguity, wouldn't it be easier, as Giovanni thought was the case, that any natural number be the precedence of at most one operator (even if this is more than needed for unambiguity) ?

How do you parse " a * b + c " if both laws have the same precedence ?

Thanks,
Benoît

[Mario Carneiro]

On Thu, Nov 7, 2019 at 6:49 AM Benoit <benoit...@gmail.com> wrote:

What do the colons and digits mean in " ((A:2) -> (B:1) : 1) " ?

They are annotating the precedence levels of subterms. It's basically a shorthand for the CFG rule

expr(1) <- expr(2) "->" expr(1)

where "expr(1)" is the nonterminal corresponding to expressions with precedence >= 1.

 

To have unambiguity, wouldn't it be easier, as Giovanni thought was the case, that any natural number be the precedence of at most one operator (even if this is more than needed for unambiguity) ?

That's a bit restrictive. For one thing, there are only 2048 precedence levels (or at least, no more than that many are required to exist), so you won't be able to have more than 2048 notations, and there are almost certainly going to be more than that many definitions. Besides this, it is not uncommon for multiple operators to "officially" live on the same precedence level. For example, + and - are generally at the same left assoc precedence level, so that a + b - c means (a + b) - c and a - b + c means (a - b) + c. If they live at different precedence levels this parse is not possible.

In C/C++, most precedence levels have several operators in them: https://en.cppreference.com/w/c/language/operator_precedence

How do you parse " a * b + c " if both laws have the same precedence ?

It is also generally agreed that * has higher precedence than + , so a * b + c means (a * b) + c and a + b * c means a + (b * c).

When faced with two operators with the same precedence (including in particular two instances of the same operator), the associativity of the operator determines the bracketing. If it is left associative, then a o b o c o d means ((a o b) o c) o d, and if it is right associative it means a o (b o (c o d)).

Mario

[Benoit]

What do the colons and digits mean in " ((A:2) -> (B:1) : 1) " ?

They are annotating the precedence levels of subterms. It's basically a shorthand for the CFG rule

expr(1) <- expr(2) "->" expr(1)

where "expr(1)" is the nonterminal corresponding to expressions with precedence >= 1.

There is something I do not understand: to me, it is operations which have a precedence, not expressions.  Or is there a rule to attribute a precedence to an expression in terms of the precedence of its root operation?

How do you parse " a * b + c " if both laws have the same precedence ?

It is also generally agreed that * has higher precedence than + , so a * b + c means (a * b) + c and a + b * c means a + (b * c).

Take two laws, * and +, which have the same precedence. Then, how do you decide how to parse "a * b + c"?  Here, left- or right-associativity is irrelevant since each law is used only once.

Or maybe we have different definitions of left/rigth-associativity?  To me, saying that * is left-associative means that "a * b * c" is to be read as "( a * b ) * c", and nothing more than that.  It seems that to you, there is an additional meaning: if * and + have the same precedence and are both left-associative, then " a * b + c " is to be read as " ( a * b ) + c".  It seems a bit abusive compared to the original meaning of the word "associative".  Is this general practice in the field of computer science?

Thanks,
Benoit

[Giovanni Mascellani]

Hi,

Il 07/11/19 14:51, Benoit ha scritto:

> There is something I do not understand: to me, it is operations which
> have a precedence, not expressions.  Or is there a rule to attribute a
> precedence to an expression in terms of the precedence of its root
> operation?

Yes, I'd say expressions have the precedence of their root symbol. See
also the explicit grammar written by Mario in MM0 docs:

https://github.com/digama0/mm0/blob/master/mm0.md#secondary-parsing

> Take two laws, * and +, which have the same precedence. Then, how do you
> decide how to parse "a * b + c"?  Here, left- or right-associativity is
> irrelevant since each law is used only once.

I'd say that's the point Mario is making: associativity has to be given
to the precedence level, not to the individual operators. So if you want
* and + to be at the same precedence level, they also have to have the
same associativity. If they are both left-associating, then your
expression will be parsed as (a * b) + c, if they are both
right-associating it will a * (b + c). From the point of associativity,
you assume all the operators at the same precedence level to associate
together.

Also, as Mario noted, infix operator should be treated as
right-associating, and conversely postfix operator should be treated as
left-associating (but, fortunately, MM0 does not allow them).

HTH, Giovanni.

[Benoit]

Thanks.  Indeed, with this extended definition of left/right-associativity (that is, associativity among all operators of a given precedence, and not merely associativity of a given operator), it all makes sense and is consistent, and indeed the condition given by Mario to ensure unambiguity (that is, a given precedence can be given to several left-assoc operators or several right-assoc operators, but not both) is the correct one.

But I still have a question: is this common practice in computer science?  It is certainly not in mathematics.  It is actually a bit strange from a mathematical-practice point of view.  For instance, if I want to define an R-module M where * is the field multiplication and . is the scalar multiplication (so for instance, if a, b \in R and s \in M, I have (a * b) . s = a . ( b . s ) \in M), I would have to type, e.g.:
  infix * rassoc precedence=1; (or "lassoc")
  infix . rassoc precedence=2;
and then one of the axioms for an algebra would read "a . b . s = a * b . s".  By the way: it is necessary to have different precedences, in this example.  Is this correct?
But it seems strange to specify that an operator of signature "scalar x vector -> vector" is either left- or right-associative.  Since vector is not a subtype of scalar, I should not have to specify that, and "a . b . s" can only be read as "a . ( b . s )".  If I had typed "infix . lassoc precedence=2;" above, would this have triggered an error?  (Another example is inner products, since "scalar" is not a subtype of "vector".)  Or would this require a too complex parser?

In the example above, I would much rather have to type, e.g.:
  infix * rassoc precedence=1;
  infix . precedence=2;
and that if I had added "rassoc" or "lassoc" in the second line, this would have triggered an error.

Benoît

[Giovanni Mascellani]

Hi,

Il 07/11/19 19:32, Benoit ha scritto:

> But it seems strange to specify that an operator of signature "scalar x
> vector -> vector" is either left- or right-associative.  Since vector is
> not a subtype of scalar, I should not have to specify that, and "a . b .
> s" can only be read as "a . ( b . s )".  If I had typed "infix . lassoc
> precedence=2;" above, would this have triggered an error?  (Another
> example is inner products, since "scalar" is not a subtype of
> "vector".)  Or would this require a too complex parser?

I think that in general it is assumed that parsing is done before type
checking, so you cannot use type information to choose between different
parses. If you decide to mix the two phases everything becomes much more
complex, which is probably not a good idea in MM0.

In C and C++, instead, this happens: in the line

a * b;

you cannot say whether * is a multiplication or a pointer declaration
unless you know if a is a type or a variable. This notoriously requires
C and C++ parser to be quite complex. In C++, in some circumstances, you
have to explicitly specify that a name is a type with the keyword
"typename" when the parser is not able to infer it (typically when
dealing with templates and names depending on a template, because it is
not possible to know whether a name depending on a template is a
variable or a type until the template is instantiated; but this happens
after parsing, and it might happens none or many times, so the parser
cannot rely on it, and the programmer has to be explicit).

In you example, you definitely want "." to be right associative, so that
a . b . s = a . (b . s) as you say. You also want * to be higher
precedence, because you probably want a * b . s = (a * b) . s. As for
the associativity of *, it is probably not very important, because * is
a field product, therefore associative. I'd say that in this case the
more predictable thing is to make it left associative. So, in the end, I
would declare

infixr . prec = 1
infixl * prec = 2

As I said, I don't think that relying on types would be a good idea,
unless you really like complicating your life with parsers (I don't: the
only programming language I have designed so far, called "G", uses RPN
to avoid parsing expressions, and in some sense this is one of its
selling points), or if you have strong reasons for doing it because you
want to support some other strange construct.

[Benoit]

Thanks Giovanni.  I hope Mario can also chime in on the questions in my previous message, since these are not right-or-wrong issues, but are more about balancing pros (proximity with mathematical practice) and cons (more complex parser).

You write:

In you example, you definitely want "." to be right associative, so that
a . b . s = a . (b . s) as you say.

Not only do I want it, but it is the only possible parse, for type reasons.  Would it have triggered an error to type " infix . lassoc prec=1 " ? Or would it trigger an error only when I write "a . b . s" without parentheses ?  (In any case, this would be unfortunate.)
 

You also want * to be higher
precedence, because you probably want a * b . s = (a * b) . s.

Idem: it is the only possible parse for type reasons.  Would it have triggered an error to give higher precedence to the scalar multiplication ?  Or would it trigger an error only if I write "a * b . s" without parentheses ?  Here, I would be ok to have to always type "(a * b) . s" and to be forbidden to type "a * b . s".  In other words, is it possible to define operation associativities and precedences which require parentheses to avoid ambiguity, without triggering errors at operation definitions ?  Allowing this might indeed require a too complex parser, and this is probably not MM0's job (which should probably allow minimal syntactic sugar as long as this does not complexify things too much).

Side remark: I agree with the treatment of prefixed operators, which looks like the most sensible one.  Is there a reason why suffixed operators are not allowed in MM0 ?  This sounds unfortunate since they are often used in math (inverse, transpose, conjugate...).

Another remark: if one retains, for simplicity of the parser (and neglecting proximity with mathematical practice), that a given precedence is associated with either left- or right-associative operations, one could even impose from the beginning that even precedence implies right-associativity and odd precedence implies left-associativity, hence doing away with the keywords "lassoc" and "rassoc".

Benoît

[Mario Carneiro]

On Fri, Nov 8, 2019 at 4:37 AM Benoit <benoit...@gmail.com> wrote:

Thanks Giovanni.  I hope Mario can also chime in on the questions in my previous message, since these are not right-or-wrong issues, but are more about balancing pros (proximity with mathematical practice) and cons (more complex parser).

I basically agree with Giovanni's answer, but I will give my own with attention to the points in your latest message.

On Thu, Nov 7, 2019 at 1:32 PM Benoit <benoit...@gmail.com> wrote:

But I still have a question: is this common practice in computer science?  It is certainly not in mathematics.  It is actually a bit strange from a mathematical-practice point of view.  For instance, if I want to define an R-module M where * is the field multiplication and . is the scalar multiplication (so for instance, if a, b \in R and s \in M, I have (a * b) . s = a . ( b . s ) \in M), I would have to type, e.g.:
  infix * rassoc precedence=1; (or "lassoc")
  infix . rassoc precedence=2;
and then one of the axioms for an algebra would read "a . b . s = a * b . s".  By the way: it is necessary to have different precedences, in this example.  Is this correct?

I have a few reactions to this example. First, it is pushing a bit too heavily on the parser. Regardless of whether the parser can take it, this is near the limit of what I would consider "good practice" regarding appropriate use of notations and associativity for parenthesis-reduction.

 

As you say, the only way to get the parses you want are for "." to be right assoc, and "*" to be left or right assoc with a higher precedence. Anything else would cause the parser to produce the wrong parse, leading to a type error. (Just put parentheses!)

But it seems strange to specify that an operator of signature "scalar x vector -> vector" is either left- or right-associative.  Since vector is not a subtype of scalar, I should not have to specify that, and "a . b . s" can only be read as "a . ( b . s )".  If I had typed "infix . lassoc precedence=2;" above, would this have triggered an error?  (Another example is inner products, since "scalar" is not a subtype of "vector".)  Or would this require a too complex parser?

Yes, you have to specify it is right associative, and if you don't then you will have to put in lots of parentheses to make type correct statements.

It may seem strange that you have to redundantly specify this information, but it's not really redundant. How can MM0 know that scalar is not a subtype of vector? It may not be right now, but perhaps later you decide to add a coercion and then it becomes ambiguous.

But the more important part comes back to why MM0 has a parser in the first place. From its inception, the parser was supposed to be some reasonable algorithm that guarantees that the underlying CFG is unambiguous. The MM0 parser specification is not deterministic, it is based on a CFG, so the constraints are necessary to ensure that any reasonable parsing algorithm will find the correct parse. The shunting-yard algorithm or what have you does *not* define the grammar, it is merely the implementation. This is why issues such as Giovanni brought up in the first post are actual problems for the functional correctness proof.

The problem with using type information for parsing is that the user could just as easily have written ". : vector x vector -> vector" with everything else the same, and now the grammar is ambiguous. So the static checks must somehow exclude this case. Moreover, if you exclude bad parses by type information you can have some much more complicated edge cases. Suppose "@" and "%" have ambiguous fixity, but have the types

@ : A x B -> C

% : C x D -> B

Then (a @ x % d) can either be parsed as ((a @ x) % d), where x: B and the expression has type B, or (a @ (x % d)) where x: C and the expression also has type C. If I throw in

^ : B x E -> B

then (a @ x % d ^ e) has two valid parses: (((a @ x) % d) ^ e) (of type B, assuming x: B) or (a @ ((x % d) ^ e)) (of type C, assuming x: C).

These examples seem very sketchy to me. It is conceivable that there is an algorithm that decide whether some set of operators (given their types and the coercion graph) is unambiguous or not, but I can not believe that it is at all a simple algorithm. It seems like you would have exponentially many paths to try because of all the local ambiguities.

Finally, I want to point out that your example is slightly unrealistic. The MM0 type system is (somewhat deliberately) impoverished, and it would be very unlikely for you to actually have types "scalar" and "vector" unless you are in a (very limited) kind of first order proof environment for modules. You wouldn't be able to do much interesting vector space theory there, because you have no higher order constructs. Much more likely, you are working in a ZFC style foundation where everything has the same type "set", and then type information is next to useless for this kind of thing.

In the example above, I would much rather have to type, e.g.:
  infix * rassoc precedence=1;
  infix . precedence=2;
and that if I had added "rassoc" or "lassoc" in the second line, this would have triggered an error.

I will add that I fell into this (cognitive) trap myself, and Giovanni caught me on it. I said to myself "It doesn't make any sense for "e." to be right or left associative, because it has type set x set -> wff, so it can't associate with itself anyway, so I'll just make it left assoc". But this is not true, because "~" lives at the same precedence, and if "e." is left assoc then there is a conflict, while if "e." was right assoc then there would be no conflict. Because *types don't matter during parsing* (at least, with the MM0 parser algorithm as it currently exists). I've written a simple C compiler before, and the "A * b;" example of type-disambiguation between a multiplication statement and a pointer declaration is a real thing (and a real pain). I don't want to replicate that.

 

You write:

In you example, you definitely want "." to be right associative, so that
a . b . s = a . (b . s) as you say.

Not only do I want it, but it is the only possible parse, for type reasons.  Would it have triggered an error to type " infix . lassoc prec=1 " ? Or would it trigger an error only when I write "a . b . s" without parentheses ?  (In any case, this would be unfortunate.)

It would not be an error to type "infixl smul: $.$ prec 1;". It would be perfectly valid, but probably less convenient than you would like because you would have to add lots of parentheses to write things like "a . (b . s)". You could try to write "a . b . s" but it would be interpreted as "(a . b) . s" and reported as a type error.

 

You also want * to be higher
precedence, because you probably want a * b . s = (a * b) . s.

Idem: it is the only possible parse for type reasons.  Would it have triggered an error to give higher precedence to the scalar multiplication ?  Or would it trigger an error only if I write "a * b . s" without parentheses ?  Here, I would be ok to have to always type "(a * b) . s" and to be forbidden to type "a * b . s".  In other words, is it possible to define operation associativities and precedences which require parentheses to avoid ambiguity, without triggering errors at operation definitions ?  Allowing this might indeed require a too complex parser, and this is probably not MM0's job (which should probably allow minimal syntactic sugar as long as this does not complexify things too much).

If you are okay with always writing "(a * b) . s", then * can have whatever precedence you want (unless you make * and . have the same precedence and opposite associativity).

 

Side remark: I agree with the treatment of prefixed operators, which looks like the most sensible one.  Is there a reason why suffixed operators are not allowed in MM0 ?  This sounds unfortunate since they are often used in math (inverse, transpose, conjugate...).

I was actually thinking about changing this, and this thread in particular has clarified matters for me regarding the CFG static analysis enough that I think it could be done without complicating the algorithm.

This came up for me with "mixfix" operators. With MM0 currently, you can define "a + b", but you can't write "a +g[ G ] b" representing a general group addition, because the +g notation does not begin with a constant. But it can be analyzed essentially like any other infix notation: it is marked either left or right assoc, and the inner variables are treated like they would be in a general notation.

This could be declared using general notation as:

notation gmul (a G b: set): set = a ($+g[$:50) G ($]$:0) b : lassoc 50;

 

(The main thing I don't like about this proposal is that it adds new keywords like "lassoc" and such since "notation" is a little limited in the way it describes the precedence of the first and last variables.) This turns into the rule

((a:50) +g[ (G:1) ] (b:51) : 50)

where the first variable stays at prec 50 because it is lassoc. For a rassoc notation it would be

((a:51) +g[ (G:1) ] (b:50) : 50)

instead. Like other general notations, the first constant is required to be unique, but in this case that means the thing after the variable. Two variables are not allowed at the start, i.e. a notation "a b + c" is not okay, although "a + G b" is, where G gets parsed with max precedence (meaning that it will either be atomic or in parentheses).

With a notation system that can support an initial variable like this, it is not difficult to leave off the trailing variable, resulting in a postfix notation such as

((a:50) ! : 50)

which is left assoc. (You could also have a right assoc postfix notation, but you would never want to, because you could not nest it with itself, i.e. you have to write "(a !) !" instead of "a ! !".) Since it follows the same rules regarding uniqueness of associativity per precedence level, this doesn't introduce any new ambiguities, and the same precedence parser algorithm can handle general notations in infix position without backtracking because of the unique constant requirement.

Another remark: if one retains, for simplicity of the parser (and neglecting proximity with mathematical practice), that a given precedence is associated with either left- or right-associative operations, one could even impose from the beginning that even precedence implies right-associativity and odd precedence implies left-associativity, hence doing away with the keywords "lassoc" and "rassoc".

I suppose that's true, but it's not obvious. MM0 is designed to be read, and having mystery rules like that seems like a good way to scare people off. The precedence system is supposed to be minimal and expressive, but not surprising, and I can already see the angry github issues asking why changing a precedence from 42 to 43 with nothing else nearby breaks their code. (MM0 actually doesn't have keywords "lassoc" and "rassoc" btw, although the proposal above would add them. It uses "infixl" and "infixr" instead.)

Regarding the barb about neglecting mathematical practice, I still don't see your argument. Your example with modules fits perfectly well within the MM0 precedence system. Yes you have to write those precedences down, and if you get it wrong then things don't typecheck, but that doesn't mean that "." isn't right associative in the example. It's *obviously* right associative because the other option doesn't typecheck, but you seem to be taking from this fact that it's not associative at all, which isn't true; a non-associative operator (which MM0 doesn't support) would *always* require parentheses.

There are plenty of other issues you could raise with the MM0 notation system regarding the neglect of mathematical practice, in particular the massive overloading of operators and implicit parameters. MM0 takes a similar stance to metamath here, so it's probably not to surprising to the folks on this forum, but I've gotten comments on it elsewhere and I can only point to the added disambiguation complexity and lack of clarity that comes with those systems.

Mario

[Giovanni Mascellani]

Il 08/11/19 12:32, Mario Carneiro ha scritto:> This came up for me with

"mixfix" operators. With MM0 currently, you can
> define "a + b", but you can't write "a +g[ G ] b" representing a general
> group addition, because the +g notation does not begin with a constant.
> But it can be analyzed essentially like any other infix notation: it is
> marked either left or right assoc, and the inner variables are treated
> like they would be in a general notation.

That seems to be a good idea to me: the difficulty of infix operators is
that you have to allow to begin parsing the first variable of a
production without yet knowing that the production is (and therefore
what is its precedence). But once you find the first constant (suppose
to be discriminating) you know which production is, and you just have to
call recursively the parser for each of the other constants. So
supporting a postfix operator or a more general "mixfix" operator
shouldn't add a big marginal work, while it would unlock a few notations
that it is nice to have in mathematics.

Basically this is also how the ternary operator in C works, at the level
of parsing.

[Benoit]

Thanks for the clear explanations.  I didn't know this use of the word "barb", and I see on dictionary.com "unpleasant remark".  My remarks were certainly not meant to be unpleasant, and I'm interested in seeing where MM0 goes.

Is it always possible to put parentheses, even where they are not needed? I mean: is there a rule saying that if A is an expression of some type, then ( A ) is also an expression of the same type, so that I can write e.g. "( a * b ) + c" even when "a * b + c" is valid?

A few comments as replies below.

It may seem strange that you have to redundantly specify this information, but it's not really redundant. How can MM0 know that scalar is not a subtype of vector? It may not be right now, but perhaps later you decide to add a coercion and then it becomes ambiguous.

Do you mean: changing one's mind at a later time, or putting a coercion later in the file?  The latter could be forbidden, maybe.
 

The MM0 parser specification is not deterministic

Would it be possible (and worth it in terms of pros and cons) to make it deterministic ?

 

Finally, I want to point out that your example is slightly unrealistic. The MM0 type system is (somewhat deliberately) impoverished, and it would be very unlikely for you to actually have types "scalar" and "vector" unless you are in a (very limited) kind of first order proof environment for modules. You wouldn't be able to do much interesting vector space theory there, because you have no higher order constructs. Much more likely, you are working in a ZFC style foundation where everything has the same type "set", and then type information is next to useless for this kind of thing.

Indeed, and that's a good point, and this was for the sake of the example.  There might be other applications of MM0 not based on set theory, towards type theories, where there could be real-life examples like this.
 

I will add that I fell into this (cognitive) trap myself, and Giovanni caught me on it. I said to myself "It doesn't make any sense for "e." to be right or left associative, because it has type set x set -> wff, so it can't associate with itself anyway, so I'll just make it left assoc". But this is not true, because "~" lives at the same precedence, and if "e." is left assoc then there is a conflict, while if "e." was right assoc then there would be no conflict. Because *types don't matter during parsing* (at least, with the MM0 parser algorithm as it currently exists). I've written a simple C compiler before, and the "A * b;" example of type-disambiguation between a multiplication statement and a pointer declaration is a real thing (and a real pain). I don't want to replicate that.

That's a clear explanation.  But in the present case, I would say that a solution which is better for human comprehension is to give lower precedence to "~".

The suffix and mixfix ideas sound promising, and they would have real-life applications indeed.

 

I suppose that's true, but it's not obvious. MM0 is designed to be read, and having mystery rules like that seems like a good way to scare people off. The precedence system is supposed to be minimal and expressive, but not surprising, and I can already see the angry github issues asking why changing a precedence from 42 to 43 with nothing else nearby breaks their code.

Agreed: this was more of a theoretical remark !
 

Regarding the barb about neglecting mathematical practice, I still don't see your argument. Your example with modules fits perfectly well within the MM0 precedence system. Yes you have to write those precedences down, and if you get it wrong then things don't typecheck, but that doesn't mean that "." isn't right associative in the example. It's *obviously* right associative because the other option doesn't typecheck, but you seem to be taking from this fact that it's not associative at all, which isn't true; a non-associative operator (which MM0 doesn't support) would *always* require parentheses.

No: I'm taking from this fact that I should not have to specify its associativity since it is obviously right-associative.  But I agree that this puts too much work on the parser (if it's even possible, as you said).

Benoît

[fl]

Thanks for the clear explanations.  I didn't know this use of the word "barb", and I see on dictionary.com "unpleasant remark".  My remarks were certainly not meant to be unpleasant, and I'm interested in seeing where MM0 goes.

Mario didn't want to hurt you. But you know that when you speak a foreign language ant that you have just learned a new word like "barb", you

want to use it at oncre. I'm sure you  do likewise. It's all human.

-- 

FL 

[Mario Carneiro]

On Mon, Nov 11, 2019 at 4:46 PM Benoit <benoit...@gmail.com> wrote:

Regarding the barb about neglecting mathematical practice, I still don't see your argument. Your example with modules fits perfectly well within the MM0 precedence system. Yes you have to write those precedences down, and if you get it wrong then things don't typecheck, but that doesn't mean that "." isn't right associative in the example. It's *obviously* right associative because the other option doesn't typecheck, but you seem to be taking from this fact that it's not associative at all, which isn't true; a non-associative operator (which MM0 doesn't support) would *always* require parentheses.

Thanks for the clear explanations.  I didn't know this use of the word "barb", and I see on dictionary.com "unpleasant remark".  My remarks were certainly not meant to be unpleasant, and I'm interested in seeing where MM0 goes.

I think the definition doesn't quite do the word justice. It can also mean "critical" (as in critique) in addition to more hurtful senses, depending on context. I use the word in the sense of a quick comment that makes a critical point but doesn't elaborate.

Is it always possible to put parentheses, even where they are not needed? I mean: is there a rule saying that if A is an expression of some type, then ( A ) is also an expression of the same type, so that I can write e.g. "( a * b ) + c" even when "a * b + c" is valid?

Yes, parentheses are specifically recognized by the parser and allows you to nest any low precedence expression inside a high precedence environment. The relevant production from the grammar is

expr(max) <- "(" expr(0) ")"

It may seem strange that you have to redundantly specify this information, but it's not really redundant. How can MM0 know that scalar is not a subtype of vector? It may not be right now, but perhaps later you decide to add a coercion and then it becomes ambiguous.

Do you mean: changing one's mind at a later time, or putting a coercion later in the file?  The latter could be forbidden, maybe.

I mean putting a coercion later in the file. It could be forbidden, but then this entails making precise the rules that dictate the acceptability of the added coercion (and an efficient decision procedure for the criterion). There is already a similar kind of restriction on coercions: the coercion graph is required to have no diamonds (more than one path between any two fixed vertices), and this is checked using a dynamic version of the Floyd-Warshall algorithm.

 

The MM0 parser specification is not deterministic

Would it be possible (and worth it in terms of pros and cons) to make it deterministic ?

Perhaps this is the wrong way to say it. The parser itself is deterministic, because the CFG is unambiguous. There is only one parse according to the CFG, so any valid parse algorithm will get the same result.

You can still have determinism with an ambiguous grammar by simply having a parsing algorithm that picks something from the grammar, and using that algorithm as the definition of the parser. But in this case, the CFG becomes superfluous, as it isn't actually defining the language correctly - it specifies that certain parses are valid that really aren't. I would much prefer for the CFG to be authoritative and unambiguous, so that the parsing algorithm is not a part of the specification.

 

Finally, I want to point out that your example is slightly unrealistic. The MM0 type system is (somewhat deliberately) impoverished, and it would be very unlikely for you to actually have types "scalar" and "vector" unless you are in a (very limited) kind of first order proof environment for modules. You wouldn't be able to do much interesting vector space theory there, because you have no higher order constructs. Much more likely, you are working in a ZFC style foundation where everything has the same type "set", and then type information is next to useless for this kind of thing.

Indeed, and that's a good point, and this was for the sake of the example.  There might be other applications of MM0 not based on set theory, towards type theories, where there could be real-life examples like this.

Actually, type theories will look at the type system of MM0 and say that it is too weak. Almost any self-respecting type theory has an infinite number of types, for example N and N->N and (N->N)->N and ((N->N)->N)->N and so on. MM0 has a finite number of types, and they all have to be declared in advance, which is why (try to) I call them "sorts" instead because "types" suggests a flexibility that MM0 sorts don't have.

This means that you can't use sorts in place of types in a type theory, so you have to model them inside the logic. This is deliberate, because using sorts as types in my experience only leads to sadness, because this ties the complexity of the type system to the complexity of the foundations, and it's never good enough. HOL uses a type theory that gives you type constructors and function types but no binders, and people said "hey look we can make lots of interesting mathematical sets in here" and used the type system for *sets* in the math sense. But then they become unhappy when they realize that math sets need more than this; categories and schemes are higher order objects, and you have things like Z/pZ where a type depends on a term; suddenly simple type theory is too simple, so the foundation must grow to dependent type theory. But then you get a big convertibility judgment for deciding if a term of type Z/4Z is also of type Z/(2+2)Z, and you want type checking to be decidable but also really powerful, efficiency goes way down, and it generally becomes a logical mess. And the mathematicians are still not happy because the system doesn't let certain true things be type correct.

I want to sidestep this whole thing by making the type system so impoverished that anything at all nontrivial must go inside the logic. Once that becomes the standard idiom, the tooling evolves to represent it, and you still get the nice type system in the end, but it's not tied to complexity of the foundations any more; you can extend the type system at will by changing the tactics and leaving MM0 untouched.

I will add that I fell into this (cognitive) trap myself, and Giovanni caught me on it. I said to myself "It doesn't make any sense for "e." to be right or left associative, because it has type set x set -> wff, so it can't associate with itself anyway, so I'll just make it left assoc". But this is not true, because "~" lives at the same precedence, and if "e." is left assoc then there is a conflict, while if "e." was right assoc then there would be no conflict. Because *types don't matter during parsing* (at least, with the MM0 parser algorithm as it currently exists). I've written a simple C compiler before, and the "A * b;" example of type-disambiguation between a multiplication statement and a pointer declaration is a real thing (and a real pain). I don't want to replicate that.

That's a clear explanation.  But in the present case, I would say that a solution which is better for human comprehension is to give lower precedence to "~".

I agree.

Regarding the barb about neglecting mathematical practice, I still don't see your argument. Your example with modules fits perfectly well within the MM0 precedence system. Yes you have to write those precedences down, and if you get it wrong then things don't typecheck, but that doesn't mean that "." isn't right associative in the example. It's *obviously* right associative because the other option doesn't typecheck, but you seem to be taking from this fact that it's not associative at all, which isn't true; a non-associative operator (which MM0 doesn't support) would *always* require parentheses.

No: I'm taking from this fact that I should not have to specify its associativity since it is obviously right-associative.  But I agree that this puts too much work on the parser (if it's even possible, as you said).

If this is your position, then it comes too close to "inference" for my taste. MM0 used to do more type inference with the "var" keyword, but I don't think that excessive type inference is good for readability. Instead, all that inference has been shuffled off to MM1, and MM0 requires everything be declared in advance, so that it can give errors in the right places. It's not required that an operator of type A x B -> B be right associative; if there is a coercion A -> B then arbitrary grouping is possible. I can imagine MM1 or similar making guesses about this and populating the fields as necessary, but MM0 is all about saying what you mean up front. No one reads specs anyway, but the best way to make a language feel simple and obvious is for it to actually be simple.

Mario

[Benoit]

I hope parts of this discussion will make their way into some kind of documentation, in particular the possibility to add extra parentheses and the fact that MM0 uses the term "sort" instead of "type" because the type system is voluntarily poor, and if some type theory is to be implemented, this has to be within the logic, and not the metalogic.

 

I mean putting a coercion later in the file. It could be forbidden, but then this entails making precise the rules that dictate the acceptability of the added coercion (and an efficient decision procedure for the criterion). There is already a similar kind of restriction on coercions: the coercion graph is required to have no diamonds (more than one path between any two fixed vertices), and this is checked using a dynamic version of the Floyd-Warshall algorithm.

Maybe this type of "delayed coercions" could be forbidden, but I cannot tell whether it is worth it (nor could I tell the precise rules and decision procedure).

 

The MM0 parser specification is not deterministic

Would it be possible (and worth it in terms of pros and cons) to make it deterministic ?

Perhaps this is the wrong way to say it. The parser itself is deterministic, because the CFG is unambiguous. There is only one parse according to the CFG, so any valid parse algorithm will get the same result.

This is what I understood.  I was referring to making the CFG deterministic, in the sense of deterministic CFGs as a proper subset of unambiguous CFGs, which allow for simpler parsing (https://en.wikipedia.org/wiki/Deterministic_context-free_grammar).  But again, I don't know much in this domain.

Benoît

[Mario Carneiro]

On Thu, Nov 14, 2019 at 11:31 AM Benoit <benoit...@gmail.com> wrote:

I hope parts of this discussion will make their way into some kind of documentation, in particular the possibility to add extra parentheses

This should be in mm0.md, in the grammar if nowhere else. This might be surprising to a metamath user, but it's basically a universal convention in other computer languages.

 

and the fact that MM0 uses the term "sort" instead of "type" because the type system is voluntarily poor, and if some type theory is to be implemented, this has to be within the logic, and not the metalogic.

Hopefully the examples will make this clear, eventually.

I mean putting a coercion later in the file. It could be forbidden, but then this entails making precise the rules that dictate the acceptability of the added coercion (and an efficient decision procedure for the criterion). There is already a similar kind of restriction on coercions: the coercion graph is required to have no diamonds (more than one path between any two fixed vertices), and this is checked using a dynamic version of the Floyd-Warshall algorithm.

Maybe this type of "delayed coercions" could be forbidden, but I cannot tell whether it is worth it (nor could I tell the precise rules and decision procedure).

Actually, this really doesn't work with the inference thing. It is reasonable to have a rule "you cannot simultaneously have X and Y" where you get an error on whichever of X or Y comes later, but if X is the result of inference then we generally want to not flag an error (because we wrote only Y, while X was inferred based on incomplete information at an earlier point), but rather we should backtrack and infer not-X based on the new information Y. This sort of thing works decently well for type inference a la Haskell, but it's a very non-local process, meaning error messages can be pretty bad, plus backtracking kills single pass analysis. Also inferring associativity plus backtracking means that a change later in the file can change the parse of an earlier statement. Very bad.

 

The MM0 parser specification is not deterministic

Would it be possible (and worth it in terms of pros and cons) to make it deterministic ?

Perhaps this is the wrong way to say it. The parser itself is deterministic, because the CFG is unambiguous. There is only one parse according to the CFG, so any valid parse algorithm will get the same result.

This is what I understood.  I was referring to making the CFG deterministic, in the sense of deterministic CFGs as a proper subset of unambiguous CFGs, which allow for simpler parsing (https://en.wikipedia.org/wiki/Deterministic_context-free_grammar).  But again, I don't know much in this domain.

It is a DCFG. Just about any CFG that is "unambiguous by construction" will be a DCFG. The DCFG recognizer is probably pretty big, though, without some more optimizations, because you need a nonterminal for every precedence level, while a parsing algorithm can just use integers for this purpose without a lot of repetition.

 

Mario