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

General
43

Note that there is also the undocumented predicate

'$factorize_term'(+Term, -Skeleton, -Assignments)

This has the same signature as term_factorized/3, but it works on the physical term rather than the “logical” one. I.e., it breaks cycles and reveals sub-terms that occur multiple time in Term in the sense that same_term/2 applies to them.

You just get the cycles by walking over Assignments and binding all Assignments where the left hand variable does not occur in the right hand term. After that you have all cycles. They are the physical cycles though, which implies that they may be a multiple of the logical cycles. E.g.

?- X = f(f(X)), '$factorize_term'(X, Skeleton, Assignments).
X = Skeleton,
Assignments = [Skeleton=f(f(Skeleton))].

It might be a useful building block though. At least, it is efficient and should handle any term. It is used by the toplevel.

45

I have rewritten compare_with_stack/3 to compare_rat/3, which compares rational terms, without
applying ==2, =/2 for compound terms, and use instead same_term/2. It flattens all compound terms,
and stores in a vector to representing a system equation.

For example, f(h(a,b), c) is converted
to 1 = f(2, 3), 2=h(4,5), 4=a, 5=b,3=c.
This equations are internally kept a vector
v(f(2,3), h(4,5), c, a, b). indexes 1,2,3,4,5 may not be in this order.

?- prepare_compare_rat([X, Y, Z], Dict, Vec),
% ?- prepare_compare_rat([f(h(a,b),c)], D, V).
%@ D = [1-c, 2-b, 3-a, 4-h(a, b), 5-f(h(a, b), c)],
%@ V = v(c, b, a, h(3, 2), f(4, 1)).

I know little of internal structures, but only hope that they might be a vector when they are read, where indexes
1,2,3,… are physical addresses. In other words, viewing physical pointers as quality (=), internally prolog is a system of equations between flat terms.

% ?- compare_rat(C, f(a,b), f(c,b)).
%@ C = (<).
% ?-  X =f(Y, 0), Y=f(X,1), compare_rat(C, X, Y).
%@ X = f(f(X, 1), 0),
%@ Y = f(X, 1),
%@ C = (<).

Borrowing @burs problem series.

% ?- X = _S1-0,  _S1 = _S1-1-0,
% Y = _S2-1-0,  _S2 = _S2-0-1,
% Z = _S3-1, _S3 = _S3-0-1,
% prepare_compare_rat([X, Y, Z], Dict, Vec),
% writeln(Vec),
%	term_index([X, Y, Z], [I, J, K], Dict),
% time(repeat(10000, (
% compare_index(CIJ, I, J, Vec),
% compare_index(CJK, J, K, Vec),
% compare_index(CIK, I, K, Vec)))).
%@ v(2-8,1-9,2-9,5-8,4-9,5-9,6-8,0,1,11-9,10-8,11-8)
%@ % 1,349,999 inferences, 0.156 CPU in 0.157 seconds (100% CPU, 8651178 Lips)
%@ X = _S1-0, % where
%@     _S1 = _S1-1-0,
%@ Y = _S2-1-0, % where
%@     _S2 = _S2-0-1,
%@ Z = _S3-1,
%@ Dict = [1-(_S3-0), 2-(_S3-0-1), 3-(_S3-1), 4-(_S2-0), 5-(_S2-0-1), 6-(_S2-1), 7-(... - ... - 0), 8-0, ... - ...|...],
%@ Vec = v(2-8, 1-9, 2-9, 5-8, 4-9, 5-9, 6-8, 0, 1, 11-9, 10-8, 11-8),
%@ I = 12,
%@ J = 7,
%@ K = 3.
48

If the following prolog builtin available, the array argument is not cecessary
from the main predicate `compare_index/4’ below.

@get_flat_term(+I,  -T)  is det. 
   I  is the phical address of term T of the form `f(I1, I2, ..., In)`
   where I1, I2, ..., In are also physical address of flat terms. 
  If T is not compound ,  T may be prolog non-compoud term incdling variable

This may be so basic predicate, at least as for my concerns. I appreciate if
some one suggests its C-level efficient implementation like arg/3.

		/**************************************
		*     compare with flat term array    *
		**************************************/

index_pair_member(A, [I-J|R]):-
	(	( A = I-J; A = J-I ) -> true
	;	index_pair_member(A, R)
	).

% ?- indexed_member(I-a, [J-a]).
% ?- indexed_member(I-a, [J-b]).
indexed_member(I-X, [I-Y|_]):- same_term(X, Y), !.
indexed_member(A, [_|R]):- indexed_member(A, R).


% ?- A = a(a,b), compare_index(C, 1, 2, A).
% ?- A = a(X,Y), compare_index(C, 1, 2, A).
% ?- A = a(f(3), f(4), 3, 4), compare_index(C, 1, 2, A).

compare_index(C, I, J, A):-
	compare_index(C, I, J, A, []).
%
compare_index(=, I, J, _, H):-
	(	I = J ;  index_pair_member(I-J, H)), !.
compare_index(C, I, J, A, H):-
	arg(I, A, X),
	arg(J, A, Y),
	(	\+ ( compound(X), compound(Y) ) ->
		compare(C, X, Y)
	;	compare_arity(D, X, Y),
		(	D = (=) ->
			compare_term_args(1, C, X, Y, A, [I-J|H])
		;	C = D
		)
	).
%
compare_term_args(I, C, X, Y, A, H):-
		arg(I, X, K),
		arg(I, Y, L),
		!,
		compare_index(D, K, L, A, H),
		(	D = (=) ->
			I0 is I + 1,
			compare_term_args(I0, C, X, Y, A, H)
		;	C = D
		).
compare_term_args(_ ,= , _, _, _, _).
49

It’s embarrassing to ask at this point, but is the following proposition still unsolved ?

Proposition:

Let (H, <) be the standard total oder on the Prolog finite terms.
Let R be the set of rational term. H\subset R.
Then there is total order extention (R, <') of (H, <).

If additional restriction on odering is not required, proof is fairy easy.
So I am afraid that I am missing some restriction which is shared in this forum.

52

Thank you for comments, which push me to write a “proof” in Latex. I am not familiar with infinite tree, so I have to begin with definition of tree, which should be tedious for me. Fortunately I like such work as well as Prolog programming as a kind of hobby.

54

It is necessary to run prepare_compare_rat before running compare_index. What are X, Y, Z to compare ? I will prepare and run.

56

I am not familiar with producing X, Y, Z using robot monkey. I can test for only concrete X, Y, Z at this time, sorry.

62

I’ve written the first draft of the proof on conservative extension of the term order, but I plan to let it sit for a week so I can refine it and make sure there are no gaps before sharing it on this forum.

T_\omega is the set of finite branching trees such that for any node x, the length of the path from the root to x is finite. H is the well known set of finite terms, which is viewed as finite tree in the proof. R is the set of cyclic terms also viewed as rational trees, which has only finite number of its subtrees modulo isomorphism.
H\subset R \subset T_\omega.

There is already given a total ordering < on H, that is, (H, <) is total transitive order.

Proposition. There is a natural extension <' on T_\omega of <.

  • <\; \subset\; <'.
  • <' is total on T_\omega. (EDIT)
  • <' is transitive.

Ín summary, (T_\omega, <') is total transitive order which extends the standard (H, <)
in a natural way. As R is a subset of T_\omega, it follows that restriction <' to R is also total and transitive.

64

By total, I do not mean it is linear.

66

By saying <’ total, I mean for any pairs x, y. either x <’ y or y<’ x is defined.

68

I dropped “ordering” as typo. Thanks,

70

<’ is transitive in T_\omega, which is in fact the goal of the draft.

74 
?- help(==).
@Term1 == @Term2                                                           [ISO]
    True if Term1 is  equivalent to  Term2. A  variable is  only identical  to a
    sharing variable.

I take “equivalent to” as “bi-simulation” equivalence between internal graphs of two terms for granted.

79

Really ? Thanks for the comment. So I should not talk about semantics on ==/2 for not finite terms.

Thanks for referring to P. Aczel’s work on AFA. It is main background of my posts
on cyclic terms and bisimulation relation. BTW, A.Colmerauer’s notion of solved form looks like AFA in system of equaitons, both are in a sense “axioms” of rational trees and that of non-well-founded sets, respectively. My recent (stupid wehn ) post is on flat term solve forms.

83

Thanks.But I am afraid that I have not time to read seemingly interesting paper. In stead, just in case, I put the recent codes on compare_with_stack/3 and codes on computing maximum bisimulation on flat terms, which is strongly influenced by P.Aczel’ books, in particular, his final coagebra theorem in ZFC, though it is another story. This codes uses when/2, which I would like to hope it is a typical useful cases for students using freeze/2, which I learned from A. Colmerauer.

compare-with-stack.pl (7.2 KB)

86

About linear ordering on infinite trees, I have found a simple but fatal counter example. So I gave up as for infinite trees. However, fortunately as for rational trees the proof still seems to work.

My proof on rational trees is simple but takes 3 pages starting with definition of graph. For readers who are interested, it is convenient for me to attach PDF or SVG to posting . But it is not allowed for security reason in this forum. So I will post brief summary of proof on rational trees. But I appreciate if the reader writes to me to ask the draft for proof reading.

EDIT BTW, how about this linear ordering on infinite trees assuming AC (axiom of choices. It follows from AC there is a linear ordering on the proper infinite trees. So if proper infinite tree is defined to be greater than any finite terms, it follows that infinite and finite terms are totally ordered. Yes this is almost joking. However, to be honest, I am not sure what kind of ordering should be investigated in this forum.

89

Thanks. I guess there is a bug in preparing flat terms vector, which I noticed at least one of.

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.