comparing infinite terms
Mats Carlsson
In the '80s, Alain Comerauer, Joxan Jaffar and others published
algorithms for unification without occurs check that could work
with infinite (cyclic) terms with termination guaranteed.
Until yesterday, I always believed that the standard total order for
finite Prolog terms readily extended to include infinite terms as
well. However, the following example shows two terms that can't be
ordered.
Consider the terms A and B defined by the equations
[1] A = s(B,0).
[2] B = s(A,1).
Clearly, A and B are not identical, so is A @< B or A @> B?
Assume A @< B. But then s(A,1) @< s(B,0) i.e. B @< A. Contradiction.
Assume A @> B. But then s(A,1) @> s(B,0) i.e. B @> A. Contradiction.
So the standard order of Prolog terms cannot include (some) infinite
terms. On reflection, the same is true for the integers---infinity
minus infinity is not defined.
Perhaps this is all obvious, but I was a bit jarred at first.
Mats Carlsson, PhD
Computing Science Department tel: +46 18 187691
Uppsala University fax: +46 18 511925
P.O. Box 311 Email: m...@csd.uu.se
S-751 05 Uppsala, Sweden
Bernhard Pfahringer
In article <u8ispas...@brigitte.csd.uu.se>,
Mats Carlsson <m...@csd.uu.se> wrote:
>In the '80s, Alain Comerauer, Joxan Jaffar and others published
>algorithms for unification without occurs check that could work
>with infinite (cyclic) terms with termination guaranteed.
>
>Until yesterday, I always believed that the standard total order for
>finite Prolog terms readily extended to include infinite terms as
>well. However, the following example shows two terms that can't be
>ordered.
>
>Consider the terms A and B defined by the equations
>
>[1] A = s(B,0).
>[2] B = s(A,1).
>
>Clearly, A and B are not identical, so is A @< B or A @> B?
>
I guess one should be able to define an order:
[1] X = s(s(X,1),0).
[2] Y = s(s(Y,0),1).
But Sicstus shows the following interesting behavior:
| ?- A=s(B,0),B=s(A,1),compare(R1,A,B),write(R1),nl,
X=s(s(X,1),0),Y=s(s(Y,0),1),compare(R2,X,Y),write(R2),nl,
A=X,B=Y,compare(R3,A,B),write(R3),nl,
compare(R4,X,Y),write(R4),nl,fail.
>
<
>
<
no
i.e. A = X < Y = B < A
Bernhard
--
--------------------------------------------------------------------------
Bernhard Pfahringer
Austrian Research Institute for http://www.ai.univie.ac.at/~bernhard/
Artificial Intelligence bern...@ai.univie.ac.at
Lee Naish
In article <ALF.96Ju...@mut.sics.se>, a...@sics.se (Thomas Sjöland) writes:
> In article <4sg7an$1j...@www.univie.ac.at> bern...@doebling.ai.univie.ac.at (Bernhard Pfahringer) writes:
>
> [quoting Mats Carlsson's article]
> >>Consider the terms A and B defined by the equations
> >>
> >>[1] A = s(B,0).
> >>[2] B = s(A,1).
> >>
> >>Clearly, A and B are not identical, so is A @< B or A @> B?
> >>
> >If you look at the two infinite terms differently,
> >I guess one should be able to define an order:
> >
> >[1] X = s(s(X,1),0).
> >[2] Y = s(s(Y,0),1).
>
> If I understood your construction correctly, you reach a "normal
> form" in this case of the (not infinite but) circular terms by
> "unfolding" other variables allowing you to define the order between
> variables referring to these equations.
>
> But you cannot always define such a normal form.
> A formal definition of the standard order is necessary for further
> discussions. The "standard order" referred to in the SICStus manual
> is for variables "roughly oldest first".
Basing comparison of infinite regular trees on their finite
representation as cyclic graphs (which are in turn represented
by Prolog terms containing bound variables) does seem to lead to
problems. Note that the trees themselves are ground so the
problem of comparing variables (perhaps) should not arise.
The problem, as I see it, is that the standard ordering relies on
a depth first traversal of the trees. The first pair of differing
labels (functor/arity or constant or unbound variable) in the depth
first left to right traversal of two terms determines the ordering.
In the terms above the labels encounted are s/2,s/2,s/2,s/2,s/2,s/2,
..... indefinitely.
It seems possible to order all terms using breadth first traversal
instead. Taking Mats' example: A @< B since A=s(s(?,?),0) and
B=s(s(?,?),1). For Thomas' example: X @> Y.
For Prolog with finite terms depth first comparison is definitely
more useful, its standard and changing it would break many programs.
However, we could combine the two ordering methods as follows:
If a depth first traversal of the two terms leads to a pair of
differring labels in a finite number of steps, these labels determine
the ordering. Otherwise a breadth first traversal is used.
This definition 1) preserves current practice for finite terms, 2)
works for infinite terms, and 3) should be possible to implement
reasonably efficiently, I think! Its probably not ideal. For
example, if two terms have equal infinite subterms it may force
the comparison into breadth first mode: f(g(X,0),1) @> f(g(X,1),0)
if X is an infinite term (if its any finite term, including a
variable, the comnparison is reversed). It should be possible to
avoid this anomaly for equal infinite subterms at least.
lee
Thomas Sjöland
In article <4sg7an$1j...@www.univie.ac.at> bern...@doebling.ai.univie.ac.at (Bernhard Pfahringer) writes:
[quoting Mats Carlsson's article]
>>Consider the terms A and B defined by the equations
>>
>>[1] A = s(B,0).
>>[2] B = s(A,1).
>>
>>Clearly, A and B are not identical, so is A @< B or A @> B?
>>
>If you look at the two infinite terms differently,
>I guess one should be able to define an order:
>
>[1] X = s(s(X,1),0).
>[2] Y = s(s(Y,0),1).
If I understood your construction correctly, you reach a "normal form"
where you need not consider "mutually recursive" occurrences of
variables in the equations, by "unfolding away" other variables allowing
you to define the order between variables referring to these
equations.
But, you cannot always define such a normal form.
consider
[1] A=s(B,A,0).
[2] B=s(A,B,1).
Unfolding one level gives
[1] A=s(s(A,B,1),s(B,A,0),0).
[2] B=s(s(B,A,0),s(A,B,1),1).
etc. ad nauseam.
You cannot get rid of the two variables in either definition by unfolding.
(also, you might perhaps violate the "older than" criterion by unfolding).
PS. (If you saw this post more than once I apologize for posting and
cancelling misleading versions). DS.
--
(Alf) Thomas Sjöland
Internet e-mail: a...@sics.se
URL: http://www.sics.se/~alf/
##
Thomas Sjöland
>Basing comparison of infinite regular trees on their finite
>representation as cyclic graphs (which are in turn represented
>by Prolog terms containing bound variables) does seem to lead to
>problems. Note that the trees themselves are ground so the
^^^^^^^^
most likely you mean "the cyclic graphs".
>It seems possible to order all terms using breadth first traversal
>instead.
>For Prolog with finite terms depth first comparison is definitely
>more useful, its standard and changing it would break many programs.
I guess it is important that @< is insensitive to unfolding,
i.e. e.g.
A=s(B,1), B=s(A,0), compare(Op,A,B)
shold give the same result as
A=s(s(A,0),1), B=s(s(B,1),0), compare(Op,A,B)
Below is a version of compare/3 that seems to accomplish this in SICStus 3.
Combining cmp/3 with the standard version of compare/3 to avoid breaking
programs where all terms are non-circular is of course interesting, but would
perhaps lead to odd behaviours (although I have no example right now).
Please hack away. It isn't exactly efficient code, using append and all...
Hope you don't find a bug :-)
/Thomas
%------------------------------------------------------------------------
% version of compare/3
% that is "stable" over unfolding of ground circular terms.
% TS, 960719
test1p :- (t1(X,Y) ; t1u(X,Y)), p(X,Y).
test2p :- (t2(X,Y) ; t2u(X,Y)), p(X,Y).
test1q :- (t1(X,Y) ; t1u(X,Y)), q(X,Y).
test2q :- (t2(X,Y) ; t2u(X,Y)), q(X,Y).
p(A,B) :- compare(O,A,B), write(O),nl,fail.
q(A,B) :- cmp(O,A,B), write(O),nl,fail.
t1(A,B) :- A=s(B,1), B=s(A,0).
t1u(A,B) :- A=s(s(A,0),1), B=s(s(B,1),0).
t2(A,B) :- A=s(B,A,1), B=s(A,B,0).
t2u(A,B) :- A=s(s(A,B,0),A,1), B=s(s(B,A,1),B,0).
cmp(O,A,B) :- % compound terms are checked separately
compound(A),
compound(B),
!, map_cmp(O,A,B).
cmp(O,A,B) :- cmp0(O,A,B).
cmp0(O,A,B) :-
A==B,
!, O='='.
cmp0(O,A,B) :-
var(A),
!, compare(O,A,B).
cmp0(O,A,B) :-
var(B),
!, compare(O,A,B).
cmp0(O,A,B) :-
atomic(A),
!, compare(O,A,B).
cmp0(O,A,B) :-
atomic(B),
!, compare(O,A,B).
cmp0(O,A,B) :- % same functor/arity
functor(A,N,I),
functor(B,N,I),
!, O='='.
map_cmp(O,A,B) :-
A=..Aargs,
B=..Bargs,
map_cmp0('=',Acc,Aargs,Bargs),
map_cmp_cont(Acc,O,Aargs,Bargs).
map_cmp0(Acc,O,[],[]) :-
!, O=Acc.
map_cmp0(Acc,O,[A|Aargs],[B|Bargs]) :-
Acc='=',
!, cmp0(Acc1,A,B),
map_cmp0(Acc1,O,Aargs,Bargs).
map_cmp0(Acc,O,_,_) :-
!, O=Acc.
map_cmp_cont('=',O,A,B) :-
!, unfold(A,Au),
unfold(B,Bu),
map_cmp(O,Au,Bu).
map_cmp_cont(Acc,O,_,_) :-
!, O=Acc.
unfold(A,Au) :-
A=..Args,
map_unfold1(Args,[],Au).
map_unfold1([],Acc,Au) :-
!, Acc=Au.
map_unfold1([H|T],Acc,Au) :-
!, H=..Args,
append(Acc,Args,L),
map_unfold1(T,L,Au).
append([],L,L).
append([H|T],L,[H|R]) :- append(T,L,R).
Lee Naish
In article <ALF.96Ju...@mut.sics.se>, a...@sics.se (Thomas Sjöland) writes:
> In article <4shfcm$e...@mulga.cs.mu.OZ.AU> l...@cs.mu.OZ.AU (Lee Naish) writes:
>
> >Basing comparison of infinite regular trees on their finite
> >representation as cyclic graphs (which are in turn represented
> >by Prolog terms containing bound variables) does seem to lead to
> >problems. Note that the trees themselves are ground so the
> ^^^^^^^^
> most likely you mean "the cyclic graphs".
No. I don't mean graphs and I don't mean tagged pointers to blocks of memory
containing tagged pointers etc etc. I mean trees!
The tree f(f(f(f(..... can be *represented* by either of the following graphs
(along with an infinite number of other ways):
A B
->f ->f
| | | |
| | | |
-- | f
| |
| |
--
> I guess it is important that @< is insensitive to unfolding,
This is based on the correct intuition that it is the tree which is
important, not how it is represented. A and B are different graphs
but they represent the same tree. In general, "unfolding" preserves
the tree but not the graph.
lee
Thomas Sjöland
>> >problems. Note that the trees themselves are ground so the
>> ^^^^^^^^
>> most likely you mean "the cyclic graphs".
>
>No. I don't mean graphs and I don't mean tagged pointers to blocks of memory
>containing tagged pointers etc etc. I mean trees!
Groundness is not a property of a tree, but of its representation.
>The tree f(f(f(f(..... can be *represented* by either of the following graphs
>(along with an infinite number of other ways):...
I read your posting as referring to the groundness of the
representations of the infinite trees (as graphs) rather than to some
property of the trees themself which often would require an induction
proof rather than a search operation to establish, but never mind,
this is beside the point since the code I posted concerned a
comparison relation for ground Prolog terms that behaves "declaratively".
>> I guess it is important that @< is insensitive to unfolding,
>
>This is based on the correct intuition that it is the tree which is
>important, not how it is represented. A and B are different graphs
>but they represent the same tree. In general, "unfolding" preserves
>the tree but not the graph.
... which has some peculiar effects when mixing the representation with
the represented.
>> I guess it is important that @< is insensitive to unfolding,
>This is based on the correct intuition that it is the tree which is
>important, not how it is represented. A and B are different graphs
>but they represent the same tree. In general, "unfolding" preserves
>the tree but not the graph.
However, this detour into the ideal world of infinite trees where
representations are irrelevant doesn't really answer Mats' original
post concerning the standard order for Prolog terms.
Mats point, as I read it, was one of astonishment concerning the behaviour
of the @</2 operation on ground circular representations.
It seems fruitless to look for "declarative" versions of @</2,
and thus compare/3, since these involve comparison of unbound variables,
but what can be done, as you pointed out earlier, is to provide a
kind of variation of @</2 etc. operation that behaves intuitively
"declaratively" when encountering ground terms (like ground circular graphs
representing infinite trees).
Lee Naish
In article <ALF.96Ju...@mut.sics.se>, a...@sics.se (Thomas Sjöland) writes:
> >... I mean trees!
>
> Groundness is not a property of a tree, but of its representation.
I disagree. I was using "tree" and "term" to mean the same thing (mostly
using "tree" because the terminology is better established, eg "rational
trees"). With this meaning groundness applies to terms = trees, not
representations = pointers etc. I guess my post didn't make this clear.
> However, this detour into the ideal world of infinite trees where
> representations are irrelevant doesn't really answer Mats' original
> post concerning the standard order for Prolog terms.
>
> Mats point, as I read it, was one of astonishment concerning the behavior
> of the @</2 operation on ground circular representations.
My point was that to get a satisfactory solution to the problem we must look
at what is being represented (inhabitants of the ideal world of infinite trees).
>It seems fruitless to look for "declarative" versions of @</2,
>and thus compare/3, since these involve comparison of unbound variables,
Agreed. One solution is to delay such comparisons until they are sufficiently
instantiated. term_compare/3 in NU-Prolog does this (you could also generate
an error if delaying is not supported).
lee
Thomas Sjöland
>In article <ALF.96Ju...@mut.sics.se>, a...@sics.se (Thomas Sjöland) writes:
>> >... I mean trees!
>>
>> Groundness is not a property of a tree, but of its representation.
>
>I disagree. I was using "tree" and "term" to mean the same thing (mostly
>using "tree" because the terminology is better established, eg "rational
>trees"). With this meaning groundness applies to terms = trees, not
>representations = pointers etc. I guess my post didn't make this clear.
OK. This kind of trees are sensible from a computer science point of view
as representations of the mathematical "infinite trees".
Since they can contain variables the notion of "groundness" has a meaning.
Lee Naish
I'm starting to wonder if this thread is finite. I hope its more intersting
than MAKE MONEY FAST spams and flames at least...
In article <ALF.96Ju...@mut.sics.se>, a...@sics.se (Thomas Sjöland) writes:
> >I disagree. I was using "tree" and "term" to mean the same thing (mostly
> OK. This kind of trees are sensible from a computer science point of view
> as representations of the mathematical "infinite trees".
> Since they can contain variables the notion of "groundness" has a meaning.
f(f(f(f(f(...... has the same number of variables as f(a), ie, zero. Both
terms may have been constructed using variables along the way. In Sicstus
(and most, but not all Prolog systems) the infinite term must have been
constructed with variables because Sicstus does not support a syntax for
infinte terms. There is no reason why a syntax such as f(g(h(@2)) should
not be provided for the term f(g(h(g(h(g(h(.... (the "@2" is a shorthand for
the tree two levels up, or speaking in terms of representation, a pointer
to the "g" node).
In fact (Mats is going to hate me for this:) there is no reason why this
syntax could not be supported in Sicstus via term_expansion. Of course
the current compiler may not have been written with infinite terms/cyclic
structures in mind.
In your average Prolog system you have to think at a very low level if you
want to play around with cyclic structures. I have set projects involving
creation and traversal of threaded trees in Prolog to test if my Logic
Programming Techniques students understand the WAM etc. In Sicstus you
can think at a slightly higher level because the unification algorithm
works for cyclic structures. However, there are many more things that could
be supported, including input and output of infinite terms and inequality of
infinite terms (which is what started this thread).
lee
Thomas Sjöland
>I'm starting to wonder if this thread is finite. I hope its more intersting
>than MAKE MONEY FAST spams and flames at least...
Don't worry, there is always the n key for those who want
exciting entertainment.
>There is no reason why a syntax such as f(g(h(@2)) should
>not be provided for the term f(g(h(g(h(g(h(.... (the "@2" is a shorthand
>for the tree two levels up, or speaking in terms of representation, a
>pointer to the "g" node).
You support the idea that "trees" are always ground,
thereby making the notion of groundness meaningless for "trees", since
variables are not an essential part of the "abstract" trees
represented by them, and don't need to be in the syntax expressing them
either. We seem to agree more and more for each iteration:).
>In Sicstus you can think at a slightly higher level because the
>unification algorithm works for cyclic structures. However, there are
>many more things that could be supported, including input and output of
>infinite terms and inequality of infinite terms (which is what started
>this thread).
Let me try some CLP/CCLP-theology here: (theory nitpicker asbestos suit on)
The right way to think of the desired "declarative" behaviour of the
built-ins is to think of them as monotonically forming a constraint
store over a domain of rational trees (or other constraint domains if
you have a more advanced CLP/CCLP-system). If B(C) is a builtin
constraint literal that holds for a constraint store C (i.e. a
conjunction of constraint literals) it should hold also for any store
C' such that C' |= C
Bernhard Pfahringer
Just to keep the 'infinite..' thread from extinction :-)
Thomas' Solution seems buggy, at least the following query loops
(on my system):
| ?- t1(X,Y), q(f(X),f(Y)).
I think it is still possible to define a 'depth-first' ordering compatible
with current compare/3 behavior for finite trees. The following is an
attempt relying on Sicstusprolog's ability to test ==/2 and \==/2 of
rational trees. It is of course inefficient for large, but almost identical
trees.
compare1(O,A,B) :- A == B, !, O = '='.
compare1(O,A,B) :- compound(A),compound(B),!, compare2(O,A,B),!.
compare1(O,A,B) :- compare(O,A,B).
compare2(O,A,B) :- compare_toplevel(O,A,B),!.
compare2(O,A,B) :-
compound(A),
functor(A,_,N),
for(I,1,N),
arg(I,A,Ai),
arg(I,B,Bi),
Ai \== Bi,
compare2(O,Ai,Bi).
compare_toplevel(O,A,B) :-
get_toplevel(A,A1),
get_toplevel(B,B1),
compare(O,A1,B1),
O \== '='.
get_toplevel(A,F-N) :- compound(A),!,functor(A,F,N).
get_toplevel(A,A).
for(_,I,N) :- I>N,!,fail.
for(X,X,_).
for(X,I,N) :- I1 is I + 1, for(X,I1,N).
For efficiency reasons compare/3 should be implemented as a builtin.
The pseudo-Prolog specification for a rational tree-savy behavior of
a builtin rt_compare/3 could look like the following. It assumes that
internally structures are 'markable', 'marks' are undone both on
backtracking and also explicitly by appropriate primitives:
rt_compare(O,A,B) :- compare_compound(O,A,B),!,unmark(A),unmark(B).
rt_compare(=,_,_).
compare_compound(O,A,B) :- compare_toplevel(O,A,B),!.
compare_compound(O,A,B) :-
compound(A),
compound(B),
at_least_one_not_marked(A,B),
mark_both(A,B),
functor(A,_,N),
for(I,1,N),
arg(I,A,Ai),
arg(I,B,Bi),
compare_compound(O,Ai,Bi).
This solution should be both efficient and compatible.
Peter Van Roy
<4t9c8h$r...@mulga.cs.mu.OZ.AU>
Organization: DFKI - German Research Center for Artificial Intelligence
Keywords:
Lee Naish writes:
> There is no reason why a syntax such as f(g(h(@2)) should
> not be provided for the term f(g(h(g(h(g(h(.... (the "@2" is a shorthand for
> the tree two levels up, or speaking in terms of representation, a pointer
> to the "g" node).
Actually, I prefer Wild_Life's syntax, which gives X:f(g(X)).
It is possible to tag any node with a variable name. It is like
allowing the expression V=Term *inside* of any term. It requires
minimal extension to Prolog--just pick an operator that resembles '='.
> In fact (Mats is going to hate me for this:) there is no reason why this
> syntax could not be supported in Sicstus via term_expansion.
It is very convenient to be able to represent textually any term including both
cyclic terms *and* terms with *shared* subterms. The 'X:' notation given above
handles both easily, which is not so easy with the '@2' notation.
Consider A=[B|B], B=[C|C], C=[D|D], ..., Y=[Z|Z]. Writing A uses rather less
space if sharing can be represented :-).
Peter
Thomas Sjöland
In article <4tiju5$1u...@www.univie.ac.at> bern...@doebling.ai.univie.ac.at (Bernhard Pfahringer) writes:
>Thomas' Solution seems buggy, at least the following query loops
>(on my system):
>
>| ?- t1(X,Y), q(f(X),f(Y)).
>
Indeed. I can't understand how it worked on any examples at all...
I should have tested some more. Thanks for pointing it out.
>I think it is still possible to define a 'depth-first' ordering compatible
>with current compare/3 behavior for finite trees. The following is an
>attempt relying on Sicstusprolog's ability to test ==/2 and \==/2 of
>rational trees. It is of course inefficient for large, but almost identical
>trees.
[snipped out code]
Looks nice, but I couldn't get it to give a result on any of my examples
with infinite rational trees... Perhaps I destroyed it in the process.
But anyway, here a is my second, last, and hopefully more intelligible
attempt at some code for this purpose.
%----- ----- ----- ----- ----- ----- ----- ----- ----- ----- ----- -----
/*
Below is a version of compare/3, called compare0/3,
that performs an iterative deepening based search.
It is considerably slower than compare/3, and also generates
a substantial number of gc-s when applied to large structures.
Hope you don't find a bug :-)
*/
% iterative deepening version of compare/3
% that is "stable" over unfolding of ground circular terms
% and that doesn't construct new terms
% TS, 960803
test1p :- (t1(X,Y) ; t1u(X,Y)), p(X,Y).
test1q :- (t1(X,Y) ; t1u(X,Y)), q(X,Y).
test2p :- (t2(X,Y) ; t2u(X,Y)), p(X,Y).
test2q :- (t2(X,Y) ; t2u(X,Y)), q(X,Y).
test3p :- (t1(X,Y) ; t1u(X,Y)), p(f(X),f(Y)).
test3q :- (t1(X,Y) ; t1u(X,Y)), q(f(X),f(Y)).
% D is the "depth" of the generated infinite tree
test4p(D) :- (t1(X,Y) ; t1u(X,Y)), tree(D,X,TX), tree(D,Y,TY), p(TX,TY).
test4q(D) :- (t1(X,Y) ; t1u(X,Y)), tree(D,X,TX), tree(D,Y,TY), q(TX,TY).
% D is the "depth" of the generated infinite tree
test5p(D) :- tree(D,foo(X),X), tree(D,bar(Y),Y), p(X,Y).
test5q(D) :- tree(D,foo(X),X), tree(D,bar(Y),Y), q(X,Y).
% D is the "depth" of the generated infinite tree
test6p(D) :- tree(D,foo(Y),X), tree(D,bar(X),Y), p(X,Y).
test6q(D) :- tree(D,foo(Y),X), tree(D,bar(X),Y), q(X,Y).
%iterates with successively deeper trees until there is no more memory
%and prints level at backtracking
foo5 :- level(D), write(D),nl, test5p(D).
bar5 :- level(D), write(D),nl, test5q(D).
%iterates with successively deeper trees until there is no more memory
%and prints level at backtracking
foo6 :- level(D), write(D),nl, test6p(D).
bar6 :- level(D), write(D),nl, test6q(D).
%----- end of test examples ------------------------------------------------
p(A,B) :- compare(O,A,B), write(O),nl,fail.
q(A,B) :- compare0(O,A,B), write(O),nl,fail.
t1(A,B) :- A=s(B,1), B=s(A,0).
t1u(A,B) :- A=s(s(A,0),1), B=s(s(B,1),0).
t2(A,B) :- A=s(B,A,1), B=s(A,B,0).
t2u(A,B) :- A=s(s(A,B,0),A,1), B=s(s(B,A,1),B,0).
tree(0,X,Tree) :- !, X=Tree.
tree(I,Leaf,t(T1,T2)) :-
I>0,
I0 is I-1,
tree(I0,Leaf,T1),
tree(I0,Leaf,T2).
%----- end of help code for the examples -----------------------------------
compare0(O,A,B) :-
A==B,
!, O='='.
compare0(O,A,B) :- % non-equal compound terms
compound(A),
compound(B),
!, level(L),
cmpterm(L,O,A,B),
\+ O='=',
!.
compare0(O,A,B) :- compare(O,A,B). % other cases as usual
level(1).
level(L) :- level(L0), L is L0+1.
cmpterm(L,O,A,B) :-
compound(A),
compound(B),
!,
(L=0 ->
O='=' % reached level 0
; % above level 0
functor(A,Na,Ia),
functor(B,Nb,Ib),
compare(Of,Na/Ia,Nb/Ib),
(Of='=' ->
cmpargs(L,O,A,B,Ia)
;
O=Of
)
).
cmpterm(_L,O,A,B) :- % other cases as usual
!, compare(O,A,B).
cmpargs(_L,O,_A,_B,0) :-
!, O='='.
cmpargs(L,O,A,B,I) :-
arg(I,A,Ai),
arg(I,B,Bi),
L0 is L-1,
cmpterm(L0,Oi,Ai,Bi),
(Oi='=' ->
I0 is I-1,
cmpargs(L,O,A,B,I0)
;
O=Oi).
Bernhard Pfahringer
What you've said about your code is true for mine, too:
>Indeed. I can't understand how it worked on any examples at all...
>I should have tested some more. Thanks for pointing it out.
But my point is still: You can do it DEPTH-FIRST!
Here comes the corrected code (needs Sicstus!):
compare1(O,A,B) :- A == B, !, O = '='.
compare1(O,A,B) :- compound(A),compound(B),!, compare2(O,A,B,[A-B]),!.
compare1(O,A,B) :- compare(O,A,B).
compare2(O,A,B,_) :- compare_toplevel(O,A,B),!.
compare2(O,A,B,Stack) :-
compound(A),
functor(A,_,N),
for(I,1,N),
arg(I,A,Ai),
arg(I,B,Bi),
\+ looping(Ai-Bi,Stack),
compare2(O,Ai,Bi,[Ai-Bi|Stack]).
compare_toplevel(O,A,B) :-
get_toplevel(A,A1),
get_toplevel(B,B1),
compare(O,A1,B1),
O \== '='.
get_toplevel(A,F-N) :- compound(A),!,functor(A,F,N).
get_toplevel(A,A).
for(_,I,N) :- I>N,!,fail.
for(X,X,_).
for(X,I,N) :- I1 is I + 1, for(X,I1,N).
looping(X,[Y|_]) :- X == Y.
looping(X,[_|L]) :- looping(X,L).
Now your test examples (and hopefully all other comparisons) work:
test1 :- (t1(X,Y) ; t1u(X,Y)), p(X,Y).
test2 :- (t2(X,Y) ; t2u(X,Y)), p(X,Y).
p(A,B) :- compare1(O,A,B), write(O),nl,fail.
t1(A,B) :- A=s(B,1), B=s(A,0).
t1u(A,B) :- A=s(s(A,0),1), B=s(s(B,1),0).
t2(A,B) :- A=s(B,A,1), B=s(A,B,0).
t2u(A,B) :- A=s(s(A,B,0),A,1), B=s(s(B,A,1),B,0).
| ?- test1.
<
<
no
| ?- test2.
<
<
no
Bernhard
Mostowski Collapse
might not be aware of it. But it made it even into Prolog system
documentation, like here:
"Please note : the standard order is only well-defined for finite (acyclic) terms.
There are infinite (cyclic) terms for which no order relation holds."
https://sicstus.sics.se/sicstus/docs/3.12.11/html/sicstus/Term-Compare.html
And here is a funny disagreement between two Prolog systems,
an old lady (SWI-Prolog) and a youngster (Scryer Prolog):
/* SWI-Prolog 9.1.7 */
?- X=f(X,a(X)), Y=f(Y,b(Y)), Z=f(Y,c(Y)),
compare(A,X,Y), compare(B,Y,Z), compare(C,X,Z).
A = B, B = (<),
C = (>).
/* Scryer Prolog 0.9.1-194 */
?- X=f(X,a(X)), Y=f(Y,b(Y)), Z=f(Y,c(Y)),
compare(A,X,Y), compare(B,Y,Z), compare(C,X,Z).
A = (<), B = (<), C = (<).
Mats Carlsson schrieb am Dienstag, 16. Juli 1996 um 09:00:00 UTC+2:
> algorithms for unification without occurs check that could work
> with infinite (cyclic) terms with termination guaranteed.
> Until yesterday, I always believed that the standard total order for
> finite Prolog terms readily extended to include infinite terms as
> well. However, the following example shows two terms that can't be
> ordered.
> [1] A = s(B,0).
> [2] B = s(A,1).
> Clearly, A and B are not identical, so is A @< B or A @> B?
Mostowski Collapse
my X,Y,Z tripple. This is a counter example for unstable
keysort, using @ridgeworks new_compare/2.
Lets define unstable_keysort/2 as follows:
unstable_keysort(L, R) :- predsort(new_compare, L, R).
I can now use unstable_keysort/2 and as expected and
useful for setof/3 implementation, it gives me ascending
order of the values for equal keys:
?- unstable_keysort([x-3,x-1,x-2,x-1], L).
L = [x-1, x-2, x-3].
?- predsort(new_compare, [3,1,2,1], L).
L = [1, 2, 3].
Now using the new counter example. The key X is such
that it mimics a pair, confusing acyclic_rep/2 inside
new_compare/2. It breaks the ascending order property:
?- X=(X-b(X)), unstable_keysort([X-b(X), X-a(X)], L).
X = X-b(X),
L = [X-b(X), X-a(X)].
?- X=(X-b(X)), predsort(new_compare, [b(X), a(X)], L).
X = X-b(X),
L = [a(X), b(X)].
Mostowski Collapse
Wiithout loss of generality its enough to handle the case
Lab, although Matt Carlson mentioned both proofs:
/* Lexical Ordering */
∀x∀y∀z∀t(Ls(x,y)s(z,t) ↔ (Lxz ∨ (x=z ∧ Lyt))),
/* Example A,B satisfies A @< B and ~(B @< A) */
Lab, ¬Lba,
/* Example A,B is A=s(B,c) and B=s(A,d), proof works for any c,d */
a=s(b,c), b=s(a,d)
/* We can derive a Contradiction */
entails p∧¬p.
https://www.umsu.de/trees/#~6x~6y~6z~6t(Ls(x,y)s(z,t)~4Lxz~2(x=z~1Lyt)),Lab,~3Lba,a=s(b,c),b=s(a,d)
The consistency means unless hell freezes over,
we can never find a less than relationship L.
Mostowski Collapse
The inconsistency means unless hell freezes over,
Mostowski Collapse
https://www.umsu.de/trees/#~6x~6y~6z~6t(Ls(x,y)s(z,t)~4Lxz~2(x=z~1Lyt)),Lab,~3Lba,a=s(b,c),b=s(a,d)|=p~1~3p
Got somehow cropped, hope this one works now?
Mostowski Collapse
laws, except lexical order. It is based on the idea to define:
S @<' T :<=> rep(S) @< rep(T)
The only requirement to the function rep is that it is injective,
then the laws, except for lexical order, are automatically satisfied.
The proof is not so difficult. Here is an example proof, showing
irreflexivity of @<’ based on irreflexivity of @<:
/* I am using r for the function rep,
R for the relation @<' and L for the relation @< */
/* Injectivity */
∀x∀y(r(x)=r(y) → x=y),
/* Bootstrapping */
∀x∀y(Rxy ↔ Lr(x)r(y)),
/* Irreflexivity */
∀x¬Lxx
/* Irreflexivity */
entails ∀x¬Rxx.
https://www.umsu.de/trees/#~6x~6y(r(x)=r(y)~5x=y),~6x~6y(Rxy~4Lr(x)r(y)),~6x(~3Lxx)%7C=~6x(~3Rxx)
Mostowski Collapse
rep(X, Y-Z) :-
term_factorized(X, Y, Z),
numberassoc(Z, 0).
numberassoc([], _).
numberassoc(['$VAR'(N)=_|L], N) :-
M is N+1,
numberassoc(L, M).
And then the comparator:
rep_compare(C, X, Y) :-
rep(X, A), rep(Y, B),
compare(C, A, B).
Any bugs? It requires that term_factorized/3 is stable and it works
only for terms that don’t have already ‘$VAR’/1 in it. Might need to
use something else, but with ‘$VAR’/1 rep/2 can be easily inspected.
Mostowski Collapse
?- A=(B,0), B=(A,1), predsort(rep_compare, [A,B], X),
term_factorized(X, P, Q).
P = [_A, _B],
Q = [_B=(_A, 0), _A=(_B, 1)].
?- A=(B,0), B=((B,0),1), predsort(rep_compare, [B,A], X),
term_factorized(X, P, Q).
P = [_A, _B],
Q = [_B=(_A, 0), _A=(_B, 1)].
And the tripple X,Y,Z that has a bug in native compare/3, the bug is gone:
?- X=f(X,a(X)), Y=f(Y,b(Y)), Z=f(Y,c(Y)),
rep_compare(A,X,Y), rep_compare(B,Y,Z), rep_compare(C,X,Z).
A = B, B = C, C = (<)
Mostowski Collapse
shows me a proof using injectivity in Wolfgang Schwartz tree tool:
/* I am using r for the function rep,
R for the relation @<' and L for the relation @< */
/* Injectivity */
∀x∀y(r(x)=r(y) → x=y),
/* Bootstrapping */
∀x∀y(Rxy ↔ Lr(x)r(y)),
∀x∀y(¬x=y → (Lyx ∨ Lxy))
/* Connectedness */
entails ∀x∀y(¬x=y → Ryx ∨ Rxy)
https://www.umsu.de/trees/#~6x~6y(r(x)=r(y)~5x=y),~6x~6y(Rxy~4Lr(x)r(y)),~6x~6y(~3x=y~5Lyx~2Lxy)%7C=~6x~6y(~3x=y~5Ryx~2Rxy)
Mostowski Collapse
mathematical proofs, one can also use the validation path.
What helps is this fuzzer:
% random_cyclic(-Term)
random_cyclic(T) :-
random_cyclic([T], T).
% random_cyclic(+List, -Term)
random_cyclic(L, T) :-
length(L, M),
random(R),
N is truncate(R*(M+3)),
(N = 0 -> T = 0;
N = 1 -> T = 1;
N = 2 -> T = s(P,Q), random_cyclic([P|L], P), random_cyclic([Q|L], Q);
K is N-3, nth0(K, L, S), S=T).
Now I found that term_factorized/3 might run into
a stack overflow. The reason could be the buggy
compare/3, in case it is used in rbtrees:
?- aggregate_all(count, (between(1,1000000,_), random_cyclic(A),
random_cyclic(B), random_cyclic(C), rep_less(A,B),
rep_less(B,C), \+ rep_less(A,C)), F).
ERROR: Stack limit (1.0Gb) exceeded
ERROR: Stack sizes: local: 0.7Gb, global: 0.2Gb, trail: 1Kb
ERROR: Stack depth: 12,882,088, last-call: 50%, Choice points: 6
ERROR: In:
ERROR: [12,882,088] rbtrees:lookup(<compound s/2>,
_64416492, <compound black/4>)
ERROR: [12,882,086] terms:insert_vars(<compound s/2>,
_64416526, <compound t/2>)
Mostowski Collapse
overflow when I use a ground term:
/* SWI-Prolog 9.1.7 */
?- T = _S1, % where
_S1 = s(s(_S1, _S2), 0),
_S2 = s(_S2, _S1), term_factorized(T, Y, L).
terms, it sadly happens for ground terms as well.
Mostowski Collapse
mirror anomaly. I find very quickly a violation of the mirror law:
/* SWI-Prolog 9.1.7 */
?- repeat, random_cyclic(A), random_cyclic(B),
compare(X,A,B), X = (<), \+ (compare(Y,B,A), Y = (>)).
A = s(A, A),
B = s(_S1, 1), % where
_S1 = s(_S1, s(1, _S1)),
X = (<) .
Mostowski Collapse
term_factorized/3 which unfortunately gives a stack
overflow sometimes? Of course:
% naish(+Term, -Termt)
naish(T, S) :-
naish(T, [], S).
% naish(+Term, +Map, -Term)
naish(T, _, T) :- \+ compound(T), !.
naish(T, C, '\a'(N)) :- nth0(N, C, S), S == T, !.
naish(T, C, S) :-
T =.. [F|L],
naish_list(L, [T|C], R),
S =.. [F|R].
% naish_list(+List, +Map, -List)
naish_list([], _, []).
naish_list([X|L], C, [Y|R]) :-
naish(X, C, Y),
naish_list(L, C, R).
Works fine:
?- A=(B,0), B=(A,1), naish(A, X).
X = (('\a'(1), 1), 0).