Cheap compare for cyclic terms [injective collation keys]

General
1

Here is a relatively cheap compare for cyclic terms that satisfies the
laws, except lexical order. It is based on the idea to define:

S @<' T :<=> rep(S) @< rep(T)

The only requirement to the function rep is that it is injective,
then the laws, except for lexical order, are automatically satisfied.
The proof are not that difficult in our modern times, where there

are automated proof assistants. Here is an example proof, showing
connectedness of @<' based on connectedness of @<:

/* I am using r for the function rep,
   R for the relation @<' and L for the relation @< */
/* Injectivity */
∀x∀y(r(x)=r(y) → x=y), 

/* Bootstrapping */
∀x∀y(Rxy ↔ Lr(x)r(y)), 

/* Connectedness */
∀x∀y(¬x=y → (Lyx ∨ Lxy))

/* Connectedness */
entails ∀x∀y(¬x=y → Ryx ∨ Rxy)

https://www.umsu.de/trees/#~6x~6y(r(x)=r(y)~5x=y),~6x~6y(Rxy~4Lr(x)r(y)),~6x~6y(~3x=y~5Lyx~2Lxy)

Here is a suggestion:

rep(X, Y-Z) :-
   term_factorized(X, Y, Z),
   numberassoc(Z, 0).

numberassoc([], _).
numberassoc(['$VAR'(N)=_|L], N) :-
   M is N+1, 
   numberassoc(L, M).

And then the comparator:

rep_compare(C, X, Y) :- 
   rep(X, A), rep(Y, B), 
   compare(C, A, B).

Any bugs? It requires that term_factorized/3 is stable and it works
only for terms that don’t have already ‘$VAR’/1 in it. Might need to
use something else, but with ‘$VAR’/1 rep/2 can be easily inspected.

4

Since term_factorized/3 gives me a stack overflow, had to revert to a
custom factorize/3. Its even a little bit faster than term_factorized/3
for the left recursive test case:

/* using term_factorized/3 */
?- X = X-0-9-5-4-2, Y = Y-7-5-2,
    time((between(1,10000,_), rep_compare(_,X,Y), fail; true)).
% 4,149,998 inferences, 0.313 CPU in 0.296 seconds (105% CPU, 13279994 Lips)

/* using factorize/3 */
?- X = X-0-9-5-4-2, Y = Y-7-5-2,
    time((between(1,10000,_), rep_compare(_,X,Y), fail; true)).
% 1,059,998 inferences, 0.125 CPU in 0.123 seconds (101% CPU, 8479984 Lips)

Source code of the new take:

rep2.p.log (2,2 KB)

6

Representation based comparison does seem to work well on everything I’ve tested, e.g., “Monkey test” for transitivity and anti-symmetry with repeat counts of 10,000,000.

A non-mathematical perspective: Representation based comparison requires the definition of a mapping predicate from any term to an acyclic equivalent such that the total order of the mapped terms is the same as the order of the original terms. These mapped terms can then be compared using standard ordering, i.e., compare/3 to define the order of the original terms.

The success of this approach depends on the definition of the mapping function. It has to ensure that the standard order of acyclic terms is respected. It also has to address the issues of transitivity and anti-symmetry with cyclic terms that cause issues with the current compare/3. @j4n_bur53’s naish/2 seems to nicely meet both of these requirements but it is not the only one so, subject to some level of standardization, it’s an implementation dependent solution. But a pretty good one IMO.

Note that since lexical ordering of cyclic terms is undecidable, different mapping functions may order cyclic terms differently. But this shouldn’t cause a problem if the ordering is only locally significant, i.e., defined by the same mapping predicate.