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 -- 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/e53012ea-28a6-4f78-af10-2685e4b38dae%40googlegroups.com.
