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

[kuniaki.mukai]

EDIT 2025/8/24
I found difficuly in icl_compare/3 on transitivity. The following
might explain the difficulty. Suppose four terms 1, 2, 3, 3’

1 A = f(a, b, c)
2 B = f(a, d, e)
3 C = f(a, d, f)
3’ C’= f(a, d’,f)

by 1,2 we have A < B
by 2,3 B < C
by 1,3 A < C

However, if d and d’ are “incomparable” like Mats Carlsson’s pair, we can not have A<C’ from A<B and B<C’.

If isomorphic terms share unique index, then transitivity works exactly like that of finite terms. Details will be posted elsewhere in the near future. Fortunately, using ==/2, it is quite easy to give such unique index. In fact, I already posted using minimum coalgebra. I will post revised version with minimum coalgebra generated by ==/2, not same_term/2.

Original Post
icl-compare.pl (1.9 KB)

I am posting a draft of icl_compare/3.

icl(-C, +X, +Y) is det.

Given rational terms X, Y,
C is unified with =, <, or > as follows:

• = if X == Y (isomorphic)
• < if Y is greater than X in lexicographic order
• > otherwise

icl_compare/3 is meant as an extension of the standard compare/3 on finite terms. It tries to provide a total linear ordering on rational trees, i.e. reflexive, antisymmetric, and transitive. I believe it can be used as the compare predicate in predsort/3.

Roughly speaking, given a pair of rational terms X, Y,
icl_compare(C, X, Y) behaves as if it builds a bisimulation starting from X and Y, and walks on both trees in parallel in a depth-first, left-to-right manner. Since X and Y are assumed rational, each path has finite depth, so the overall walk is finite. This seems to guarantee termination for any X, Y. I think these two properties form the basis for correctness, in particular for transitivity, though I may be missing something.

For guaranteeing that each branch depth decreases, the ordering on branches turned out to be critical. I tried to note some details on that part.

The uploaded version includes a small change, which looks tiny but I believe is essential for keeping depths finite.

It still feels a bit strange to me that no counterexamples for transitivity appeared in the older version, even though I ran a fuzzer with a time limit of 2,000 seconds. In earlier buggy versions, counterexamples used to show up within 10 seconds. Although I still have this unanswered question in mind, I decided to post the current version as “final” for now.

It relies heavily on ==/2 and otherwise works just like the standard compare/3, without any preprocessing step.

Note on ordering on sub-term sequences.

\def\arg{\mathrm{arg}} \def\prefix{\mathrm{prefix}} \def\cycle{\mathrm{cycle}}

If A is a compound term of Prolog, \arg(i, A) denotes i-th argument of A. For example if A = f(a,g(b),c) then \arg(1, A)=a, \arg(2,A)= g(b), \arg(3,A)=c. B is called a subterm of A if B=\arg(i, A) for some i.

A sequence \gamma:= A_1, A_2, \ldots, A_n (n>1)
is called a subterm sequence if A_{i+1} is a subterm of A_i (1\leq i<n). n is called the length of the sequence, and written
n=|\gamma|=|A_1, A_2, \ldots, A_n|.

Let \Gamma be the set of subterm sequences
\gamma := A_1, A_2, \ldots, A_n such that A_i\neq A_j (i\not= j) for 1\leq i, j<n and A_k=A_n for some 1\leq k<n.

The subsequence A_i,A_{i+1}\ldots,A_n is called the cycle of the sequence, and written \cycle(\gamma). i is called the start of the cycle of \gamma, and n-i+1 is called the length of the cycle of the sequence. The subsequence A_1, A_2, \ldots, A_{i-1} (i>1) is called the prefix of \gamma, and is written \prefix(\gamma). When i=1, by convention, \prefix(\gamma)=\varepsilon (empty sequence), and the length of \varepsilon is defined to be 0.

For example, suppose \gamma is an sequence \gamma:=A, B, C, D, C
in \Gamma, where A, B, C, D are distinct. Then |\gamma|=5, the start of the cycle of \gamma is 3, |\cycle(\gamma)|=2.

For \gamma, \delta \in \Gamma, we define \gamma < \delta to mean that the following conditions holds:

• |\cycle(\gamma)| < |\cycle(\delta)|, or
• |\cycle(\gamma)| = |\cycle(\delta)| and the start of \cycle(\gamma) is less than that of \cycle(\delta).

We define \gamma\sim\delta to mean that neither \gamma<\delta nor \delta<\gamma holds.

It should be clear that for \gamma, \delta\in\Gamma, exactly one of the following holds.

• \gamma<\delta.
• \delta<\gamma.
• \gamma\sim\delta.

Also clearly it follows from \gamma\sim\delta that |\gamma|=|\delta|, |\cycle(\gamma)|=|\cycle(\delta)|, and |\prefix(\gamma)|=|\prefix(\delta)|.

[kuniaki.mukai]

@anon95304481

 @(X<Y,L) = @(S_1<S_2,[S_1=s(s(1,S_1),1),
     S_2=s(s(1,S_2),s(_5150,1))]), maplist(call, L), 
     icl_compare(C, X, Y)

Thanks for reporting. Fixed. I saw transitivity test passed for 255152 terms within 200 seconds thanks to fuzzy. I am ashamed to confess that trace, spy, and inserting snapshot (gtrace, … not at all) are still all I can use for debugging Prolog codes.

[kuniaki.mukai]

@anon95304481

You used the wrong fuzz(y) testing generator. Because this
easy to find non-terminating example, slipped your attention:

Please wait. I am going to read the SWI-Prolog manual on testing codes. It takes one week for me, who is slow to read manual.

[kuniaki.mukai]

@kuniaki.mukai

If isomorphic terms share unique index, then transitivity works exactly like that of finite terms. Details will be posted elsewhere in the near future. Fortunately, using ==/2, it is quite easy to give such unique index.

I wrote codes (mcoa_vec/2) to compute the minimum coalgebra for given a rational term using ==/2. Output is of a vector form:

Using mcoa_vec/2, I defined a comparing predicate mcomp/3

mcomp(C, X, Y):- 
       mcoa_vec(X, U), 
       mcoa_vec(Y, V), 
       compare(C, U, V).

Surprisingly, no counter example against transitivity is found so far, though not tested extensively. But I am interested in
this experiment, which seems suggest that minimum coalgebra of a (rational) term represents some lexical ordering of rational terms. This is unexpected happening. I take time for a while to see what happened.

% ?- mcoa_vec(f(g(a), b), V). 
%@ V = m(f(2, 4), g(3), a, b). 
% ?- X=f(Y,0), Y=f(X,1), mcoa_vec(X, U), mcoa_vec(Y, V). 
%@ X = f(f(X, 1), 0), 
%@ Y = f(X, 1), 
%@ U = m(f(2, 4), f(1, 3), 1, 0), 
%@ V = m(f(2, 4), f(1, 3), 0, 1). 

[kuniaki.mukai]

@anon95304481

Is your mcoa_vec/2 conservative ? I bet not ! On the other hand
an injective and conservative representation already exists for ages:

No counter example against transitivity found for acyclic terms, though not extensively tested yet. I used your fuzzer with acyclic_term inserted for restriction to Herebrand term with time limit 600 seconds
EDIT
You may be right. I forgot to insert @< test. I check later soon.

[kuniaki.mukai]

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.

[kuniaki.mukai]

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 = (>).

[kuniaki.mukai]

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 = (>).

[jan]

@anon95304481

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

[kuniaki.mukai]

@anon95304481

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 = (>).

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.

[kuniaki.mukai]

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).

[kuniaki.mukai]

@anon95304481

@kuniaki.mukai

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).

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

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.

[kuniaki.mukai]

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 = (>).

[kuniaki.mukai]

@anon95304481

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 = (>).

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 = (>).
%