Parsing Metamath proof statements into expression trees

[void4]

Given a proof statement like $p wff ( A -> ( B -> C ) ) $=, is it always possible to parse it into an expression tree?

In this case

[wff, 
    [->, 
        [A, 
            [->, 
                [B, C]
            ]    
        ]
    ]
]

Or does the way Metamath uses its substitutions prevent this?

Or, asked differently, given the set.mm database, can I create a parser that gives me these trees?

A use case would be outputting the statements in another format (e.g. Latex), or analyzing tree transformations.

[digama0]

One thing to notice is that the proof of $p wff ( ph -> ( ps -> ch ) ) is effectively its expression tree. In this case there is exactly one proof, written in RPN as wph wps wch wi wi or in function style as wi(wph, wi(wps, wch)), which is the expression tree you are looking for. Just like regular theorems, some strings have no proof, some have many. These correspond to statements that are not well formed in the first case and ambiguities in the grammar in the second.

The set.mm grammar has no ambiguities, but this is not enforced by metamath - a standards-conforming metamath verifier makes no attempt to prove that statements have a unique parse. They are effectively given a parse as part of the proof, so a basic verifier will not even need to know how to do math parsing. The IDE-like verifiers and proof authoring tools, like MM-PA and mmj2, will perform math parsing on the strings in order to discharge these proof obligations automatically.

Moreover, mmj2 has a special parser that only works on a class of grammars that are unambiguous by construction, so if this parser succeeds then this amounts to a proof that the grammar is unambiguous. We run this parser on set.mm as part of our continuous integration system, so we can be sure that set.mm stays unambiguous.

If you have any other questions, feel free to drop by the mailing list (https://groups.google.com/forum/#!forum/metamath), where most of the discussion traffic is.

[tirix]

As for “outputting the statements in another format (e.g. Latex)”, this is the way the “structured” typesetting works: it considers the tree rather than the string of symbols.

You can check it out at [http://metamath.tirix.org/index.php]

Right now it’s working with MathML, but the exact same principle would also work with LATeX. Only the definition file would need to be changed.

[void4]

Thanks!