I wasn't talking about set.mm or mmj2. I was talking in metamath in general, which doesn't seem to enforce non-ambiguity since it only reads strings of tokens with no other underlying structure. I was in learning the definition checker rules in terms of learning in detail how definitions are theoretically justified. I didn't know there was a parsing step in mmj2 separate from metamath itself, so I assumed it was part of the definition checker (since theorem grammar is taken care of by 'w' axioms during proof verification).
On Wednesday, July 12, 2023 at 12:02:45 AM UTC-4 [email protected] wrote: > On Wed, Jul 12, 2023 at 4:35 AM Marshall Stoner <[email protected]> > wrote: > >> I trust that intuitively that these definitions are valid. The problem >> is an alias rule can still fail if the syntax of the definition doesn't >> meet certain criteria. If the parenthesis surrounding ↔ were missing in >> the definition of the biconditional, for instance. If I could understand >> how the definition checker for the set.mm database works I would have a >> better understanding. I have my own hypothesis, but I'm not sure if it's >> fully sufficient. > > > That example fails for a very simple reason: it wouldn't parse. Step 0 of > the definition checker is to parse the definition as a wff, and if you omit > the parentheses then the parser would fail on this axiom. This would > actually cause mmj2 to fail if you wrote a non-parsing statement anywhere, > not just in a definition but in any $e, $a, or $p statement. > > If you changed the definition of the syntax "ph ↔ ps" itself to not have > parentheses, and removed it from the definition as well, then it would > parse, but mmj2 would still fail for a different parsing reason: the > resulting grammar is ambiguous and the parser constructs some tables that > witness unambiguity of the grammar, meaning that this parser construction > will fail if the grammar is ambiguous. > > In both cases it isn't really the definition checker catching the error. > The definition checker presupposes that the database has an unambiguous > grammar and all statements parse by that grammar. > -- 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/1c92e482-fcee-4659-a858-076edb89d6e5n%40googlegroups.com.
