(Nothing of importance)
Did you give counter examples against compare_with_stack/3. Sorry for missing.
Could you show me again ?
Thanks. But I am afraid it is not a counter example.
% ?- X = _S1-0, _S1 = _S1-1-0,
% Y = _S2-1-0, _S2 = _S2-0-1,
% Z = _S3-1, _S3 = _S3-0-1,
% compare_with_stack(CXY,X,Y),
% compare_with_stack(CYZ,Y,Z),
% compare_with_stack(CXZ,X,Z).
%@ X = _S1-0, % where
%@ _S1 = _S1-1-0,
%@ Y = _S2-1-0, % where
%@ _S2 = _S2-0-1,
%@ Z = _S3-1,
%@ CXY = CXZ, CXZ = (<),
%@ CYZ = (>).
it means X<Y, X<Z, Y>Z, that is, X< Z < Y, which is normal. Am I missing ?
Replace same_term with ==. Then you could get the same result of mine, which I posted before. Let me know the result.
The problem2(X, Y, Z) is not a counter example for the latest compare_with_stack3.
I am new to compare_expensive/3, which is unrelated to compare_with_stack/3, I think.
EDIT
There was typo in the previous post. This is what I wanted to see.
It seems that ==/2 checks bi-similarity between two terms, not being isomorphic as directed graphs. (right ?)
101 ?- X = f(X), Y = f(f(Y)), X=Y.
X = Y, Y = f(f(Y)).
102 ?- X = f(X), Y = f(f(Y)), X==Y.
X = Y, Y = f(f(Y)).
103 ?- X = f(X), Y = f(f(Y)), same_term(X, Y).
false.
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.
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.
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(_ ,= , _, _, _, _).
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.
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.
It is necessary to run prepare_compare_rat before running compare_index. What are X, Y, Z to compare ? I will prepare and run.
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.
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.
By total, I do not mean it is linear.
By saying <’ total, I mean for any pairs x, y. either x <’ y or y<’ x is defined.
I dropped “ordering” as typo. Thanks,
<’ is transitive in T_\omega, which is in fact the goal of the draft.
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…
?- 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.