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

General
92

In addition to stacks holding history, I have added bisimulation vector bringing around with comparing tasks, which represents quotient set modulo the bisimulation. Then your “counter example” is fixed. Before your example, I didn’t think such maximum bisimulation is necessary for comparing cyclic terms, though I doubt it’s necessity.

Thank you for surprising example. I need to take time on comparing cyclic terms without relying ==/2 and =/2

% ?-  S1 = S1-1-0,
% 	X = S1-0-0,
%   S2 = S2-1-0,
%   Y = S2-1-1,
%   S3 = S3-1-0,
%	Z = S3-0,
%    xcompare_rat(CXY, X, Y),
%    xcompare_rat(CXZ, X, Z),
%    xcompare_rat(CYZ, Y, Z).
%@ S1 = S2, S2 = S3, S3 = S3-1-0,
%@ X = _S1-0-0, % where
%@     _S1 = _S1-1-0,
%@ Y = _S2-1-1, % where
%@     _S2 = _S2-1-0,
%@ Z = S3-0,
%@ CXY = (<),
%@ CXZ = CYZ, CYZ = (>) .

	Z<  X  <  Y  !
96

This is a partial comment.

I took Mats Carlson’s cyclic terms was a discovery that property of ‘@<’ on finite terms
fails on cyclic terms.

If A@<B then f(A, C) @< f(B, C)

Although it was really surprising, that is all for me. I know little of consequence afterward.

Here is query logs about compaireing Mats Carlson’s cyclic terms as it is.

% ?- 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(D, B, A).
%@ A = f(f(A, 1), 0),
%@ B = f(A, 1),
%@ D = (>).

% ?- A=f(B, 0), B=f(A, 1), compare_rat(C, A, B).
%@ A = f(f(A, 1), 0),
%@ B = f(A, 1),
%@ C = (<).

% ?- A=f(B, 0), B=f(A, 1), compare_rat(D, B, C).
%@ A = f(f(A, 1), 0),
%@ B = f(A, 1),
%@ D = (>).
98

I could not find such cases. Could you reproduce such samples of
cyclic terms X, Y, Z here that X<Y, Y<Z but NOT X<Z. I believe there is no such cases
for the recent version `compare_rat/3` and `compare_with_stack/3.` Thanks.

101

Really ? That’s sounds great ! BTW, I have found another variant of `compare_rat/3`, which does not use `union-find` but argument stack instead, which is directly after my "proof" of "conservative extension of the finite terms order to cyclic terms. I will report within a couple of days. Thanks for reply.

105 
Finally, I have noticed the following fact which the reader might have been already familiar with.  Is it too late ? 
The conservative extension of ordering on finite terms to rational terms 
is not total, However, it is possible to check whether given pairs of  
rational terms are comparable or not.  
So I have added a couple of lines to call bisimilarity checking. 

%  ?- X = S1-1,  S1 = S1-1-0, 
%     Y = S2-1-0,  S2 = S2-1-0,
%	  Z = S3-1, S3 = S3-0-1,
%	xcompare_rat(CXY, X, Y),
%   xcompare_rat(CXZ, X, Z),
%   xcompare_rat(CYZ, Y, Z).
%@ incomatible      <<<  only show incompatibility found.
%@ incomatible
%@ X = S3, S3 = S3-0-1,
%@ S1 = Y, Y = S2, S2 = S2-1-0,
%@ Z = S3-1,
%@ CXY = CYZ, CYZ = (<),
%@ CXZ = (>).

I have not said about the definition of order on rational terms, which I thought we shared from the ordering “@<“ on finite terms.

107 
Now the updated version of `compare_with_stack/3` may return `incomparable`.
As I have admitted (due to your persuasion ? ) incomparability among rational terms, now it sounds reasonable.  

I noticed earlier the incomparability among irrational trees, 
but I did not noticed the same situation may occur already even in rational trees. 

```
% Mats Carlson's terms.
% ?- A=f(B, 0), B=f(A, 1), compare_with_stack(C, A, B).
%@ C = incomparable.
```


		/******************************************
		*   compare_with_stack 	based on  ==/2.	  *
		******************************************/


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, _):- X==Y, !.
compare_with_stack(incomparable, X, Y, H):- 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]).

pair_memq(A,[I-J|_]):- (A == (I-J); A==(J-I)), !.
pair_memq(P,[_|R]):- pair_memq(P, R).

% ?- predsort(compare_arity, [a(2,2), a(2,2)], S).
compare_arity(C, A, B):- functor(A, F, J),
		functor(B, G, K),
		compare(C, J/F, K/G).



% ?- X = _S1-1,
%     _S1 = _S1-1-0,
% Y = _S2-1-0,
%     _S2 = _S2-1-0,
% Z = _S3-1,
%     _S3 = _S3-0-1,
%	compare_with_stack(CXY, X, Y),
%   compare_with_stack(CXZ, X, Z),
%   compare_with_stack(CYZ, Y, Z).
%@ X = _S3-0-1,
%@ Y = _S2-1-0,
%@ Z = _S3-1,
%@ CXY = CXZ, CXZ = incomparable,
%@ CYZ = (<).
109

Instead of direct replying, let me say about what I observe. The incomparable cases occurs only on the left most branches. Do you share similar observation ? At first it sounds strange, but the following example may support my observaton. I could explain partially to myself that it is a consequence of definition of order of terms. Sorry for this useless reply.

% ?-  X = f(a, \_S1-4-1-7-6-3-7-7-7-9),

%     \_S1 = \_S1-4,
% Y = f(a, \_S2-5-9-5-9-3-0-5-2),
%     \_S2 = \_S2-4,
% Z = f(a, \_S3-5-3-9-3-2-9-1-1-9),
%     \_S3 = \_S3-9-3-1-5-4,
%	compare_with_stack(CXY, X, Y),
%	compare_with_stack(CXZ, X, Z),
%	compare_with_stack(CYZ, Y, Z).
%@ X = f(a, … - … - 1-7-6-3-7-7-7-9), % where
%@     \_S1 = \_S1-4,
%@ Y = f(a, \_S2-5-9-5-9-3-0-5-2),
%@ Z = f(a, … - … - 3-9-3-2-9-1-1-9), % where
%@     \_S3 = \_S3-9-3-1-5-4,

%@ CXY = CXZ, CXZ = CYZ, CYZ = (<).

i.e.
X<Y, X<Z, Y<Z

111

EDID 2025/7/31. The below posted seems now too ad-hoc. Non-isomophic pairs
should recurrently appear getting even off and off the left-most branch. Outputting “incomparable” for such pair is at my best, though smart solution may exist without “incomparable. ” I should wait. END

Based on observation that incomparability occurs only left most branches,

I wrapped cyclic terms X, Y, Z with f, a as f(a, X), f(a, Y), f(a, Z) , where f and

a are not used in X, Y, Z. Then I got incomparable-free result Y< X<Z. Strange enough.

I may be missing, but just post what I saw.

% ?- X = _S1-1,
%     _S1 = _S1-1-0,
% Y = _S2-1-0,
%     _S2 = _S2-1-0,
% Z = _S3-1,
%     _S3 = _S3-0-1,
%	compare_with_stack(CXY, f(a,X), f(a,Y)),
%   compare_with_stack(CXZ, f(a,X), f(a,Z)),
%   compare_with_stack(CYZ, f(a,Y), f(a,Z)).
%@ X = _S3-0-1,
%@ Y = _S2-1-0,
%@ Z = _S3-1,
%@ CXY = (>),
%@ CXZ = CYZ, CYZ = (<).
113

(I have trouble with posting. Safari, macOS Sequioa: could not type backquote, strange line feed. etc. So short reply here)

EDIT solved by selecting U.S. input sources.

I have a proof that in rational terms, if X< Y and Y< Z then X<Z , by lifting argument of finite terms to rational ones. It is not difficult, rather easy but tedious in formal way. graph, tree, ancestor, descendant, linear order on direct children, is_left_ of , isomorphic, restriction, arity-labeled tree, definition of order < , depth of node, restriction of rational trees by depth.

Then proof of transitivity is based on finte terms and lifiting to X<Y, Y<Z => X< Z. In short given X, Y, Z with X< Y and Y<Z. Then there exists sufficiently large n for the following. Consider finite Xn, Yn, Zn of X,Y, Z restricted by depth n. Then Xn< Yn, Yn<Zn by restriction property for the large n, then we have Xn < Zn. The final step is to lift Xn < Zn to X<Z, which is divided by 5 cases depending on the definition of order <.

121

I have updated compare_with_stack so that it resolves incomparable pairs on the fly without need of “physical address” of compound terms. Still it relis heavily on ==/2. Before posting the updated codes, I would like to give monkey test fuzzer (?) of testing transitive law. But I failed to find the fuzzer. I will appreciate if someone points the post for the fuzzer or send it to me.

123

Thanks. I ran it with time limit 600, which must be too short for now.

% ?- call_with_time_limit(600, problem(X, Y, Z)).
%@ ERROR: Unhandled exception: Time limit exceeded

problem(X, Y, Z) :-
   repeat, fuzzy(X), fuzzy(Y),
   d_compare(C, X, Y), C = (<),
   fuzzy(Z),
   d_compare(D, Y, Z), D = (<),
   d_compare(E, Z, X), E = (<).

The revised compare_with_stack/3, which resolves incomparable pairs on the fly
happens to be transitive, anti-symmetric, and total. But proof of transitivity seems
much more complex than ordinal depth-first left-to-right walk order.
For now, it is not surprising that the fuzzy test find a counter example.

125

Me too doubt on termination, though I applied the König lemma for termination.
The fuzzy test is running with time limit 20000. If it gives no counter example, I will post the new d_compare/3 ( = for short of revised compare_with_stack/3) as planned but in 10 hours. I have to take a sleep

EDIT Something wrong with my d_compare/3. I realize that fuzzy is useful.

% ?- call_with_time_limit(20000, problem(X, Y, Z)).
%@ /Users/cantor/local/bin/pac: line 7: 63832 Killed: 9               ${SWIPL} -l $PAC -l $ZDD
1 Like
128

icl_compare/3 below compares rational terms. So far, fuzzy test fails to find a counter example for transitivity. So I am posting the codes as I posted to do so.

The codes relies on ==/2 heavily, and I borrowed idea from @janW’s post using length of the initial cycle on the path of subterm series, which I saw vaguely a couple of years ago. It is appreciated if the code is tested by others. In fact, I’m in doubt.

% ?- icl_compare(C, a, b).
% ?- icl_compare(C, b, a).
% ?- X=(Y,0), Y=f(X,1), icl_compare(C, X, Y).

icl_compare(C, I, J):- icl_order(C, [0*0, I-J], []).

% icl: initial cycle length based ordering
icl_order(=, [], []):-!.
icl_order(C, [], [[_,_|Ps]|A]):-!, icl_order(C, Ps, A).
icl_order(C, [_, I-J|Ps], A):-
	(	I == J -> icl_order(C, Ps, A)
	;	\+ (compound(I), compound(J)) -> compare(C, I, J)
	;	compare_arity(D, I, J),
		(	D = (=) ->
			initial_cycle_length(I-J, A, L*R, 1),
			(	nonvar(L), nonvar(R) ->
				compare(E, L, R),
				(	E = (=) ->
					A = [[_,_|Qs]|A0],
					icl_order(C, Qs, A0)
				;	C = E
				)
			;	I =.. [_|Is],
				J =.. [_|Js],
				zipper(Is, Js, Zip),
				(	var(L) -> L = 0
				;	true
				),
				(	var(R) -> R = 0
				;	true
				),
				icl_order(C, Zip, [[L*R, I-J|Ps]|A])
			)
		;	C = D
		)
	).

% ?- initial_cycle_length(a-b, [[0*0, a-b]], L*R, 1).
% ?- initial_cycle_length(a-b, [[0*0, a-c], [0*0, d-b]], L*R, 1).
initial_cycle_length(_, [], _, _):-!.
initial_cycle_length(_, _, L*R, _):- nonvar(L), nonvar(R), !.
initial_cycle_length(X-Y, Cs, L*R, K):-
	Cs=[[L0*R0, A-B|_]|Cs0],
	(	nonvar(L) -> true
	;	L0>0 -> L = L0
	;	X == A -> L = K
	;	true
	),
	(	nonvar(R) -> true
	;	R0>0 -> R = R0
	;	Y == B -> R = K
	;	true
	),
	K0 is K + 1,
	initial_cycle_length(X-Y, Cs0, L*R, K0).
%
compare_arity(C, A, B):- functor(A, F, J),
		functor(B, G, K),
		compare(C, J/F, K/G).

% ?- zipper([a,b],[1,2], Z).
zipper([], [], []).
zipper([A|As], [B|Bs], [A-B|Cs]):-
	zipper(As, Bs, Cs).
130

Fixed. Thanks. Fortunately, it’s careless bug as usual for me.

icl_order(=, [], []):-!.
icl_order(C, [], [[_,_|Ps]|A]):-!, icl_order(C, Ps, A).
icl_order(C, [LPair, I-J|Ps], A):-       %% was bug.
	(	I == J -> icl_order(C, Ps, A)
	;	\+ (compound(I), compound(J)) -> compare(C, I, J)
	;	compare_arity(D, I, J),
		(	D = (=) ->
			initial_cycle_length(I-J, A, L*R, 1),
			(	nonvar(L), nonvar(R) ->
				compare(E, L, R),
				(	E = (=) ->
					A = [[_,_|Qs]|A0],
					icl_order(C, Qs, A0)
				;	C = E
				)
			;	I =.. [_|Is],
				J =.. [_|Js],
				zipper(Is, Js, Zip),
				(	var(L) -> L = 0
				;	true
				),
				(	var(R) -> R = 0
				;	true
				),
				icl_order(C, [L*R|Zip], [[LPair, I-J|Ps]|A])  % was bug.
			)
		;	C = D
		)
	).
133

Did you mean this ?

?- icl_compare(C, X, 1).
%@ C = (<).
136

Is this what is said that ==/2 is not compatible

icl_compare/3 is not related to the “problem”, I hope.

% ?-  X = s(X, 1),
% Y = s(Y, _),
%	icl_compare(C, X, Y),
%	\+ X == Y.
%@ X = s(X, 1),
%@ Y = s(Y, _),
%@ C = (>).
139

No. The two lines in the icl_compare/3 indicated by comment " % was bug" are all.
(macOS 15.6 iMac intel 2020, m4 MacBook pro, latest swipl via GitHub source).

I wrote my ==/2 (named cong/2) using same_term/2 and a list for book keeping bisimulation. Thus replacing ==/2 with my cong/2, I saw nothing different with icl_compare/3 you have.

Surely it is strange that when the \+ _ ==_ is used in fuzzy test, something strange happens.

142

You may be right. I reviewed more on the codes, and have found one of clauses still to be reviewed in deep.

Roughly, icl_order is left-most derivation of a context free grammar, very roughly. But left most non terminal has extra information on cycle lengths. It depends on context whether dropping or keeping the extra information. I am explaining in analogy. But needs time to fix it in clear mind.

143

Following the above naive analogy, I rewrote icl_compare so that my confusion should be minimized. There were surely confusion on L*R information (pair of lengths of initial cycles of Left and Right paths from the top). It should be of the parent node which is shared with siblings. This update fixes all pointed out so far. Thanks.

icl_compare(C, I, J):- icl_order(C, [[0*0, I-J]]).
%
icl_order(=, []):-!.
icl_order(C, [[_] | Anc]):-!, icl_order(C, Anc).
icl_order(C, [[LPair,I-J|Ps] | Anc]):-!,
	(	I == J -> icl_order(C, [[LPair|Ps] | Anc])
	;	\+ (compound(I), compound(J)) -> compare(C, I, J)
	;	compare_arity(D, I, J),
		(	D = (=) ->
			initial_cycle_length(I-J, Anc, L*R, 1),
			(	nonvar(L), nonvar(R) ->
				compare(E, L, R),
				(	E = (=) ->
					icl_order(C, [[LPair|Ps] | Anc])
				;	C = E
				)
			;	I =.. [_|Is],
				J =.. [_|Js],
				zipper(Is, Js, Zip),
				(	var(L) -> L = 0
				;	true
				),
				(	var(R) -> R = 0
				;	true
				),
				icl_order(C, [[L*R|Zip], [LPair, I-J|Ps] | Anc ])
			)
		;	C = D
		)
	).
146

Sorry to hear that. Nevertheless I must thank you for testing old icl_compare/3. BTW, I posted already the full codes of new icl_compare/3. The new version fixes all which were pointed as bugs.

I do not intend to waste your valuable time any more, but I would like to continue to develop this approach by myself, which is inspired by idea to use length of first cycle of branch as a character for comparing two “incomparable” branches. This idea was posted in this forum a couple of years ago, I believe. I don’t know exact reason why it discontinued. In this direction, we will finally get an order which is conservative for the standard order on finite terms, total, transitive. If we would achieve such goal, it would never successful without the fuzzy test tool.

Thanks again. Bye.

% ?- X=f(Y,0), Y=f(X,1), icl_compare(C, X, Y), \+ X==Y.
%@ X = f(f(X, 1), 0),
%@ Y = f(X, 1),
%@ C = (>).

% ?-  call_with_time_limit(100, (  repeat,fuzzy(X), fuzzy(Y), icl_compare(C, X, Y), C = (=),
%	\+ X == Y)).
%@ ERROR: Unhandled exception: Time limit exceeded

% ?-  X = s(_, 1), Y = s(_, 1), icl_compare(C, X, Y).
%@ X = s(_, 1),
%@ Y = s(_, 1),
%@ C = (<).

% ?-  X = s(A, 1), Y = s(B, 1), icl_compare(C, X, Y).
%@ X = s(A, 1),
%@ Y = s(B, 1),
%@ C = (<).

% ?-   call_with_time_limit(100, (repeat,fuzzy(X), ground(X),  fuzzy(Y), ground(Y), icl_compare(C, X, Y), C = (=),
%	\+ X == Y)).
%@ ERROR: Unhandled exception: Time limit exceeded