Re: [Metamath] Re: mmj2 compact representation for $d statements

2023-04-02 Thread Mario Carneiro
The implementation in mmj2 is here: https://github.com/digama0/mmj2/blob/master/src/mmj/lang/ScopeFrame.java#L154-L294 It does not use the same algorithm as mm-web-rs. I don't have any particular insights regarding the theoretical properties of the mmj2 algorithm. On Sun, Apr 2, 2023 at 9:59 PM

Re: [Metamath] Re: mmj2 compact representation for $d statements

2023-04-02 Thread Mario Carneiro
I recently implemented a variation on this algorithm for mm-web-rs: https://github.com/digama0/mm-web-rs/blob/master/src/render.rs#L1026-L1077 As the function name suggests, the thing to google is "clique cover". It is an NP hard problem, but there are some okay approximations. On Sun, Apr 2,

[Metamath] Re: mmj2 compact representation for $d statements

2023-04-02 Thread Benoit
Did you try searching things like "search complete subgraphs" ? Benoît On Sunday, April 2, 2023 at 1:44:45 PM UTC+2 Glauco wrote: > What's the algorithm used by mmj2 to represent $d pairs as $d sets ? > > For instance, for a given theorem, with yamma I'm producing > > $d ph x $. $d k x $. $d k

[Metamath] mmj2 compact representation for $d statements

2023-04-02 Thread Glauco
What's the algorithm used by mmj2 to represent $d pairs as $d sets ? For instance, for a given theorem, with yamma I'm producing $d ph x $. $d k x $. $d k ph $. $d j x $. $d j k $. $d F x $. $d F k $. $d A x $. $d A k $. $d A j $. whereas mmj2 produces $d A j k x $. $d F k x $. $d k ph x $.