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.

72

Here is a (the?) theory of Prolog’s cyclic terms:
Prolog and Infinite Trees - A Colmerauer (1982):
https://www.softwarepreservation.org/projects/prolog/marseille/doc/Colmerauer-InfTree-1982.pdf/view

But given any concrete Prolog system such as SWI, (IIANM) we could simply compare pointers (or use same_term/2) if the internal representation of terms was already normalised (“minimal” in terms of Colmerauer’s article), which it apparently isn’t. Indeed, here is yet another example that the pointer-based approach in SWI is not applicable and how the specific shape of internal term representations would have to matter:

?- X = f(f(X)), arg(1, s(X), X1), arg(1, s(X1), X2), same_term(X1, X2).
X = X1, X1 = X2, X2 = f(f(X2)).

?- X = f(f), arg(1, s(X), X1), arg(1, s(X1), X2), same_term(X1, X2).
X = X1, X1 = X2, X2 = f(f).

[But now that I look at that code again, maybe I should have written e.g. arg(1, X1, X2)… anyway, the only point I am really raising is that the internal representation of terms matters.]

Indeed, reassessing, I think you ask the right question with that 1 + 2: given X = f(X) and X = f(f(X)), are we to consider the obtained terms equivalent or not?

Of course, along the route of cyclic terms proper (where the terms induced by X = f(X) and X = f(f(X)) are to be considered equivalent), in a Prolog system such as SWI (that does not do the minimization at term parsing and instantiation time – which would in fact require, to begin with, distinguishing a surface/input syntax from a/the deep syntax), Prolog terms in the theory can only be equivalence classes of the syntactic terms…

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.

76

My question was rather part of the explanation, and you are anyway not answering it. Indeed, 1) ISO does not cover cyclic/infinite terms (wasn’t that clear already?); and 2) “bi-simulation” is a red-herring really: that “X = f(X)” and “X= f(f(X))” generate equivalent terms won’t give you a canonical form nor anything to put them in order. And have you also considered the relationship between X = f(X) and Y = f(Y)? IOW; you do need a theory of terms, and a specific one at that, or so I would think.

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.

87

[Axiom of Choice, etc.] Yes this is almost joking.

That was indeed mathematically imprecise, but especially keep in mind that classical mathematics, generally speaking, does not have computational content. E.g. with AC you have a proof that the real numbers (equiv. the complete binary tree) can be well-ordered, but that won’t give you any concrete such well-order…

I am not sure what kind of ordering should be investigated in this forum.

IMO, in this context, i.e. SWI and more generally Prolog, it would be interesting to write a compare that is sound and correct for the cyclic terms, too (which initially I thought was what you were trying to do).

89

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