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

(Nothing of importance)

I checked that, as pointed, the minimum coalgebra representation (MCOA) of mine is not conservative. Thanks,

Originally I planned to use the MCOA representation for conservative extension. I have to be back to original plan.

(Nothing of importance)

(Nothing of importance)

I might have made a wrong test. I tried again below after a little change, then now it shows no counter example against conservative property and transitivity. The minimum coalgebra for input is flattened so that it might be close to the standard lexical comparison. Recursive id in coalgebra is replaced with the length of cycles in the system of equations of coalgebra. However, I am still not sure on the whole on transitivity, like stray sheep.

jcomp(C, X, Y):-
	mcoa_vec(X, U),
	flat_id(1, U, U0, [], []),
	mcoa_vec(Y, V),
	flat_id(1, V, V0, [], []),
	compare(C, U0, V0).
problem9(X, Y) :-
	repeat,
	fuzzy(X), acyclic_term(X),
	fuzzy(Y), acyclic_term(Y),
	jcomp(C, X, Y),
	compare(D, X, Y),  write(.), flush_output,
	C \== D.

% ?- call_with_time_limit(300, problem10(X, Y, Z)).
problem10(X, Y, Z) :-
	repeat,
	fuzzy(X),
	fuzzy(Y),
	jcomp(C, X, Y), C = (<),
	fuzzy(Z),
	jcomp(D, Y, Z), D = (<),
	jcomp(E, X, Z),  write(E), flush_output,
	E = (>).

This ft_compare/3 below seems another conservative, transitive, and total comparing predicate on the rational trees. This solution for ft_compare(C, A, B), just flattens each of input A, B into A0, B0 ant then passes to the standard compare/3. No need of minimum coalgebra things, instead, use heavily ==/2. I don’t think it is a goal we might have been pursuing but, this is experimental for seeing effect of serializing structured cyclic terms.

ft_compare(C, A, B):- flatten_term_compare(C, A, B).
%
flatten_term_compare(C, A, B):-
	flatten_term(A, X, [], []),
	flatten_term(B, Y, [], []),
	compare(C, X, Y).
%
flatten_term(A, [U|X], Y, H):- compound(A), !,
	(	cycle_period(A, H, 1, K) ->
		U = ref(K),
		Y = X
	;	A =.. [F|As],
		length(As, N),
		U = fun(F/N),
		flatten_term_list(As, X, Y, [A|H])
	).
flatten_term(A, [basic(A)|X], X, _).
%
flatten_term_list([], [end|X], X, _).
flatten_term_list([A|As], X, Y, H):-
	flatten_term(A, X, Z, H),
	flatten_term_list(As, Z, Y, H).
%
cycle_period(I, [J|_], K, K):- I == J, !.
cycle_period(I, [_|H], J, K):- J0 is J + 1,
	cycle_period(I, H, J0, K).

% ?- call_with_time_limit(100, problem_ft(X, Y, Z)).
problem_ft(X, Y, Z) :-
	repeat,
	fuzzy(X),
	fuzzy(Y),
	ft_compare(C, X, Y), C = (<),
	fuzzy(Z),
	ft_compare(D, Y, Z), D = (<),
	ft_compare(E, X, Z),  write(E), flush_output,
	E = (>).

It is not conservative, you didn’t implement shortlex.
Means you didn’t implement the standard lexical order
as found in the ISO core standard:

?- ft_compare(C, a(1,2), b(3)).
C = (<).

?- compare(C, a(1,2), b(3)).
C = (>).

Otherwise its just like naish/2 , so you don’t need to test
transitivity. You can just prove it, by the order homomorphism
theorem. But you would need to show injectivity though.

It is naish/2 with deBruijn indexes:

?- X = f(X), Y = g(X,h(X)), naish(Y, Z).X = f(X),
Z = g(f('$IDX'(1)), h(f('$IDX'(2)))).

?- X = f(X), Y = g(X,h(X)), flatten_term(Y, Z, [], []).
Z = [fun(g/2), fun(f/1), ref(1), end, fun(h/1), 
fun(f/1), ref(1), end, end|...].

deBruijn indexes means counted from the leaf to the root,
and not from the root to the leaf, when determining a
circle Index.

In as far the Million Dollar question of Prolog is still open.

Problem is, because it belongs to the naish/2 family of
representations and because it uses (==)/2, it is extremly
slow. Try this performance test case:

hydra(0, _) :- !.
hydra(N, h(X,X)) :- M is N-1, hydra(M, X).

test(N) :- hydra(N,X), hydra(N,Y), compare(_, X, Y).

test2(N) :- hydra(N,X), hydra(N,Y), ft_compare(_, X, Y).

The SWI-Prolog implementation maintains time linearity
in the term size, since it uses Union Find:

/* compare/3 */
?- member(N,[5,10,15]), time(test(N)), fail; true.
% 12 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
% 22 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
% 32 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
true.

naish/2 family of representations simply explodes, not
to be recommended in practice:

/* ft_compare/3 */
?- member(N,[5,10,15]), time(test2(N)), fail; true.
% 832 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
% 36,874 inferences, 0.000 CPU in 0.004 seconds (0% CPU, Infinite Lips)
% 1,507,348 inferences, 0.125 CPU in 0.130 seconds (96% CPU, 12058784 Lips)
true.

Union Find as deployed by SWI-Prolog compare/3 can not only
detect loops but also sharing. Union Find algorithms were
introduced by Hopcroft and Karp in 1971 through this paper:

A Linear Algorithm for Testing Equivalence of Finite Automata
Hopcroft & Karp - 1971
https://ecommons.cornell.edu/server/api/core/bitstreams/47fc124d-2094-4f23-be59-d25fde0f9108/content

I guess it is actually possible to realize a compare/3 around the HK
technique, that is a total order for cyclic terms and that is conservative.
Through a modification of SWI-Prolog compare/3.

That is actually what we are looking for … Particularly if it doesn’t loose (significant) performance for acyclic terms. After implementing that we can also close this discussion :slight_smile:

To speed up acyclic terms you could use the simple trick:

naish2(X, Y) :- acyclic_term(X), !, Y = X.
naish2(X, Y) :- naish(X, Y).

The acyclic_term/2 is usually also linear in term size.
So you could still use a naish/2 kind of representation
compare algorithms, for acyclic terms. naish/2 has the

property that it does nothing for acyclic terms, and instead
running through naish/2, you can just short cut it, and
you wouldn’t change any of the semantics:

/* does nothing for acyclic */
?- X = f(g(a,Y),b), naish(X, Z).
Z = f(g(a, Y), b).

/* only does something for cyclic */
?- X = f(g(a,X),b), naish(X, Z).
Z = f(g(a, '$IDX'(0)), b).

But the Union Find algorithm is also fast for cyclic terms.
It detects both sharing and looping at the same time.
The Hopcroft and Karp 1971 algorithm can deal with

acylic and cyclic terms in linear time, in a uniform way.
So modifying compare/3 would have this benefit that it
would cover (==)/2 in subtrees, even when they are

cyclic, not only for acyclic subtrees.

I changed fun(F/N) to fun(N/F) to appear in the flattened list, which seems work as term order of the ISO standard.

Congratulations, you are now on this level:

Cheap Compare for Cyclic Terms
https://swi-prolog.discourse.group/t/cheap-compare-for-cyclic-terms/6427/11

After 24 months and 1000 posts. But the Million
Dollar question is still open! How make it fast ? I used
the adjective “cheap” in 2023, because it is easy to

implement. But a “cheap” car does not necessarely
have a lot of horse powers. I am not sure whether
@kuniaki.mukai takes the posed problem of making

it speedy, seriously? Maybe he is still thinking about
other things, like transitivity, anti-symmetry etc..? That
would be correctness and not performance.

About the Product Automata Construction:

For example running along two flat representions
in parallel doesn’t give any speed. If you would fold
the two flat calls into the compare/3 call. (*)

You can try yourself with variants of hydra/2. It wont
detect so much sharing. It will only provide fast failure,
if there is a an early difference. But it wont help

with (==)/2 along subtrees that are either cyclic
or acyclic, and that are equal. It wont have the same
speed profile like a Union Find algorithm has, and that

the current compare/3 implementation also shares.
The Union Find algorithm goes beyond the usual
Product Automata Construction for binary predicates.

And using Naish Indexes in parallel would still be
a product construction. You find the Product Automata
Construction also here, he uses it for an equal.

But it will horribly fail for hydra/2 like example,
just like your old predicate compare_with_stack/2
would fail, since it didn’t use Union Find either:

DFA algorithms in a Python library
https://pypi.org/project/dfa/

Hopcroft and Karp from 1971, have extremly raised the
bar, and luckily for (==)/2 and (=)/2 that some Prolog systems
have adopted it. But it makes the compare/3 problem

exremly challenging, when adopting the Union Find viewpoint.

(*) You could even automatize this step, using
a partial evaluator for Prolog. Instead of doing
the program transformation manually.

Back to the original retro compare_with_stack, I have added small changes. Now surprisingly, it have passed the fuzzer test with 600 seconds on transitivity test. The new version mimics the recent codes of mine on flattening cyclic terms in mind. The new version runs with two history stacks. The second change is to compare cycles without comparing arity. The final change is to remove the clause in the original version for isomorphic pairs. It is unbelievable for now, but the experiment is real unless I missed something.

The revival version of compare_with_stack/3
EDIT to improve for isomorphich input as =

 compare_with_stack(C, X, Y):-once(compare_with_stack(C, X, Y, []-[])).

%
compare_with_stack(C, X, Y):-once(compare_with_stack(C, X, Y, []-[])).

%
compare_with_stack(C, X, Y, _):- \+ (compound(X), compound(Y)), !,
	compare(C, X, Y).
compare_with_stack(C,  X, Y, H):- scan_count(X, Y, H, L, R), % without compare_arity.
	( L>0; R>0 ),
	!,
	compare(C,  L, R).
compare_with_stack(C, X, Y, U-V):-
	compare_arity(D, X, Y),
	(	D = (=) ->
		(  X == Y -> C = (=)
		;  compare_args_with_stack(1, C, X, Y, [X|U]-[Y|V])
		)
	;	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(_ ,= , _, _, _).


%
scan_count(X, Y, H-H0, L, R):-
	scan_count(X, H, 1, L),
	scan_count(Y, H0, 1, R).
%
scan_count(_, [], _, 0).
scan_count(X, [Y|_], K, K):- X==Y, !.
scan_count(X, [_|R], K, N):-  K0 is K + 1,
	scan_count(X, R, K0, N).
%
compare_arity(C, A, B):- functor(A, F, J),
		functor(B, G, K),
		compare(C, J/F, K/G).

It will still explode for hydrax/2, since it uses Lee Naish traversal:

?- member(N,[5,10,15]), time(testx4(N)), fail; true.
% 738 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
% 33,803 inferences, 0.000 CPU in 0.003 seconds (0% CPU, Infinite Lips)
% 1,409,045 inferences, 0.078 CPU in 0.118 seconds (66% CPU, 18035776 Lips)
true.

Try L. Peter Deutsch traversal, it can do hydrax/2, no explosion:

?- member(N,[5,10,15]), time(testx5(N)), fail; true.
% 175 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
% 445 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
% 815 inferences, 0.000 CPU in 0.000 seconds (0% CPU, Infinite Lips)
true.

Did you know that L. Peter Deutsch wrote a LISP system for the
PDP-1 when he was 17 years old ? His LISP system, just like
the IBM 704 progenitor by McCarthy, had a garbage collector,

which needed memory traversal. The test code was simply:

testx4(N) :- hydrax(N,Z,X), hydrax(N,Z,Y), compare_with_stack(_, X, Y).

testx5(N) :- hydrax(N,Z,X), hydrax(N,Z,Y), deutsch_compare(_, X, Y).

deutsch_compare(C, X, Y) :-
   deutsch(X, A),
   deutsch(Y, B),
   compare(C, A, B).

For L. Peter Deutsch see here:

Switching Gears: From Lee Naish to Peter Deutsch
https://swi-prolog.discourse.group/t/switching-gears-from-lee-naish-to-peter-deutsch/9231

Yes, your are right. Main concern of mine was why the original version was not transitive despite of the innocent looking codings.

I have no idea for speeding up inlcuding preprocessing of terms into minimum coalgebra.

% ?- hydra(20, _H), minimum_coa([_H], [I], G).
%@ I = 21,
%@ G = m(_, h(1, 1), h(2, 2), h(3, 3), h(4, 4), h(5, 5), h(6, 6), h(7, 7), h(8, 8), h(9, 9), h(10, 10), h(11, 11), h(12, 12), h(13, 13), h(14, 14), h(15, 15), h(16, 16), h(17, 17), h(18, 18), h(19, 19), h(20, 20)).

Anyway I am happy to have time to close this long thread. Thanks for your help.

According to Jan W. the thread is not yet completed,
since hydrax/2 is an acyclic term example:

We might keep you busy for another 24 months!

minimum_coa/3 might be similar like deutsch/2, but you still
need something like compare/3 (or the 100% Prolog order/3),
that does also structure detection. The later comparators are

using Union Find algorithm from Hopcroft and Karp (1971). But
even with deutsch/2 and order/3 , the Million Dollar question
is not yet solved. deutsch/2 is still slow, and the order/3

combo is only for educational purposes.

I got the following result as for “hydra” test, where mcoa_compare/3 is a compare predicate converting input terms into minimum coalgebra. I hope it is not so bad.

% ?-time(( hydra(10, _X), mcoa_compare(C, _X, _X))).
%@ % 7,123 inferences, 0.003 CPU in 0.004 seconds (89% CPU, 2277902 Lips)
%@ C = (=).
% ?-time(( hydra(20, _X), mcoa_compare(C, _X, _X))).
%@ % 16,283 inferences, 0.004 CPU in 0.004 seconds (98% CPU, 3917007 Lips)
%@ C = (=).
% ?-time(( hydra(20, _X),  hydra(19, _Y), mcoa_compare(C, _X, _Y))).
%@ % 59,786 inferences, 0.013 CPU in 0.013 seconds (98% CPU, 4590448 Lips)
%@ C = (>).

deutsch/2+order/3 from here gives:

?- time(( hydra(20, _X),  hydra(19, _Y), 
                  order_compare(C, _X, _Y))).
%@ % 2,485 inferences, 0.000 CPU in 0.001 seconds
%@ (0% CPU, Infinite Lips)
%@ C = (>).

You could first test speed of minimum_coa/2 and deutsch/2.
You didn’t publish minimum_coa/2, so I cannot do the comparison
for you. I generally suspect methods that produce a new Prolog

term and not some integer index, to be the faster methods. I
do not think indirection of integer indexes makes any sense.
But you have also to look at the asymptotic behaviour,

like I did with member(N, [5,10,15]). The asymptotic behaviour
tells you what is really going on.

Great !

Although I don’t mean to challenge you, from curiosity I timed in a separate way with this. I don’t know about deutsch, but only basics on coalgebras and naive its usage.

mcoa_compare(C, X, Y):-
	time(minimum_coa([X,Y],[I,J], M)),
	time(mcoa_compare(C, I, J, M, []-[])).
% ?- time(( hydra(20, _X),  hydra(19, _Y))), mcoa_compare(C, _X, _Y).
%@ % 39 inferences, 0.000 CPU in 0.000 seconds (67% CPU, 3900000 Lips)
%@ % 59,153 inferences, 0.003 CPU in 0.004 seconds (99% CPU, 17076501 Lips)
%@ % 589 inferences, 0.000 CPU in 0.000 seconds (96% CPU, 12270833 Lips)
%@ C = (>).
%