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/CAFXXJSs43X3RzHmC0YUqRdkRe22YRZVZsR_qgDDN499dC-np0A%40mail.gmail.com.
