I think that this incident has made it clearer that we need a proper spec for definition checking though, as well as at least one other implementation, suitable as a reference implementation and not tied to a complex system. Unfortunately definition checking requires higher parsing requirements than verification, because axioms don't come with parse trees, plus you have to be able to read $j rules (or be willing to hardcode lots of things like the names of sorts).
On Tue, Sep 24, 2019 at 6:29 PM Jim Kingdon <[email protected]> wrote: > Thanks to everyone who worked on this issue. As described in that github > issue, we now have a (better) working definition checker as part of the > Travis build. > > The definition checker means that unsound definitions are a matter of > "well, we might or might have an elegant design but we at least have a > way of catching mistakes or people who don't understand the system well > enough" as opposed to "OMG we need to rearchitect the whole thing > because how can we trust the hundreds of definitions in set.mm?". > > On 9/24/19 11:54 AM, David A. Wheeler wrote: > > FYI: > > > > @wlammen recently posted an example where an unsound definition causes > problems: https://github.com/metamath/set.mm/pull/1089 > > Details below if you'd like. > > > > This is expected per the Metamath book, because definitions are just > axiomatic ($a) statements, and Metamath verifiers merely confirm that > proven ($p) statements follow from $a statements. There are far fewer > definitions than proven statements, and definitions are generally far > simpler than proofs. > > > > That said, we don't *really* want unsound definitions. mmj2 already has > a number of checks on definitions. Thanks to Mario, mmj2 version v2.5.3 now > has a tweaked definition checker that does a deifnitional soundness check, > which rejects this kind of nonsense. This version of mmj2 is now > incorporated in our CI build, so every merged change into set.mm will be > checked to prevent these kinds of crazy things. > > > > A related improvement: previously mmj2's checkers were configured to > exclude df-sbc , because it reused a constant that has already been > introduced, namely [ A / x ] ph. However, Norm changed it to use new > constants in Jan 2017. df-sb is '[ y / x ] ph' and df-sbc is now '[. A / x > ]. ph'. So df-sbc can be removed from the exception list, so that's one > less thing that needs to be handled specially. > > > > For more about this, see: https://github.com/metamath/set.mm/pull/1089 > > > > --- David A. Wheeler > > > > P.S. Here's the definition that caused the problem. > > > > $( Declare a new symbol. $) > > $c BustVerifier $. $( A meaningless symbol $) > > > > $( Extend wff definition to include BustVerifier. $) > > wbustverifier $a wff BustVerifier $. > > > > ${ > > $d x y $. > > $( Try to bust the proof verifier using this definition. > (Contributed by > > Wolf Lammen, 9-Sep-2019.) $) > > df-bust-verifier $a |- ( BustVerifier <-> x = y ) $. > > $} > > > > ${ > > $d x y $. > > $( A contradiction. (Contributed by Wolf Lammen, 9-Sep-2019.) $) > > bust-verifier $p |- ( -. x = y -> F/ x x = y ) $= > > ( weq wnf wn wbustverifier df-bust-verifier bicomi nfv nfxfr a1i > ) ABCZAD > > LELFAFLABGHFAIJK $. > > $} > > > > -- > 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/a0108bbd-b35e-71ec-223a-6b9e0c591be7%40panix.com > . > -- 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/CAFXXJSuwOGEunAvNwrE1X44%2BMMTjrZWq5MUT1%3DxOXGVF1LoC3Q%40mail.gmail.com.
