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

[ridgeworks]

@anon95304481

Now using the new counter example. The key X is such that it mimics
a pair, confusing acyclic_rep/2 inside new_compare/2.

Just to confirm your example:

?- X=(X-b(X)), predsort(comparable,[X-b(X), X-a(X)], L).
X = X-b(X),
L = [X-b(X), X-a(X)].

?- X=(X-b(X)), predsort(comparable,[b(X), a(X)], L).
X = X-b(X),
L = [a(X), b(X)].

@anon95304481

It breaks the ascending order property:

Or is it an issue with the top level output. X = X-b(x) so L in the first query is equivalent to [X, X-a(X)]; is the ascending order property broken?

Is this an equivalent query:

?- X=(X-b(X)), predsort(comparable,[X, X-a(X)], L).
X = X-b(X),
L = [X-b(X), X-a(X)].

And if X isn’t one of the list members:

?- X=(X-b(X)), predsort(comparable,[X-c(X), X-a(X)], L).
X = X-b(X),
L = [X-a(X), X-c(X)].

?- X=(X+b(X)), predsort(comparable,[X-b(X), X-a(X)], L).
X = X+b(X),
L = [X-a(X), X-b(X)].

[ridgeworks]

@anon95304481

if you are not sure whats going on, you can use sorted/1,
it was defined here. If it fails, there is anyway no output. You
might want to replace (@<)/2 by new_compare/3 with C=(<).

Yes, since you’ve exposed a problem using SWIP’s term compare, my version of sorted/1 uses comparable/3:

?- X=(X-b(X)), predsort(comparable,[X-b(X), X-a(X)], L), sorted(L).
X = X-b(X),
L = [X-b(X), X-a(X)].

?- X=(X-b(X)), predsort(comparable,[X-a(X), X-b(X)], L), sorted(L).
X = X-b(X),
L = [X-b(X), X-a(X)].

@anon95304481

Combine it with library(pairs), the pairs_values/2 predicate,
I get the following unexpected result, since there is only one key,

Using X=X-b(X) as a key and an element in a list to be key-sorted is a bit beyond my abstract thinking capability. (Why would you choose ‘-’ as the functor for this term?) But I guess it is unexpected; to what extent is it a problem?

[Boris]

At least to me the two cyclic terms X = [a,b|X] and Y = [b,a|Y] look identical. It is an arbitrary choice where you choose to start writing them down. I am trying to say that cyclic terms are comparable syntactically (maybe, in the source code) but definitely not structurally (or as they are represented in the machine), unless we want to use accidental properties like how it was written or where in memory it resides.

None of what I wrote is rigorous enough to be taken seriously.

[kuniaki.mukai]

This is all what I think I know about extending order @< onto rational trees. Also I attach codes compare_roughly/3 and queries on predsort for around Matt Carlson’s example.
(compare_roughly should be named useless_compare. )

First, definition of the extension of @< written < for simplicity. Let R be the set of rational trees,
and H is the set of Herbrand terms (H\subset R). (H, <) is the standard totally ordered set. Note that (H, <) is defined inductively.

Let F be an operation on relations on R.

F(P) = \{(U, V) \mid \mbox{ $U$ lexically goes before $V$ wrt $P$}\},

where U=f(a_1,\ldots, a_n) lexically goes before V=g(b_1, \ldots, b_m) wrt P
when one of the conditions holds.

• n<m
• n=m, f lexicallly goes before g
• n=m, f=g, for some k\leq n,
  a_i = b_i ( i < k) and (a_k, b_k) \in P.

As F is clealy monotone there is the largest fixpoint Q of F.
Q=F(Q). Clearly Q is an extension of @< on H. However,
Carlson’s example is a counter example against that Q is order (reflexive, transitive, anti-symmetric).
Q seems complex, at least for me, more than it looks simple as for the definition. It seems to
interesting to investigate Q, but also far beyond me

Before dropping out of this thread, I have written codes compare_roughly/3, which uses ==/2, cyclic_term/1, compare/3 for limited case, and somewhat ad hoc limit of depths.

% ?- A=f(A, 0), B=f(B, 1), compare_roughly(R, A, B).
%@ A = f(A, 0),
%@ B = f(B, 1),
%@ R = (<).
% ?- A=f(A, 0), B=f(B, 1), C=f(C, 2), predsort(compare_roughly, [A, B, C], R).
%@ A = f(A, 0),
%@ B = f(B, 1),
%@ C = f(C, 2),
%@ R = [f(A, 0), f(B, 1), f(C, 2)].
% ?- A=f(A, 0), B=f(B, 1), C=f(C, 2), predsort(compare_roughly, [A, B, A, B, C, A], R).
%@ A = f(A, 0),
%@ B = f(B, 1),
%@ C = f(C, 2),
%@ R = [f(A, 0), f(B, 1), f(C, 2)].

compare_roughly(C, X, Y):- compare_roughly(10, C, X, Y).  % default depth = 10.
%
compare_roughly(_, =, X, Y):- X == Y, !.
compare_roughly(N, C, _, _):- N<0, !, C = (=).
compare_roughly(N, C, X, Y):- compare_cyclic_terms_with_depth_limit(N, C, X, Y), !.
compare_roughly(_, C, X, Y):- compare(C, X, Y).

%
compare_cyclic_terms_with_depth_limit(N, C, X, Y):- cyclic_term(X),
		cyclic_term(Y),
		functor(X, F, I),
		functor(Y, G, J),
		compare(D, I, J),
		(	D = (=) ->
			compare(E, F, G),
			(	E = (=) ->
				X=..[_|As],
				Y=..[_|Bs],
				N0 is N-1,
				compare_list(N0, C, As, Bs)
			;	C = E
			)
		;	C = D
		).

%
compare_list(_, =, [], []).
compare_list(N, C, [A|As], [B|Bs]):- A == B, !, compare_list(N, C, As, Bs).
compare_list(N, C, [A|As], [B|Bs]):- compare_roughly(N, D, A, B),
	(	D = (=) ->
		compare_list(N, C, As, Bs)
	;	C = D
	).

[kuniaki.mukai]

Dict was out of my thought. I am not sure on dict syntax.

[jan]

As is, dicts are just compound terms with a non-atom functor. All you need to do is to give this functor a place among the atoms. Actually, ordering blobs (the super type of atoms) is defined.

[kuniaki.mukai]

@anon95304481

A = _{bar:B,baz:0}, B = _{bar:A,baz:1}, compare(X, A, B).

@jan

As is, dicts are just compound terms with a non-atom functor. All you need to do is to give this functor a place among the atoms. Actually, ordering blobs (the super type of atoms) is defined.

I have checked that compare_roughly works also for @anon95304481 dict sampl, though I understand only half of your comments. Anyway, as I used basically what SWI-Prolog provides with my minior limited use of them for not going looping, it is quite natural it works so.

% ?- A = _{bar:B,baz:0}, B = _{bar:A,baz:1}, compare_roughly(X, A, B).
%@ A = _{bar:_A{bar:A, baz:1}, baz:0},
%@ B = _A{bar:A, baz:1},
%@ X = (<).

Unfortunately, despite of useful information flowing in this thread, still I am unclear about spcification of limited but useufl lexical ordering on rational trees. Maybe I am lazy for digesting new things.

[ridgeworks]

@Boris

At least to me the two cyclic terms X = [a,b|X] and Y = [b,a|Y] look identical. It is an arbitrary choice where you choose to start writing them down. I am trying to say that cyclic terms are comparable syntactically (maybe, in the source code) but definitely not structurally (or as they are represented in the machine), unless we want to use accidental properties like how it was written or where in memory it resides.

Not sure why you think they look identical. Rational trees (cyclic terms) are still trees and they have roots. In this case the roots are different [a|_] for X and [b|_] for Y.

From another perspective: would you say X=[a,b|TX] and Y=[b,a|TY] look identical? Does subsequent unification (X=TX and Y=TY) change that?

[brebs]

@anon95304481

X=[a,b|X]

That’s an invalid construct, due to the cyclic term X, so… why is it discussed?

I get the feeling I’m missing something obvious

[kuniaki.mukai]

Google search for “rational tree” returns 61,800,000 hits. It is used to represent
directed graph with cycles, stream, perpetual process, …

[Boris]

Yes, so the only thing that is different is where your handle is, at some given moment. But it doesn’t have a root since it is a cycle.

In the same vein, I understand perfectly well that under some interpretation, X = [a|X] and Y = [a,a|Y] are different terms. But length/2 refuses to tell me how “big” or “deep” they are and for any predicate that needs to iterate through the list they are defacto identical. Try member/2, for example.

And I have no idea what sort/2 is doing check this out:

?- X = [a|X], Y = [a,a|Y], sort([X,Y], Sorted).
X = Y, Y = [a, a|Y],
Sorted = [_S1], % where
    _S1 = [a|_S1].

?- X = [a,a|X], Y = [a|Y], sort([X,Y], Sorted).
X = Y, Y = [a|Y],
Sorted = [_S1], % where
    _S1 = [a, a|_S1].

?- X = [a|X], Y = [a,a|Y], sort([Y,X], Sorted).
X = Y, Y = [a, a|Y],
Sorted = [[a, a|Y]].

?- X = [a,a|X], Y = [a|Y], sort([Y,X], Sorted).
X = Y, Y = [a|Y],
Sorted = [[a|Y]].

EDIT
Ok I think I see now, the difference between the first two and the last two queries is again something about how the top-level reports it, most probably.

no in fact I have no idea what this means.

EDIT2

Hmm… so contrary to my expectations sort/2 seems to attempt to do something like unification? Because:

?- X = [a|X], Y = [a,a|Y], X = Y.
X = Y, Y = [a, a|Y].

?- X = [a,a|X], Y = [a|Y], X = Y.
X = Y, Y = [a|Y].

In other words, I take back everything I said, those two cyclic terms are clearly unifiable so they are indeed the same term. Not sure which one but since they are the same it doesn’t matter. Case closed, sorry for the noise.

Last EDIT I promise they also compare equal, not sure what decides how the answer is printed, with one or two "a"s.

?- X = [a|X], Y = [a,a|Y], compare(Order, X, Y).
X = Y, Y = [a, a|Y],
Order = (=).

?- X = [a,a|X], Y = [a|Y], compare(Order, X, Y).
X = Y, Y = [a|Y],
Order = (=).

[ridgeworks]

@brebs

That’s an invalid construct, due to the cyclic term X, so… why is it discussed?

I get the feeling I’m missing something obvious

Not invalid in most Prolog’s but varying degrees of support. A quote from a paper referenced earlier in this thread by @anon95304481:

From as early as (Colmerauer 1982; Jaffar and Stuckey 1986), Prolog implementers have chosen to omit the occurs check in unification. This has resulted in generating cyclic terms known as rational terms or rational trees in Prolog. While the introduction of cyclic terms in Prolog was unintentional, soon after applications for cyclic terms emerged in fields such as definite clause grammars (Colmerauer 1982; Giannesini and Cohen 1984), constraint programming (Meister and Frühwirth 2006; Bagnara et al. 2001) and coinduction (Gupta et al. 2007).

Perhaps a bit unfortunate that your original post concerning comparing non-ground terms got expanded to include comparing rational trees. But it does seem to have exposed a flaw in the current (standard order) compare/3.

[ridgeworks]

@Boris

Last EDIT I promise they also compare equal, not sure what decides how the answer is printed, with one or two "a"s.

IIRC printing them was the subject of two papers @anon95304481 referenced previously in this thread. I think there’s a minimal form but SWIP doesn’t enforce it for top level output.

I’ve written code which heavily depends on cyclic terms but I never try to compare, print or walk them, let alone assert or table them. Custom hooks (portray, attr_portray_hook and project_attributes) are used to minimize (not eliminate) their exposure to the “outside world”.

[kuniaki.mukai]

I have changed codes of compare_roughly/3. The new codes compare_with_stack/3,
which can be used instead of compare/3 for predsort for a list of ground possiby cyclic terms.
It is still experimental, but for now I am seeing high possiblity that it could give one of final solutions to what disscussed in this thread.

I appreciate for any comment. The codes is short and hopefully clear.

compare_with_stack/3 is actually 4 value version of compare, <, =, >, and unstable.

% ?- compare_with_stack(C, a, a).
%@ C = (=).
% ?- A=f(A), compare_with_stack(C, A, A).
%@ A = f(A),
%@ C = (=).
% ?- A=f(A), B=f(B), compare_with_stack(C, A, B).
%@ A = B, B = f(B),
%@ C = (=).
% ?- A=f(A,0), B=f(B,1), compare_with_stack(C, A, B).
%@ A = f(A, 0),
%@ B = f(B, 1),
%@ C = (<).
% ?- A=f(B,0), B=f(A,1), compare_with_stack(C, A, B).
%@ A = f(f(A, 1), 0),
%@ B = f(A, 1),
%@ C = (>).
% ?- A=f(B,0), B=f(A,1), compare_with_stack(C, B, A).
%@ A = f(f(A, 1), 0),
%@ B = f(A, 1),
%@ C = (<).
% ?- A=f(A, 0), B=f(B, 1), C=f(C, 2), predsort(compare_with_stack, [A, B, C], R).
%@ A = f(A, 0),
%@ B = f(B, 1),
%@ C = f(C, 2),
%@ R = [f(A, 0), f(B, 1), f(C, 2)].
% ?- A=f(A, 0), B=f(B, 1), C=f(C, 2), predsort(compare_with_stack, [A, B, A, B, C, A], R).
%@ A = f(A, 0),
%@ B = f(B, 1),
%@ C = f(C, 2),
%@ R = [f(A, 0), f(B, 1), f(C, 2)].
% ?- A = _{bar:B,baz:0}, B = _{bar:A,baz:1}, compare_with_stack(X, A, B).
%@ A = _S1, % where
%@     _S1 = _S1{bar:_S2, baz:0},
%@     _S2 = _S2{bar:_S1, baz:1},
%@ B = _S2{bar:_S1, baz:1},
%@ X = (>).
% ?- H = H-9-7-6-5-4-3-2-1-0, Z = H-9-7-6-5-4-3-2-1,
%     Y = Y-7-5-8-2-4-1, compare_with_stack(<, Z, Y).
%@ H = H-9-7-6-5-4-3-2-1-0,
%@ Z = H-9-7-6-5-4-3-2-1,
%@ Y = Y-7-5-8-2-4-1.
% ?- X = X-0-9-7-6-5-4-3-2-1, Y = Y-7-5-8-2-4-1, compare_with_stack(<, X, Y).
%@ X = X-0-9-7-6-5-4-3-2-1,
%@ Y = Y-7-5-8-2-4-1.
% ?- H = H-9-7-6-5-4-3-2-1-0, Z = H-9-7-6-5-4-3-2-1,
%     Y = Y-7-5-8-2-4-1, compare_with_stack(<, Z, Y).
%@ H = H-9-7-6-5-4-3-2-1-0,
%@ Z = H-9-7-6-5-4-3-2-1,
%@ Y = Y-7-5-8-2-4-1.

compare_with_stack(C, X, Y):- compare_with_stack(C, X, Y, []).
%
compare_with_stack(C, X, Y, P):-
	( 	X == Y -> C = (=)
	;	(atomic(X); atomic(Y)) -> compare(C, X, Y)
	;	memberchk(X-Y, P) -> C=(=)
	;	functor(X, F, N),
		functor(Y, G, M),
		compare(D, N, M),
		(	D == (=) ->
			compare(E, F, G),
			(	E == (=) ->
				X=..[_|Xs],
				Y=..[_|Ys],
				compare_with_stack_list(C, Xs, Ys, [X-Y|P])
			;	C = E
			)
		;	C = D
		)
	).
%
compare_with_stack_list(C, [], [], _):-!, C = (=).
compare_with_stack_list(C, [X|Xs], [Y|Ys], P):-
	compare_with_stack(D, X, Y, P),
	(	D = (=) ->	compare_with_stack_list(C, Xs, Ys, P)
	;	C = D
	).

[jan]

@Boris

Last EDIT I promise they also compare equal, not sure what decides how the answer is printed, with one or two "a"s.

The toplevel finds variable that have the same value (==), and as X = [a|X] and Y = [a,a|Y] are the same terms, it will print X = Y and print more or less randomly ether X or Y. The toplevel printing for a single term factorizes the term if it is cyclic, but on the internal structure rather than by finding equivalent subterms. In other words, it prints the physical cycle in memory rather than the logical one.

[kuniaki.mukai]

@anon95304481

But you seem to prefer thinking in terms of an operator than in terms of an axiom.

I think I am far from saying something difficult more than written
in Lloyd book on foundation of logic programming.

BTW, my lesson on the operator F teachs me that although F is simple and expected useful
to define some lexical order on rational trees, the largest fixpoint F contains
Matts Carllson’s pair, which is not good I think. Maybe F is too simple.
I am revising F so that largest fixpoint is semi-lexcical total order on rational trees, of course without
the Matt Carllson’s pairs. I am afraid that a revised F would look similar to my codes compare_with_stack (sigh)

I am looking forward to see someone would propose relevant smart operators, or, anything else
to manage lexcai order on cyclic terms.

[kuniaki.mukai]

@anon95304481

Its impossible, this was shown by Matt Carlssons counter example.

Of course, its impossible. So far, no one seems against.

However, fortunately for rational terms it is decidable whether they are comparable in the sense of lexical order or not. I think, with a little change, comapare_with_stack could be such a decision predicate.
Giving order between two incomparable terms in a conservative way, it could be used
to sort lists (sort only locally coherent ). comapare_with_stack together with semi_lex_sort are for such direction, which was pushed by accepting Matt Carllson’s pairs positively.

[kuniaki.mukai]

@anon95304481

What is the specification of compare_with_stack/3?

Change compare_with_stack/3 to return ‘incomparable’ when
given terms are incomparable.

[kuniaki.mukai]

@anon95304481

You cannot add a 4-th value.

I know. This is why I let = include incomparable case.

[kuniaki.mukai]

I appreciate if you could give me an example of lists of rational terms
to test functionality of semi_lex_sort.