Proof-of-concept for 'syntax axiom based parsing'

[Marnix Klooster]

Hello all,

Just now I uploaded some ugly code to GitHub (https://github.com/marnix/mmpyparse) that implements 'syntax axiom based parsing' for Metamath files.

I posted about that earlier, in 2015, 2016, and 2019 (see GitHub README for exac references), and occasionally worked on a proof-of-concept implementation, but never got around to cleaning it up.

Now I realized I don't know when I _will_ get around to that, so I've uploaded it mostly as-is.  I tried to do a brief-but-careful write-up in the README file, though.

Hope this is useful to someone!

Groetjes,

 <><

Marnix
--

Marnix Klooster
marnix....@gmail.com

[Thierry Arnoux]

Hello Marnix,

Thanks for sharing!

If I understand well, you are parsing by trying all possible matches. This is probably very computationally intensive. One interesting trick used by Norm's Metamath program is to use the fact that set.mm's parentheses are always balanced, i.e. if you count up for each opening parentheses, and down for closing ones, then you know for sure that your sub-expression is not over until your count is back down to zero. This includes all types of parentheses: (), [], <. >., <" ">, etc.

This shall allow to drastically reduce your parsing time for complex formulas like ~opelopabt, but of course works only with well-behaved databases which follow this rule.

It looks like the TOP keywords you introduce have actually the same use as the $j "syntax" commands.

I believe that you could instead say that the syntax tree of a statement ` |- a b c `, is the proof of the corresponding statement ` wff a b c ` where the turnstile |- typecode was simply replaced by the wff typecode. The set.mm database actually has a few such proofs: ~bj-0, ~weq, ~wel, but one could provide such a proof for all statements. (BTW, could this help reduce the database size?)

BR,
_
Thierry

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAF7V2P8AGB9Gd3zSxmH01ng7wDcC3eaDzG%2BRPjymzTuXEh8JyQ%40mail.gmail.com.