Question about the notation system

[Lakedaemon]

Hello Mario

I am developing a software infrastructure to teach & do maths in 70+ languages (that will ultimately be mm0 interroperatable instead of being mm0 based). It is now quite advanced and I am at the stage where I now have to rewrite my parser to make it dynamic that should parse mathml trees (with attributes to desambiguate things) and It would really speed development if you could answer the following question :

What are the limitations of the mm0 notation system ? (with regards to infixl, infixr, prefix and notations & the way humans naturally write math) ?

1. can "- A" be parsed with a prefix simple notation with arity = 1 ?
2. can "3 !" be encoded with an infixl simple notation with arity=1 ?
3. Are there things in maths that CANNOT be expressed simply and naturally with the notation system
4. What about "f(x,y,z)" ?
5. Should I consider a different kind of parser ?

(I do not want to write "3 !" as "Fact 3", as my aim is to make math easily usable worldwide for all people without special training)

The GALIPH project 2 months old results : presentation of the project (in english) latest results a computation (in french)

Best regards, Olivier

[digama0]

All of the above are supported by the notation system implemented by MM0. (You need to use notation instead of infixl for postfix notations though.) However you cannot mix prefix and postfix operations at the same precedence level, otherwise - A ! would be ambiguous.

As for things the notation system cannot handle, I think the main category of over-conservativity is the fact that constants cannot be reused: you can't define A. x e. A, ph and A. x, ph simultaneously, because every notation needs to contain a constant symbol used in no previous notation. But there are probably lots of things; the notation system is very simplistic and was intended to capture only the most common cases. It's difficult to come up with a larger subset which is still easy to prove unambiguous though.

[Lakedaemon]

A. Apparently I managed (thanks to your answers and to the inspiration provided by mm0) to write a good and flexible dynamic parser for mathml to mathTrees (akin to the math trees of mm0)

Parsing mathml (trees & attributes !) instead of text brings quite a lot of flexibility and solve some problems :

• unique constants
• infix & postfix operators with an arbitrary number of children
• looks like standard math
• mixing maths with simple decorations
• invisible ops

As the parser will have to cope with documents mixing different styles (as can be found in the wild), it will probably still have to evolve a bit to

• handle decorations (spaces, funky parentheses...)
• handle different kind of invisible ops (multiplications, intersections...)
• handle DSL/subtree parser configurations (to handle physics, mechanics, statistics, and different styles...)
• and who knows what more... ? (not me)

I just hope that a simple solution exists thanks to attributes & mathml trees, it behaves like math so maybe it can do what math is able to do.

B. Now that the conversion layer (subset of TeX => mathml with attributes => mathTree => subset of TeX or mathml with attributes) is operational, though not finished, I'll start working on the next step :

match & unify mathTrees

At the moment, my mathTrees only have

• vars

• numbers

• terms

• I'm thinking of having mathTrees mostly similar to mm0 mathTrees with :

• sorts

• vars, dummies, binders & types

• terms

• defs

• axioms

• theorems

• proofs

but I'm wondering if I should add a new node "encoded" to sementically represent

• numbers
• matrices ?
• functions ? in a compact and performent manner

something that translates arbitrary stuff like ; ; ; ; ; ; 1 2 3 4 5 6 7 into the (compact and sementic) string representation '1234567'

I remember integer computations taking such a huge part of a metamath proof and I would like to avoid the memory/performence/energy hit of working with numbers, and computing heavy proofs (by delegating them to other processes, in an optional top to bottom process)