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 -- 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/c66f8097-1b86-48ac-8a82-11f6469c26a3%40googlegroups.com.
