Sorry for causing confusion. Oh dear, I did say I was pretty hazy on the
concept of unification didn't I.
> in a metamath verifier unification is trivial
Yes. Because a proof contains both "essential hypotheses" (logical
assertions) and "non-essential hypotheses" (syntax construction), there is
really very little unification work left for a verifier to do. That means
the proof assistant has to do it. The metamath book uses the proof in
demo0.mm as an example
$( Prove a theorem $)
th1 $p |- t = t $=
$( Here is its proof: $)
tt tze tpl tt weq tt tt weq tt a2 tt tze tpl
tt weq tt tze tpl tt weq tt tt weq wim tt a2
tt tze tpl tt tt a1 mp mp
$.
And guides the reader through proving it in metamath.exe with commands
(Section 2.4 - Your First Proof): assign 1 mp, assign 4 mp, assign 3 a2,
etc.
So you have to specify all the essential hypotheses (a1, a2, mp), but the
proof assistant usually manages to infer all the syntax construction stuff
(tt, tze, tpl, weq, etc.). I currently have no clue where these come from
and how it manages to do that, but this is the unification algorithm I was
referring to.
> DOES MMJ use the same algo?
> HOW does MMJ do it?
Yes, you're asking all the right questions, I'd like to know too :-)
> My intuition (I've never broached this notion before, I look forward to
seeing if it falls completely flat on its face here) is that as things
stand at the moment there are three pillars to working with mm files -
verification, unification, and html generation.
Now I've said it out loud (so to speak) and had a chance to think about it,
this isn't profund at all is it. All I'm really saying is that as a
metamath user I'd like to be able to
1. Write my proof and have most of the syntax construction bits
automatically filled in (unification)
2. Verify that my proof is correct (verification)
3. Have my proof displayed to myself and others in a nice format (html
generation)
So it's obvious why those are the most fundamental parts of the system. Oh
well.
Best regards,
Antony
On Mon, Aug 22, 2022 at 12:53 AM Peter H. Meadows <
[email protected]> wrote:
> > That's the piece of MMJ I'd be after first if it was me.
>
> OK. Thanks for this clue! :)
>
> > (you can un-unify a regular proof by removing all the tokens who's
> expressions don't start with |-
>
> ??? un-unify??
>
> > but I don't know how you put them back in.
>
> > It's important because having to specify all the symbols used in a proof
> would be really pedantic).
>
> ?
>
>
> in a metamath verifier unification is trivial because:
> (
> Mandatory hypotheses must be pushed on the proof stack in the order in
> which they appear.
> In addition, each variable must have its type specified with a $f
> hypothesis
> before it is used and that each $f hypothesis have the restricted
> syntax of a typecode
> (a constant) followed by a variable.
> The typecode in the $f hypothesis must match the first symbol of the
> corresponding RPN stack entry
> (which will also be a constant),
> so the only possible match for the variable in the $f hypothesis
> is the sequence of symbols in the stack entry after the initial constant.
> )
>
>
> to discover new proofs
> is non-trivial because ... ... Godel... etc. P != NP ......?
>
>
>
> The general algorithm for unification described in the literature is
> somewhat complex.
> In the Proof Assistant, a more general unification algorithm is used.
>
> DOES MMJ use the same algo?
> HOW does MMJ do it?
>
> What is the best (description of the) algorithm? ?
>
> GtMM currently has some tricks/features.
> eg, you can work forwards and backwards.
>
> forwards = starting with the essential hypoths and moving from left right .
>
> backwards = starting with the chain we want to make and moving right to
> left.
> suppose we guess at the last machine we'll use,
> then GtMM can show us what chain(s) that machine would need for its inputs
>
>
>
>
>
>
> chains are strings of blobs.
> blobs are metamath variables.
> triangular blobs are variables that can be 'mapped' to other chains.
> square blobs cannot be mapped.
>
>
> unification = doing the mapping? / finding it
>
> |- = provable / starting chain / essential hypoths
>
> GtMM just ignores floating hypoths????
>
> chain we need to make to complete the level
> always shown top-center in Gtmm
>
> essential hypoths = chains given to start with,
> they are used as input for the machines.
> shown in top left of gtmm.
>
> machines you can use (= things we've already proved)
> are shown on the right of the screen.
>
> click on a machine to add it to the workspace pane.
> workspace pane is always in the center of gtmm screen.
>
>
>
>
>
>
>
> 4.3.1 The Concept of Unification During the course of verifying a proof,
>
> when Metamath encounters an assertion label,
> it associates the mandatory hypotheses of the assertion
> with the top entries of the RPN stack.
>
> Metamath then determines what substitutions
> it must make to the variables in the assertion’s mandatory hypotheses
> in order for these hypotheses to become identical to their
> corresponding stack entries.
>
> This process is called unification.
>
> (We also informally use the term “unification”
> to refer to a set of substitutions that results from the process,
> as in “two unifications are possible.”)
>
> After the substitutions are made,
> the hypotheses are said to be unified.
>
> If no such substitutions are possible,
> Metamath will consider the proof incorrect and notify you with an error
> message.
>
> While a proof is being developed, sometimes not enough information is
> available to determine a unique unification.
> In this case Metamath will ask you to pick the correct one.
>
>
>
>
>
>
>
>
>
> How is MetamathZero different?
>
--
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/CAJ48g%2BDpw5XixJu8Sv80JpkywVfn0s16zxcGDmpd9kxwuCfsGA%40mail.gmail.com.
