Benoit's description is a good explanation of how mmj2's definition checker works today. The main worry I have about a pure reimplementation is the automated theorem prover part.
If you aren't worried about dependence on set.mm metatheory, or on actually producing proofs, the easiest algorithm to implement is to keep track of all binding operators, and ensure that all dummies are not free in the true sense (while also calculating the binding structure of the new definition). On Thu, Sep 26, 2019, 2:28 PM David A. Wheeler <[email protected]> wrote: > Here's a first cut at modifying the "conventions" text to > explain the additional rules for the definitioncheck and also LRParser. > I took existing text as a starting point. I think it's > important to have "Rule 5" and "Rule 6" as separate items, since > that is how users will see error reports. > > Mario: I know you're working to generalize this, but I think it's > important to document "as it is" now, and refine it as other > refinements occur. > > --- David A. Wheeler > > ============================ > > > diff --git a/set.mm b/set.mm > index 7ff58bf..4b4c9cb 100644 > --- a/set.mm > +++ b/set.mm > @@ -369106,7 +369106,81 @@ $) > renamer theorem like ~ cbval . The section > ~ mmtheorems32.html#mm3146s also describes the > metatheorem that underlies this. > - </p></HTML> > + </p> > + > + <p> > + Standard Metamath verifiers do not distinguish between axioms and > + definitions (both are $a statements). > + In practice, we require that definitions (1) not be creative > + (a definition should not allow an expression > + that previously qualified as a wff but was not provable > + to become provable) and be eliminable > + (there should exist an algorithmic method for converting any > + expression using the definition into > + a logically equivalent expression that previously qualified as a > wff). > + To ensure this, we have additional rules on almost all definitions > + ($a statements not beginning with the name ax-). > + These additional rules are not applied in a few cases where the > rules > + are too strict ( ~ df-bi , ~ df-clab , ~ df-cleq, ~ df-clel ); > + see those definitions for more information. > + These additional rules are checked by at least > + <A HREF=" > https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/definitionCheck.js > " > + >mmj2's definition check</A>. > + This definition check relies on the database being very much like > + set.mm, down to the names of certain constants and types, so it > + cannot apply to all Metamath databases but is useful in set.mm. > + In this definition check, a $a-statement with a given label and > + typecode ` |- ` passes the test if and only if it > + respects the following rules in order (these rules imply that we > have > + an unambiguous tree parse, which is also checked): > + </p> > + > + <ul> > + <li>Rule 1: > + The expression must be a biconditional or an equality (i.e. its > + root-symbol must be ` <-> ` or ` = `). > + We define its definiendum as its left hand side (LHS) and > + its definiens as its right hand side (RHS). > + We define the *defined symbol* as the root-symbol of the LHS. > + We define a *dummy variable* as a variable occurring > + in the RHS but not in the LHS. > + Note that the "root-symbol" is the root of the considered tree; > + it need not correspond to a single token in the database > + (e.g. ~ w3o or ~ wsb ). > + <li>Rule 2: The defined symbol should not occur in an earlier > + $a-statement with typecode ` |- ` or in any another place > + in this labelled expression. > + <li>Rule 3: No two variables occurring in the LHS should share a > + distinct variable (DV) condition. > + Without this rule, you can define something like > + cbar $a wff Bar x y $. > + ${ $d x y $. df-bar $a |- ( Bar x y <-> x = y ) $. $} > + and now "Bar x x" is not eliminatible; > + there is no way to prove that it means anything in particular, > + because the definitional theorem that is supposed to be > + responsible for connecting it to the original language wants > + nothing to do with this expression, even though it is well > + formed. > + <li>Rule 4: All dummy variables are required to be disjoint from > any > + other (dummy or not) variable occurring in this labelled > expression. > + <li>Rule 5: Either > + (1) there must be no non-set dummy variables, or > + (2) there must be a justification theorem. > + The justification theorem must be of form > + ` |- ( ` definiens root-symbol definiens' ` ) ` > + where definiens' is definiens but the dummy variables are > replaced > + with other unused dummy variables of the same type. > + Note that root-symbol is ` <-> ` or ` = ` , and that set > variables > + are simply variables with the ` setvar ` typecode. > + <li>Rule 6: One of the following must be true: > + (1) there must be no set dummy variables, > + (2) there must be a justification theorem as described in Rule > 5, or > + (3) we must prove that each dummy set variable is > + not free, that is, we must prove that > + ` ( ph -> A. x ph ) ` for each dummy variable ` x ` > + where ` ph ` is the definiens. > + Part 3 of rule 6 is typically how most dummy variables are > handled. > + </ol></HTML> > > Here is more information about our processes for checking and > contributing to this work: > @@ -369135,6 +369209,34 @@ $) > (triggering further review). > </li> > > + <li><b>LRParser check.</b> > + Metamath verifiers ensure that $p statements follow from previous > + $a and $p statements. > + However, by itself the Metamath language permits certain kinds of > + syntactic ambiguity that we want to avoid in this database. > + Thus, we require that this database unambiguously parse > + using the "LRParser" check (implemented by at least mmj2). > + Details are in > + <A HREF=" > https://github.com/digama0/mmj2/blob/master/src/mmj/verify/LRParser.java"; > + >LRParser.java</A>. > + This check > + <A HREF="https://github.com/metamath/set.mm/pull/754"; > + >counters, for example, a devious ambiguous construct > + developed by saueran at oregonstate dot edu</A> > + posted on Mon, 11 Feb 2019 17:32:32 -0800 (PST) > + based on creating definitions with mismatched parentheses. > + <!-- Devious Construct: > + ${ > + wleftp $a wff ( ( ph ) $. > + wbothp $a wff ( ph ) $. > + df-leftp $a |- ( ( ( ph ) <-> -. ph ) $. > + df-bothp $a |- ( ( ph ) <-> ph ) $. > + anything $p |- ph $= > + ( wbothp wn wi wleftp df-leftp biimpi df-bothp mpbir mpbi > simplim > + ax-mp) ABZAMACZDZCZMOEZOCQAEZNDZRNAFGSHIOFJMNKLAHJ $. > + $} > + --> > + > <li><b>Proposing specific changes.</b> > Please propose specific changes as pull requests (PRs) against the > "develop" branch of set.mm, at: > > -- > 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/E1iDYUy-0003oQ-5I%40rmmprod07.runbox > . > -- 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/CAFXXJSsRCphwcvSZJvvtt5Twmm9HEcSmE3qGoV8K%3D86dnM9ggQ%40mail.gmail.com.
