How to compare/3 without surprises on non-ground terms?

Help!
47

Notably for sort/2. Sorting does rely on transitivity (depending on the algorithm) and if this is not guaranteed, also terms that can be compared reliably may end up out of order. My intuition tells me that when sorting a list that holds some terms for which the order cannot be decided we can no longer guarantee that all duplicates are removed. I.e., setof/3 is broken if such terms are in the result set.

Now I do not know how serious this is. The undecidability seems to be relevant to only a subset of the cyclic terms (could this be defined?) and cyclic terms are anyway rather rare in Prolog. Still, AFAIK, most Prolog implementations simply crash on them (there was a survey some years ago). I’ve only seen a couple of cases where they really made sense.

48

As for the original comparable/3, it was strange for me why it didn’t work for a certain cases. I suspeted that codes using append/3 is the cause of looping. So I rewrote the comparable so that it does not extend lists arguments by append, which is suggested by the Konig lemma for termination of the comarable for cycic terms (infinite trees).

Fortunately, as far as I have tested, queries posted in this thread have been passed. Moreover, this version returns multiple outputs, which seems verifiable
with the striking comments posted by J.Burse, though
I am not familiar with order relation over cyclic terms.

Anyway, this version is at most a proto-type, which is far and far from final solution.

% ?- X=f(X,a(X)), Y=f(Y,b(Y)), Z=f(Y,c(Y)),
%    lazy_compare(A,X,Y), lazy_compare(B,Y,Z), lazy_compare(C,X,Z).
%@ X = f(X, a(X)),
%@ Y = f(Y, b(Y)),
%@ Z = f(Y, c(Y)),
%@ A = B, B = C, C = (<) ;
%@ X = f(X, a(X)),
%@ Y = f(Y, b(Y)),
%@ Z = f(Y, c(Y)),
%@ A = B, B = (<),
%@ C = (>) ;
%@ X = f(X, a(X)),
%@ Y = f(Y, b(Y)),
%@ Z = f(Y, c(Y)),
%@ A = (>),
%@ B = C, C = (<) ;
%@ X = f(X, a(X)),
%@ Y = f(Y, b(Y)),
%@ Z = f(Y, c(Y)),
%@ A = C, C = (>),
%@ B = (<).

qassoc(A-B, [C-D|_]):- A == C, !, B = D.
qassoc(H, [_|R]):- qassoc(H, R).
%
lazy_compare(C, X, Y) :-
	(	C == =	-> X = Y
	;	X == Y	-> C = (=)
	;	when((ground(X), ground(Y)), compare_ground(C, X, Y, []))
	).
%
compare_ground(C, X, Y, P):-
	( 	X == Y -> C = (=)
	;	(atomic(X); atomic(Y)) -> compare(C, X, Y)
	;	memberchk(p(X, Y)-D, P) ->
		C = D,
		member(C, [<,>])
	;	functor(X, F, N),
		functor(Y, G, M),
		compare(D, N, M),
		(	D == (=) ->
			compare(E, F, G),
			(	E == (=) ->
				X=..[_|Xs],
				Y=..[_|Ys],
				compare_ground_list(C, Xs, Ys, [p(X, Y)-C|P])
			;	C = E
			)
		;	C = D
		)
	).
%
compare_ground_list(C, [], [], _):-!, C = (=).
compare_ground_list(C, [X|Xs], [Y|Ys], P):-compare_ground(D, X, Y, P),
	(	var(D)	->	member(C, [<, >])
	;	D = (=) ->	compare_ground_list(C, Xs, Ys, P)
	;	C = D
	).
49

Move the Xs to be the first argument, to take advantage of first-argument indexing on [] vs [X|Xs].

50

I believe equivalence is decidable, so duplicate removal should be guaranteed. However, as the Carllson example demonstrated, the order of unequal acyclic terms is undecidable in general, although, if supported, it should be repeatable for any given implementation. Personally, I don’t think this is very serious but…

Perhaps usage in Prolog is rare (as is Prolog usage in general), but while they’re not often subject to decomposition/comparison in the sense we’ve been discussing, they’re essentially graphs which, like acyclic trees, are not an uncommon data structure in computer science. Graphs essentially require direct references rather than some additional addressing/lookup scheme (facts, lists, dictionaries, global vars,…).

A concrete example: any clpBNR constraint network is one big cyclic term; each attributed interval variable provides a “handle” to it. I never want to deal with it in its entirety, i.e., print it or walk it, but it’s indispensable for efficient constraint propagation and “tidy” code.

And I haven’t done or seen any survey but I’d hazard a guess that they are supported to various degrees on most modern Prolog implementations: Sicstus, YAP, SWIP, Scryer, …

51

I believe the predicate canonical_term/2 described in the paper can be implemented in SWIP using term_factorized/3:

canonical_term(Term, Canonical) :-
	terms:term_factorized(Term, Canonical, Subs),
	assoc:maplist(call, Subs).

Now,

?- A = s(s(s(A))).
A = s(s(s(A))).

?- A = s(s(s(A))), canonical_term(A,C).
A = C, C = s(C).

?- A=s(B,0), B=s(A,1), canonical_term(A,AC), canonical_term(B,BC).
A = AC, AC = s(s(AC, 1), 0),
B = BC, BC = s(s(BC, 0), 1).

I guess it’s an open discussion as to what the top level should do.

52

No, but I don’t think that’s what happens, at least not on SWIP:

?- A = s(s(s(A))), B=s(s(B)).
A = B, B = s(s(B)).

and (with Naish’s @N syntax replaced by '\a'(N))

?- A = s(s(s(A))), B=s(s(B)), acyclic_rep(A,ARep), acyclic_rep(B,BRep).
A = B, B = s(s(B)),
ARep = BRep, BRep = s('\a'(1)).

?- A = s(s(s(A))), B=s(s(B)), comparable(Op,A,B).
A = B, B = s(s(B)),
Op = (=).

And as term_factorized generates the minimal form, acyclic_rep (newly renamed) using Carllson’s example:

?- A=s(B,0), B=s(A,1), acyclic_rep(A,ARep), acyclic_rep(B,BRep).
A = s(s(A, 1), 0),
B = s(A, 1),
ARep = s(s('\a'(2), 1), 0),
BRep = s(s('\a'(2), 0), 1).

I think it does work; no?

Rightly or wrongly, it seems to explain the following:

?- A=s(B,0), B=s(A,1), comparable(Op,A,B).
A = s(s(A, 1), 0),
B = s(A, 1),
Op = (>).

Maybe the Op is < or > depending on whether the implementation chooses to “rewrite” the B in A or the A in B.

54

But that’s not the paper you originally referenced (MANTADELIS et al.). Using the code from that paper, “Alg. 2: Predicate canonical_term/2” on page 11.

?- _A = [a|_A], canonical_term(_A, Print).
_A = Print, Print = [a|Print].

From the text:

To reconstruct each cyclic subterm as acyclic, the algorithm copies the unique parts of the term and introduces an unbound variable instead of the cyclic references.

That’s different from acyclic_rep which does use Naish-like notation (required for comparable/3 as described previously):

?- _A = [a|_A], acyclic_rep(_A,Print).
_A = [a|_A],
Print = [a|'\a'(1)].
Code from MANTADELIS et al. 
canonical_term(Term, Canonical) :-
	Term =.. InList,
	decompose_cyclic_term(Term, InList, OutList, OpenEnd, [Term]),
	Canonical =.. OutList,
	Canonical = OpenEnd.
	
decompose_cyclic_term(_CyclicTerm, [], [], _OpenEnd, _Stack) :- !.
decompose_cyclic_term(CyclicTerm, [Term|Tail], [Term|NewTail], OpenEnd, Stack) :-
	acyclic_term(Term), !,
	decompose_cyclic_term(CyclicTerm, Tail, NewTail, OpenEnd, Stack).
decompose_cyclic_term(CyclicTerm,[Term|Tail],[OpenEnd|NewTail],OpenEnd,Stack) :-
	CyclicTerm == Term, !,
	decompose_cyclic_term(CyclicTerm, Tail, NewTail, OpenEnd, Stack).
decompose_cyclic_term(CyclicTerm,[Term|Tail],[Canonical|NewTail],OpenEnd,Stack) :-
	\+ in_stack(Term, Stack), !,
	Term =.. InList,
	decompose_cyclic_term(Term, InList, OutList, OpenEnd2, [Term|Stack]),
	Canonical =.. OutList,
	( Canonical = OpenEnd2,
	  Canonical == Term,
	  !
	; OpenEnd2 = OpenEnd
	),
	decompose_cyclic_term(CyclicTerm, Tail, NewTail, OpenEnd, Stack).
decompose_cyclic_term(CyclicTerm,[_Term|Tail],[OpenEnd|NewTail],OpenEnd,Stack) :-
	decompose_cyclic_term(CyclicTerm, Tail, NewTail, OpenEnd, Stack).
	
in_stack(E, [H|_]) :- E == H.
in_stack(E, [_|T]) :- in_stack(E, T).
56

Let S be a signature with a linear order (like functors with arity in Prolog), and
(H, <) the Herbrand Univers with the standard total order (like @< in Prolog).

It is well known that (H, <) is defined as the minimum fixpoint of
an appropriate monotone operation F on sets (like terms in Prolog).
Usually (H, <) is defined by structual INDUCTION.

Assuming a non-well-found sets, for the same operation F, also there
exists the largest fixpoint, say (H’,<‘),
which is, I think, a well-known standard fact.
As H’ is non-well-founded, the maximal fixpoint (H’, <') is not obtained
by the induction but by co-induction.

The example MC x=f(y, 0), y=f(x, 1) shows that
the relation <’ violates the transitive law.

Before you informed us on MC (Mats Carlsson) example, I took without thought or evidence that <’ inherits the property of total ordering from <,
but MC tells that it is not the case.

Now that cyclic terms lost order, I simply doubt in that compare/3 takes care of cyclic terms.

I am writing this short comment based on what I learned about 30~40 years ago.
I forgot technical details. I may be missing something.

Thanks again for quite interesting information.

57

I guess the bottom line is that, like compare/3, canonical_term/2 might require variations to suit a purpose. What’s need for printing mightn’t be what’s needed for comparison.

I have implemented a version of acyclic_rep/2 using terms:term_factorized/3 provided with SWIP (as discussed in both those papers), and you’re right it isn’t cheap. Profiling an implementation using your original example shows that 80% or more of the time is spent creating a “canonical” acyclic equivalent representation that can be compared. Current code below.

Module `comparable` 
:- module(comparable, [comparable/3, acyclic_rep/2]).
	
comparable(Op,X,Y) :- Op == =, !,                     % Op = =, unify X and Y
	X = Y.
comparable(=,X,Y) :- X == Y, !.                       % X and Y identical, Op = =
comparable(Op,X,Y) :- compound(X), compound(Y), !,    % comparing two unequal compound terms
	((cyclic_term(X), cyclic_term(Y))                 % if both cyclic
	 -> acyclic_rep(X,XRep), acyclic_rep(Y,YRep)      % then use pseudo equivalent acyclic terms
	 ;  XRep = X, YRep = Y                            % else just use original form
	),
	functor(XRep,_,XA), functor(YRep,_,YA),
	compare(FOp,XA,YA),           % compare arities, as per standard order
	( (FOp == =)
	 -> XRep =.. FX, YRep =.. FY, % arities equal, 	    
	    comparableArgs(FX,FY,Op)  % lists are same length
	 ;  Op = FOp                  % arities unequal
	).
comparable(Op,X,Y) :- nonvar(X), nonvar(Y), !,        % comparing two other nonvars
	compare(Op,X,Y).              % standard compare
comparable(Op,X,Y) :-                                 % else X and/or Y are vars
	when((nonvar(X),nonvar(Y)), comparable(Op,X,Y)).  % defer
	
comparableArgs([X],[Y],Op) :- !,
	comparable(Op,X,Y).
comparableArgs([X|XArgs],[Y|YArgs],Op) :-
	comparable(IOp,X,Y),
	(nonvar(IOp)  % is arg compare Op defined?
	 -> comparableArg(IOp,Op,XArgs,YArgs)                     % yes, test
	 ;  when(nonvar(IOp), comparableArg(IOp,Op,XArgs,YArgs))  % no, defer
	).

% arg compare Op defined, continue if =, else exit
comparableArg(IOp,Op,XArgs,YArgs) :-
	(IOp = =) -> comparableArgs(XArgs,YArgs,Op) ; Op = IOp. 

% Create an acyclic representation for a rational tree (cyclic term) using 
% L. Naish "pointers", which can be used as a substitute for comparison purposes.
acyclic_rep(Term,Rep) :-
	terms:term_factorized(Term,Rep,Subs),
	make_acyclic_rep(Subs).
	
make_acyclic_rep([]).
make_acyclic_rep([V = ExpIn|Subs]) :-
	acyclic_subs(0,V,ExpIn,ExpOut),
	V = ExpOut,
	make_acyclic_rep(Subs).
	
acyclic_subs(Lvl,V,X,'\a'(Lvl)) :- var(X), V==X, !.   % Naish's @N ==> '\a'(N)
acyclic_subs(Lvl,V,TermIn,TermOut) :- compound(TermIn), !,
	NxtLvl is Lvl+1,
	terms:mapargs(comparable:acyclic_subs(NxtLvl,V),TermIn,TermOut).
acyclic_subs(_Lvl,_V,Term,Term).
58

I wouldn’t take it that far. For example, Carllson doesn’t claim that cyclic term equivalence is undecidable, only that ordering unequal cyclic terms is undecidable.

Given that it is undecidable, I find it hard to imagine an application that depends on such an ordering. So isn’t it sufficient (and useful?) to say the ordering is arbitrary, but fixed and repeatable for a given application?

I think the Sicstus documentation expresses the semantics fairly well:

And I would point out that there are cyclic terms where the order relation does hold:

?- X=f(1,X), Y=f(2,Y), compare(C,X,Y).
X = f(1, X),
Y = f(2, Y),
C = (<).

As Carllson also points out there is an analogy with arithmetic on infinities; you just have to be aware of the limitations in the context of your application.

59

If remember correctly, cyclic term equivalence is decidable like that for regular expressions.
I take it rather that what Carlson showed is that order (transitive and anti-symmetric) does not exist for the cyclic terms, which is still striking for me.

Of course I can imagine situations where cyclic terms comparison is useful, like for use in predsorting.

60

In the sense that you can deduplicate, yes. The trivial O(n^2) algorithm works as expected. Deduplication in e.g. setof/3 uses sort/2 though. This is O(n*log(n)) and relies on transitivity of comparison. If that is not guaranteed, I fear that equivalent terms may not end up as neighbors and the final deduplication pass that compares all neighbors is not guaranteed to work as expected. Would be nice if someone can proof this reasoning is incorrect.

62

Of course I agree. It sounds quite natural that there is a well-ordering over the (cyclic) terms which is not the lexical ordering.

63

So isn’t this a solution, i.e., define a “standard order” of unequal cyclic terms based on the comparison of their (acyclic) canonical form? One example of a canonical form is that suggested by Lee Naish, e.g., X=f(X) <=> f(@1). I think an order based on the canonical form has the necessary properties to be used for sorting and setof.

66

I mean the well-known thing that any set ( for example, even the set of real numbers) is well-ordered
assuming Axiom of choice. So I thought it is not surprising that some clever persons find
well-ordering for the set of possibly cyclic terms.

By the way, I learned in this thread that SWI-Prolog can facterise terms, which is a colalgera
of a given signature ( flat solved form of A. Colmerauer). This means that it is easy for SWIPL to
calculate the maximal bisimulation over the domain of the coalgebra, which almost gives decision of ordering. This is what I had rough idea in mind.

68

This seems equivalent to say that rational trees is a coalgebra whose domain is finite.

70

I agree. In fact infinite many variables necessary for the flat solved form (coalgebra)
to represent the tree (3).

72

Your intuition that term_factorezed/2is a key to comparable/3 seems right.
The maximal bisimulation for the term_facotrized (=coalgebra) is straightforward by prolog unification
between prolog variables. Then, the order <, =, > between given two terms is fairy easy from the the result of unifcation with the given coalgebra, and seems not too bad in efficiency.

74

No. I said too much. I meant non-lexical comparison, which is a revision of my lazy_compare/3 posted.
Anyway I might have to write prototype codes which uses term_factorized (=coalgebra) for test.
It would take a few days for me, but others would do it in half hour.
I wiil post immediately when I encounter unexpected things.

76

Hi Jan,

There is no mention to cyclic terms in the manual help(compare). Is it intentional, or
in fact there is nothing problematic for ground terms including cyclic ones.

I have tested compare/3 and sort/2 on some ground terms including cyclic ones
including X=f(Y,0), Y=f(X, 1). As far as my testing every case works as expected.

Although I know I am asking a strange question, what is a problem on compare/3 ?