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

General
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