Tree methods going on infinite loop

Viewed 158

So all of my tree code is not working properly when I instantiate my integer variables. Here's an example of what I mean:

% relates a tree and the numbe of nodes in that tree(order)
tree_order(empty,0).
tree_order(tree(_, Left_Subtree, Right_Subtree), Order) :- 
    Order #> 0,
    Order #= Left_Subtree_Order + Right_Subtree_Order + 1,
    tree_order(Left_Subtree, Left_Subtree_Order), tree_order(Right_Subtree, Right_Subtree_Order).

I'm not actually using that but here's my definition of a tree:

% Definition of a Binary Tree

tree(empty).
tree(tree(_, Left_Subtree, Right_Subtree)) :- 
    tree(Left_Subtree), tree(Right_Subtree).

So if run the following query tree_order(Tree, 2). it gives me a solution then when it backtracks it goes on an infinite loop. It's honestly baffling me, because I've run the program in my head a thousand times and I still can't find an answer.

One possibility is that Prolog is adding infinitely many nodes to the left of the tree and it doesn't realize that it actually leads to the tree having order greater than 2.

But if that's the case, how can I tell prolog to stop adding more than 2 nodes to the tree? I've thought about using CLP but the only methods I know reason about numerical domains and lists but not predicates.

Thanks in advance!

2 Answers

The reason for non-termination of tree_order(T, 2). is the following :

tree_order(empty,0) :- false.
tree_order(tree(_, Left_Subtree, Right_Subtree), Order) :- 
    Order #> 0,
    Order #= Left_Subtree_Order + Right_Subtree_Order + 1,
    tree_order(Left_Subtree, Left_Subtree_Order), false,
    tree_order(Right_Subtree, Right_Subtree_Order).

?- tree_order(T, 2).
   loops.

In order to make this terminating, you need to specialize this program somehow. Like by adding T = tree(_,empty,empty) in front of the query.

Or by adding the redundant constraint Right_Subtree_Order #>=0.

Note that strictly speaking, this is no longer an example of finite domains but rather (potentially) infinite domains. Not all clpfd implementations support this. SICStus, Scryer, and SWI do support it. But only in Scryer and SWI does unification of such terms always terminate.

Better to constraint every free variable involved:

/*  File:    tree_order.pl
    Author:  Carlo,,,
    Created: Oct 19 2021
    Purpose: https://stackoverflow.com/q/69623834/874024
*/

:- module(tree_order,
          [tree_order/2
          ]).
:- use_module(library(clpfd)).

% relates a tree and the number of nodes in that tree(order)
tree_order(empty, 0).
tree_order(tree(_, Left_Subtree, Right_Subtree), Order) :-
    % Order #> 0, implicit given the following 3 constraints
    Left_Subtree_Order #>= 0,
    Right_Subtree_Order #>= 0,
    Order #= Left_Subtree_Order + Right_Subtree_Order + 1,
    tree_order(Left_Subtree, Left_Subtree_Order),
    tree_order(Right_Subtree, Right_Subtree_Order).

yields

[debug]  ?- tree_order(T,2).
T = tree(_, empty, tree(_, empty, empty)) ;
T = tree(_, tree(_, empty, empty), empty) ;
false.
Related