I was writing a Metamath verifier some time ago (in OCaml), and I found looking at mmverify.py in Python by Raph Levien very useful, see https://github.com/david-a-wheeler/mmverify.py/blob/master/mmverify.py (the "proof decompression" was added by Scott Fenton). Actually, I made a PR that avoids decompression and directly verifies the compressed proofs (making a four-fold speedup), that adds some comments (some especially relevant to your questions) and typing annotations for clarity, and that separates the different steps (see the three functions "treat_step", "treat_normal_proof", and "treat_compressed_proof"), see https://github.com/benjub/mmverify.py/blob/faster/mmverify.py.
Benoît On Monday, May 2, 2022 at 7:41:44 PM UTC+2 [email protected] wrote: > Hi Phillip, > > On Mon, May 2, 2022 at 1:16 PM 'Philip White' via Metamath < > [email protected]> wrote: > >> I have two questions: >> >> 1. What is a subproof? I thought that uncompressed proofs are just >> sequences of labels, so there doesn't seem to be enough structure for >> steps to refer to a "subproof". >> > > A normal mode proof is essentially a tree of theorem applications written > in reverse polish notation (RPN), so the "subproof" corresponding to a > given step is all the steps that lead into it. For example if the last step > is ax-mp which has four arguments (two wffs and two hypotheses) then the > subproof ending at that step is the "ax-mp" step plus the four subproofs > that came before it (recursively using this definition to define the extent > of those four subproofs). > > You could use something like that to convert a proof to normal mode if you > wanted, but I don't recommend it for verification, since there is a much > simpler and asymptotically far less wasteful way to check the proofs (see > next point). > > 2. Should the compressed proof verifier skip running steps of a saved >> subproof the second time it sees it? Given my first question, I don't >> really understand what steps a subproof will contain, so I can't even >> tel if skipping the duplicate steps would end up being sound. I would >> have expected a verifier to operate on a stream of labels, and then the >> uncompressed or compressed verifiers would merely be a fold over those >> labels. However, if we skip sub-proofs, that means the compressed >> verifier is not just a different representation, but also a different >> algorithm. >> > > The key to understanding this is to view a normal mode proof not as a tree > structure like I mentioned above, but instead as operations on a stack > machine. The stack starts empty, and each theorem reference pops n > statements from the stack (where n is the arity of the theorem) and pushes > one more statement. At the end there should be exactly one statement on the > stack, which should match the $p statement. This encodes the RPN structure, > so it's really the same thing stated in a different way, but this > generalizes better to the compressed case. > > The stack elements here are "statements", which are roughly speaking the > stuff that can go in the body of a $e or $p ... $= , that is, a token > string consisting of a constant (the typecode) followed by zero or more > constants or variables. The existence of such an element on the stack > represents that in the current theorem context, that expression is > provable, so if we get the final $p expression on the stack then we have > proven the theorem, and each theorem application is asserting that since > certain things are provable we can deduce that something else is provable. > These stack elements don't have any names, they are just steps in the proof > and they get constructed in a tree structure based on the order of theorem > applications. > > With compressed proofs, we add another data structure, the "heap", which > also consists of statements but has random access unlike the stack. The Z > command pushes the thing on top of the stack to the heap (labeled with the > next available number). When you reference a heap element, that statement > is pushed onto the stack. So you can do a big subproof to generate some > statement, save it to the heap (which does not pop it from the stack), and > then recall it later to use that same statement 2 or more times in the same > proof without having to go through all the steps of the proof again. > > Mario > -- 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/80ae3687-3523-4a8b-9a04-f9991dd12af2n%40googlegroups.com.
