Cyclic terms unification `X=f(f(X), X), Y=f(Y, f(Y)), X = Y. `

General
1

I have tested query 1 and 2.

(1)

?- X=f(X), Y=f(f(X)).
 X = Y, Y = f(f(_S1)), % where
     _S1 = f(_S1).

(2)

?- X=f(f(X), X), Y=f(Y, f(Y)), X = Y.
 false.

As X and Y in query 2 are obviously expanded to the same infinite trees, query 2 should return true, I think.

Is this (query 2) a bug of SWI-Prolog, or normal in some ISO semantics ?

BTW, even if it were a bug, If there is such a hidden predicate available, say @term_address/2, that @term_address(T, A) returns the current address A of a given compound term T, it should be straight to fix this “bug”, and as a bonus comparing cyclic terms becomes easy, though sorting list of cyclic terms might not be straight in efficiency, but would be marginal, I expect.

EDIT: I have come to notice that =/2 and ==/2 are for terms as directed graphs but not for expanded (infinite trees). However, then, should query 1 return false because as directed graphs they are not isomorphic. Anyway still it is not clear what is A = B, A == B, A@<B for cyclic terms A, B. I am afraid I am missing some basics on Prolog.

2

Interesting case. And no, AFAIK, ISO says nothing about cyclic terms. Semantics is undefined, the system may loop or crash, whatever. It is still ISO compliant.

It doesn’t look like an implementation bug either. SICStus, Ciao and YAP all consider this to fail. Cyclic unification is documented in the comments of pl-prims.c. Explained to me by Bart Demoen who claims this is one of the known variations.

No. There is same_term/2 that might do what you are thinking about?

This could be related to an older post based on analysis my Mats Carlson (if I recall well) that indicates a problem with comparison of cyclic terms. Maybe someone recalls or can find it? It was discussed here.

3

Is same_term/2 like eq in LISP ? @term_address/2 asks moreover to return index (address) of a term, which is used to compare with other cyclic terms, which, I think, could be used for comparing terms. Once I posted codes compare_with_stack/3 to compare two cyclic terms, which uses the builtin ==/2. I have to check that ‘same_term’ could be substitute for ==/2. I am not sure for now about ordering on cyclic terms when using ‘same_term’.

4

It is true if both terms have the same physical address. There is not much need for a term_address/2 in my view. Just keep the term you want to compare against in your data structure and use same_term/2 does not use more memory and is not significantly slower than taking the address and compare that. Most importantly, garbage collection changes term addresses, so you’d need to guarantee these do not happen while your predicate is executing.

5

Please help me understand the problem in Query 2 with a bit more detail? We have an f/1 and an f/2, which I rename to f1/1 and f2/2 for convenience:

X = f2(f1(X), X), 
Y = f2(Y, f1(Y)), 
X = Y.

With one more layer, we have

X = f2(f1(f2(...)), f2(...)), 
Y = f2(f2(...), f1(f2(...))), 
X = Y.

Why should this unify?

6

You are right. I forgot that =/2 (unification) and ==/2 are syntactical operations, and as for cyclic terns, I thought as semantical operations, like confusion 1 + 2 = 3 with 1+2=:=3, the former is false, and the latter is true. I mean expanded infinite trees by meaning of cyclic terms.

7

I have to agree. It is only useful to give a linear ordering on cyclic terms quickly no matter whether it is natural or unnatural. More worse, I don’t see significance of ordering cyclic terms. Is there applications of ordering cyclic terms ? Currently my concern is whether ordering induced by my compare_with_stack ( same_term not yet used) is transitive or not. So far I believe I got positive result. But I have no answer for “so then what” question.

8

I don’t know, but Prolog defines there exists a standard order of terms that relates any two terms as @<, == or @> and that this relation shall be transitive. We know this is currently violated for cyclic terms :frowning:

9

Here is updated version of my compare_with_stack/3, which use same_term instead of ‘==/2.’ The updated version seems work also for sorting lists of cyclic terms with ‘predsort/3’, though I am not sure 100% correct. It is based only mental simulation so far. I appreciate If someone there proves that the relation induced by the predicate is
a total linear ordering on terms including cyclic ones.

I am writing a related short note why I put emphasis physical addresses of cyclic terms, which has been always hidden from Prolog user. Before doing so, I would like to receive comments from those who did similar works on cyclic terms.

compare_with_stack/3 (queries/ source) 
		/*************************************
		*   naive  compare_with_stack    *
		*************************************/

% ?- compare_with_stack(C,a,a).
% ?- A=f(B, 0), B=f(A, 1), compare_with_stack(C, A, B),
%	compare_with_stack(D, B, A).
%@ A = f(f(A, 1), 0),
%@ B = f(A, 1),
%@ C = (>),
%@ D = (<).

% ?- A=f(B, X), B=f(A, Y), compare_with_stack(C, A, B),
%	compare_with_stack(D, B, A).
% ?- A=f(B, 0), B = f(A, 1), compare_with_stack(C, A, B), predsort(compare_with_stack, [A, B, A, B, A, B], R).
% ?- A=f(B, 1), B = f(A, 0), compare_with_stack(C, A, B), predsort(compare_with_stack, [A, B, A, B, A, B], R).
% ?- A=f(B, 0), B = f(A, 1), compare_with_stack(C, A, B), predsort(compare_with_stack, [A, B, A, B, A, B], R).
% ?- A=f(B, 0), B = f(A, 1), compare_with_stack(C, A, B), predsort(compare_with_stack, [A, B, A, B, A, B], R).

% ?- predsort(compare_with_stack, [A, A, A], R).
% ?- A = f(A), predsort(compare_with_stack, [A, A, A], R).
% ?- A = f(A, A), B = f(B, B), predsort(compare_with_stack, [A, B, A, B], R).
% ?- A = f(A, A), B = f(A, B), predsort(compare_with_stack, [A, B, A, B],

% ?- A = f(B, 0), B=f(A, 1),  predsort(compare_with_stack, [A, B, A, B], R).
%@ A = f(f(A, 1), 0),
%@ B = f(A, 1),
%@ R = [f(A, 1), f(f(A, 1), 0)].

compare_with_stack(C, X, Y):-compare_with_stack(C, X, Y, []).
%
compare_with_stack(C, X, Y, _):- \+ (compound(X), compound(Y)), !,
	compare(C, X, Y).
compare_with_stack(=, X, Y, H):- ( same_term(X, Y); pair_memq(X-Y, H)), !.
compare_with_stack(C, X, Y, H):-
	compare_arity(D, X, Y),
	(	D = (=) ->
		compare_args_with_stack(1, C, X, Y, [X-Y|H])
	;	C = D
	).
%
compare_args_with_stack(I, C, X, Y, H):-
		arg(I, X, A),
		arg(I, Y, B),
		!,
		compare_with_stack(D, A, B, H),
		(	D = (=) ->
			I0 is I + 1,
			compare_args_with_stack(I0, C, X, Y, H)
		;	C = D
		).
compare_args_with_stack(_ ,= , _, _, _).

% ?- pair_memq(a-b,[a-b]).
%@ true.
% ?- A=f(A), pair_memq(A-A,[A-A]).
%@ A = f(A).
% ?- A=f(A), B=f(B), pair_memq(A-B,[A-A]).
%@ false.
pair_memq(X-Y,[X0-Y0|_]):- same_term(X, X0), same_term(Y, Y0), !.
pair_memq(P,[_|R]):-pair_memq(P, R).
1 Like
12

(Nothing of importance)

13

Thanks. Your example led me to revise my codes. I hope it will returns as expected soon.

14

(Nothing of importance)

15

I checked that your examples are not counter examples for my compare_with_stack/3.

compare_with_stack/3 preserves that of finite terms, and gives
total order on rational trees. Of course we knew that for such order
this property must be given up

f(A) < f(B) => A < B

However, it is not proved yet that compare_with_stack/3 gives a total order on rational trees, though I am fairy sure it is the case. Also I have proved in mind that there is such extension of the standard term order to rational trees, which is not always preserved along subterms.

I may be missing, but can not find it.

18

(Nothing of importance)

19

I agree that the current compare_with_stack/3 does not work. Thanks for the counter example. I assumed all cyclic terms are given in a system of equations
of x = f(x1, …, xn) where x, x1, …, xn is “address” of terms , i.e., flat terms.
As far as standing on the assumption, stacks should hold addresses, but I thought
stacks is allowed to hold compound terms instead of addresses without paying attention to difference between address and term.

20

(Nothing of importance)

21

Replacing back same_term/2 with ==/2, the result seems get consistent.

% ?- H = H-9-7-6-5-4-3-2-1-0, Z = H-9-7-6-5-4-3-2-1, X = X-0-9-7-6-5-4-3-2-1,
%    compare_with_stack(CHZ, H, Z),
%    compare_with_stack(CHX, H, X),
%    compare_with_stack(CZX, Z, X),
%    predsort(compare_with_stack, [H, Z, X, X, H, X], R), length(R, N).
%@ H = H-9-7-6-5-4-3-2-1-0,
%@ Z = X, X = X-0-9-7-6-5-4-3-2-1,
%@ CHZ = CHX, CHX = (>),
%@ CZX = (=),
%@ R = [H-9-7-6-5-4-3-2-1, ... - ... - 6-5-4-3-2-1-0],
%@ N = 2.

This suggests that there was no need to change the original compare_with_stack/3
I am confusing. But ==/2 is more reasonable than same_term in theory.

EDIT
If we stand on a system of equations for flat terms over finite address spaces X, then things goes almost obvious, though I never wrote on this. However it may explain intuitive idea behind `compare_with_stack/3.’ Consider of such a tree T with X x X as node label set. For example

   x= f(y, z), 
   z= f(u, v),

here (x,y) has two child (y,u) and (z,v) in order, and so on. Each path
of T has never same label. So T must be finite trees. Hence it should be clear
that by left-most depth-first search on T, we can find a first pair (a, b) such
that a and b have different arities. Otherwise, as a consequence of the guaranteed maximum congruence relation, the expanded trees x and y are isomorphic, i.e., identical as rational trees, though we need not to define such rational trees. System of equations supports these arguments. However such relation induced above is transitive ? This is out of general theory of system of the flat equations. But as far as my mental simulation more than 10 times, it is the case. I am easy to make logiical error. Need to another 10 times mental simulation.

23

I thought the native compare/3 is not applicable to cyclic terms. Fortunately, `compare_with_stack/3’ shows transitivity also on this particular example.

% ?-  X = f(f(f(X, 1), 1), 1),
% Y = f(f(Y, 1), 0),
% Z = f(f(f(Z, 1), 0), 1),
% compare_with_stack(CXY, X, Y),
% compare_with_stack(CXZ, X, Z),
% compare_with_stack(CYZ, X, Z).
%@ X = f(f(f(X, 1), 1), 1),
%@ Y = f(f(Y, 1), 0),
%@ Z = f(f(f(Z, 1), 0), 1),
%@ CXY = CXZ, CXZ = CYZ, CYZ = (>).

% ( X>Y, X>Z, Y>Z)

As compare_with_stack/3 is based on arity_compare/3, which is clearly transitive, my conjecture is positive.

24

(Nothing of importance)

25

I may have found a simple way to prove the transitivity property, which
reduces cyclic terms to finite terms by forgetting irrelevant deep nodes.

Let A, B, C be cyclic terms, and hXY
be the depth of nodes of X, Y whose aritties differs first time
(Depth-First, Left-Right) (XY = AB, BC, AC). Let h = max{hAB, hBC, hAC}.

Let hA, hB, hC be finite terms obtained from A, B, C forgetting nodes
of depth more than h. Ordering hA, hB, hC are preserved so that
X < Y <==> hX < hY. (X, Y in { A, B, C})

Since the standard ordering of finite terms is transitive,
it follows that A<B, B < C ==> A<C.

This is not a proof yet, but details are executable, I think. But I am not sure
I can write it. To be honest, I wish someone try it.