Hi Jim,
The grammar parser of metamath-knife might be used to that effect.
You can generate an image of the parsing tree with the following commands:
git clone https://github.com/metamath/metamath-knife.git
cd metamath-knife
cargo run --features dot -- -E <PATH TO SET.MM>
dot -Tsvg -o grammar.svg grammar.dot
I've uploaded a recent image built with these instructions here:
https://mm.tirix.org/grammar.svg
There, you can see the node parsing a "dju" syntax at node 531.
metamath-knife's -g and -p options will respectively build the grammar
parse tree, and check the statement's grammar. If the first fails, the
grammar might be ambiguous.
Currently the following "garden path" commands help metamath-knife's
parser with syntaxes such as copab and coprab :
$( $j garden_path ( A => ( ph ;
type_conversions;
garden_path ( x e. A => ( ph ;
garden_path { <. => { A ;
garden_path { <. <. => { A ;
BR,
_
Thierry
On 31/05/2025 02:06, Jim Kingdon wrote:
On 5/30/25 12:10, Mario Carneiro wrote:
this is one of the most difficult cases in the proof of unambiguity.
See https://us.metamath.org/downloads/grammar-ambiguity.txt for more
on this
Has anyone done any work on a tool to automatically check the metamath
grammar for ambiguities? When I was encouraged to add additional
syntax I was told "oh don't worry it won't be ambiguous". I presume
that was true in the particular case which I think was probably
https://us.metamath.org/mpeuni/df-dju.html although I don't remember
for sure whether that is the only syntax I've added. Maybe this isn't
quite up there with the definition checker in terms of likely ways to
introduce unsoundness, but if we did manage to make the grammar
ambiguous it likely would have similar consequences to the things the
definition checker checks for.
--
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 visit
https://groups.google.com/d/msgid/metamath/05148385-b5d6-4483-8e5c-7f65e3678125%40gmx.net.
