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

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