Question on definitions (in particular for copab)

[bil...@gmail.com]

We have the assertion: copab $a class { < x , y > | ph } $.

My question is how does one know that < x , y > refers to: cop $a class < A , B > $.

Couldn't the "<" and ">" be just notational constants to syntactically form the class expression being introduced?

In particular, just like the introduction of new wffs, shouldn't we have a detailed syntax breakdown of this "axiom" ?

Something like the following:

-- Detailed syntax breakdown --

wph ph

vx setvar x

cv class x

vy setvar y

cv class y

cop class < x , y >

class using constants { | } and wff and a particular type of class depending on x and y

Of course, that last line is the fuzzy one (whereas detailed syntax breakdown for wffs doesn't have that fuzziness)

[Mario Carneiro]

On Fri, May 30, 2025 at 5:47 PM bil...@gmail.com <bil...@gmail.com> wrote:

We have the assertion: copab $a class { < x , y > | ph } $.

My question is how does one know that < x , y > refers to: cop $a class < A , B > $.

It doesn't! In fact, copab is just a composite syntax containing the tokens "{", "<.", variable x, ",", variable y, "|", variable ph, "}" in that order. It is connected to cop in two ways:

* As a visual aid, since this is often how people write ordered pair abstractions (although it visually suggests that it is a special case of an `{ A | ph }` form and that does not exist because the binding structure is weird)

* Because it uses the exact same constant tokens as those used in cop, this is a potential ambiguity in the grammar. It is actually not ambiguous, exactly because `{ A | ph }` is not legal and `{ x | ph }` can only have a variable on the left, which can't start with a `<.` token, but 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; copab is treated in the "type 3" section.

The detailed syntax breakdown looks like this, which should clarify the atomic nature of copab: (note also that x and y have to be set variables here, not classes, which is why the cv steps are missing)

wph ph

vx setvar x

vy setvar y

copab class { <. x , y >. | ph }

[bil...@gmail.com]

So, indeed, the "<" and ">" are just notational constants to syntactically form the class expression being introduced.

In particular, consider the axiom df-opab $a |- { < x , y > | ph } = { z | E x E y ( z = < x , y > /\ ph }.

The first "< x , y >" is just notational syntax, whereas the second "< x , y >" is a "true" ordered pair (justified by cop and df-op.

As an aside: the reason I am bringing this up is that I am trying to allow a user to look up the "meaning" of a metamath symbol.

Thus "copab $a class { < x , y > | ph } $." has no "meaning", but only provides the syntax. I don't have to explain the meaning of < x , y >.

But, df-opab $a |- { < x , y > | ph } = { z | E x E y ( z = < x , y > /\ ph } gives the meaning/semantics of the syntactical expression { < x , y > | ph }.

The user might not know the "meaning" of "< x , y >" on the right hand side, so could request a lookup for its meaning (which is has by df-op).

[Jim Kingdon]

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.

[Thierry Arnoux]

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

[Glauco]

Hi Jim,

Il giorno sabato 31 maggio 2025 alle 02:06:55 UTC+2 kin...@panix.com wrote:

> Has anyone done any work on a tool to automatically check the metamath
> grammar for ambiguities? 

I guess you are asking for set.mm ambiguity, am I right? Or are you actually asking for the metamath language ambiguity? 

Yamma uses Nearly.js to parse every wff in the theory (and every single proof step formula, when you build the model for step suggestions).

Here
https://nearley.js.org/
they state "nearley handles ambiguous grammars gracefully. Ambiguous grammars can be parsed in multiple ways: instead of getting confused, nearley gives you all the parsings (in a deterministic order!)"

In other words, if a wff happened to have multiple possible parsing trees, Nearly.js should return them all.

I check for ambiguity here
https://github.com/glacode/yamma/blob/b7a76cb1992d047c9c425fff8c345c04ad41f255/server/src/mmp/MmpParser.ts#L440

I’m not quite as graceful — I throw an exception that would crash the language server — but that means I’d be able to trace it down easily.

So far, with set.mm, that exception has never been triggered.

I’d feel much more confident setting up a unit test with an intentionally ambiguous theory. If anyone has one handy and wants to open an issue in Yamma’s repo, they’re very welcome to do so.

Glauco

 

[Jim Kingdon]

On 5/31/25 04:17, 'Thierry Arnoux' via Metamath wrote:

> The grammar parser of metamath-knife might be used to that effect.

I've written up this suggestion (and some other ideas from this thread,
such as the idea of maybe using yamma's check in addition) at
https://github.com/metamath/set.mm/issues/4864 . We apparently have many
of the pieces needed to make this a reality.

[Mario Carneiro]

Yes, this informal proof was later turned into the LRParser which is part of mmj2 (actually a slight extension of LR which I call KLR), and this is running in set.mm CI IIRC, so I think that issue is already resolved. (The metamath-knife parser isn't quite as powerful and requires hints to resolve tricky cases, and I'm not entirely convinced it is correct or provides a proof of unambiguity when it completes successfully.) I have a paper proof of the correctness of the KLR parser which I've been meaning to publish at some point, but I don't really know who would be interested in that kind of submission...

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/3b59996d-72f6-4e7f-aad3-14c31b2daab5%40panix.com.