Fixing the compare/3 mirror anomaly in SWI-Prolog?

General
1

I was too optimistic about the native compare/3. It has also the
mirror anomaly. I find very quickly a violation of the mirror law:

/* SWI-Prolog 9.1.7 */
?- repeat, random_cyclic(A), random_cyclic(B), 
compare(X,A,B), X = (<), \+ (compare(Y,B,A), Y = (>)).
A = s(A, A),
B = s(_S1, 1), % where
    _S1 = s(_S1, s(1, _S1)),
X = (<) .

Its indeed a violation of this law:

It can be reproduced on the top-level:

/* SWI-Prolog 9.1.7 */
?- A = s(A, A),
B = s(_S1, 1), % where
_S1 = s(_S1, s(1, _S1)), compare(X,A,B), compare(Y,B,A).
%%% answer
X = Y, Y = (<).

This could explain why the native compare/3 has transitivity violations?
But where does the SWI-Prolog implementation make a decision,
which violates the mirror law?

Edit 05.04.2023
Interestingly Scryer-Prolog doesn’t have the mirror anomaly. I neverthless
found somewhere a transitivity violation, but the mirror anomaly seems not
to be there. So there is no guarantee if the mirror anomaly is fixed, that

the native compare/3 works correctly. But for the mirror anomaly here the
same in Scryer Prolog, it doesn’t yield anything:

/* Scryer-Prolog 0.9.1-218 */
?- repeat, random_cyclic(A), random_cyclic(B),
compare(X,A,B), X = (<), \+ (compare(Y,B,A), Y = (>)).
%%% runs and runs and runs

Was using the below fuzzer version. This fuzzer only generates ground
cyclic terms. So the mirror law is violated by two ground terms. Couldn’t
find a violation yet in Scryer-Prolog though.

fuzzer_20230405.p.log (1,7 KB)

3

Assuming mirror anomaly means anti_symmetricity,
IMO, transitivity is not problem because in general, binary relation becomes transitive by taking
simply transitive closure. The origin of problem seems mirror anomaly, which requires
detecting closed paths of comparing. Using your random-cyclic and generating
anomaly triples of terms which violates transitivity I often observed something long closed paths, which discouraged me to find new compare/3 to sort list of cyclic terms. I feel I am getting
into negative to apply compare on rational trees.

I am not familiar with the state of art of comparing rational terms in other languages.

EDIT.

For the first time for me, I have tried a little bit to generate a universe of rational trees without mirror anomaly by trying to find operations which transform binary relations to mirror-anomaly-free ones.
However any of them seems not monotone increasing because of including set-minus operations.
As a very personal feeling, still I am pessimistic to find a “constructive” universe of mirror-anomaly-free universe of rational trees.

5

@kuniaki.mukai did you study @ridgeworks proposal already or what considers
your research in an universe of rational trees equipped with compare/3? Basically
this would be structure, since compare/3 can be bootstrapped from (@<)/2:

/* Structure Signature */
<R, (==)/2, (@<)/2>

Maybe people are not aware, that @ridgeworks proposal of representation
based comparison is a total order. It only violates lexical ordering, but total order
laws will obviously not be violated.

What are total order laws (not violated by all terms):

  • Not A @< A (irreflexiv)
  • If A @< B then not B @< A (asymmetric)
  • if A @< B and B @< C then A @< C (transitive)
  • if not A == B, then A @< B or B @< A (connected)

What is lexical ordering (violated by some cyclic terms):

  • (A,B) @< (C,D) iff A @< C or (A ==C and B @< D) (lexical)
6

It was out of my sight, but it is good news that he found a solution to mirror anomaly problem
loosening lexical order.

8

That was exactly what I was thinking. I came to this. Just finished 100M tests in 5 minutes. It can be optimized
a bit further, but it is mostly a demonstrator that can be used as basis for an implementation in the core.

rep_compare(C, X, Y) :-
    rep_compare(C, X, [], Y, []).

rep_compare(C, X, SX, Y, SY), compound(X), compound(Y) =>
    naish_lookup(X, SX, X2, Flag),
    naish_lookup(Y, SY, Y2, Flag),
    (   Flag == true
    ->  compare(C, X2, Y2)
    ;   compound_name_arity(X, NX, AX),
        compound_name_arity(Y, NY, AY),
        (   NX == NY, AX == AY
        ->  compare_args(C, 1, AX, X, [X|SX], Y, [Y|SY])
        ;   compare(C, AX-NX, AY-NY)
        )
    ).
rep_compare(C, X, _, Y, _) =>
    compare(C, X, Y).

compare_args(C, I, Arity, X, SX, Y, SY), I =< Arity =>
    arg(I, X, AX),
    arg(I, Y, AY),
    rep_compare(C0, AX, SX, AY, SY),
    (   C0 == (=)
    ->  I1 is I+1,
        compare_args(C, I1, Arity, X, SX, Y, SY)
    ;   C = C0
    ).
compare_args(C, _I, _Arity, _X, _SX, _Y, _SY) =>
    C = (=).

naish_lookup(Term, Stack, Naish, true) :-
    nth1(N, Stack, Term2),
    Term2 == Term,
    !,
    Naish = N.
naish_lookup(Term, _, Term, _).

With test code like this (should check transitivity as well).

test(N, Pred) :-
    N > 0,
    !,
    (   N mod 10000 =:= 0
    ->  format(user_error, '\r~t~D~20|', [N])
    ;   true
    ),
    random_cyclic(X),
    random_cyclic(Y),
    call(Pred, C1, X, Y),
    call(Pred, C2, Y, X),
    (   consistent(C1, C2)
    ->  N2 is N - 1,
        test(N2, Pred)
    ;   format(user_error, 'FAILED:~n\t~q~n\t~q~n', [X, Y])
    ).
test(_, _).

consistent(=, =).
consistent(<, >).
consistent(>, <).

% random_cyclic(-Term)
random_cyclic(T) :-
   random_cyclic([T], T).

% random_cyclic(+List, -Term)
random_cyclic(L, T) :-
   length(L, M),
   random(R),
   N is truncate(R*(M+3)),
   (   N = 0
   ->  T = 0
   ;   N = 1
   ->  T = 1
   ;   N = 2
   ->  T = s(P,Q),
       random_cyclic([P|L], P),
       random_cyclic([Q|L], Q)
   ;   K is N-3,
       nth0(K, L, S),
       S = T
   ).
1 Like
10

Congratulation for definitive implementation on comparing cyclic terms. Below
is a monkey test for transitivity of the compare predicate rep_compare/3, which
is after your codes on totality of the predicate.

Although it might be too late to ask a question, is there any article on verification of the algorithm ? I searched for such paper on the net, but failed. I tried to prove the transitivity for myself from scratch, but I could not fill a gap in my “proof”. Thank you in advance.

% ?- transitive_monkey(10000000, rep_compare).
transitive_monkey(N, Pred) :-
    N > 0,
    !,
    (   N mod 10000 =:= 0
    ->  format(user_error, '\r~t~D~20|', [N])
    ;   true
    ),
    random_cyclic(X),
    random_cyclic(Y),
    random_cyclic(Z),
    call(Pred, C1, X, Y),
    call(Pred, C2, Y, Z),
	call(Pred, C3, X, Z),
    (   transitive_consistent(C1, C2, C3)
    ->  N2 is N - 1,
        transitive_monkey(N2, Pred)
    ;   format(user_error, 'FAILED:~n\t~q~n\t~q~n\t~q~n', [X, Y, Z])
    ).
transitive_monkey(_, _).
%
transitive_consistent(C1, C2, C3):-
	(	transitive(C1, C2, D) -> C3 = D
	;	true
	).
%
transitive(=, =, =).
transitive(=, <, <).
transitive(=, >, >).
transitive(>, =, >).
transitive(<, =, <).
transitive(>, =, >).
transitive(<, <, <).
transitive(>, >, >).