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.
