无限循环的树方法

Question

所以当我实例化我的整数变量时，我所有的树代码都不能正常工作。这是我的意思的一个例子：

% 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).

我实际上并没有使用它，但这是我对树的定义：

% Definition of a Binary Tree

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

所以如果运行下面的查询 tree_order(Tree, 2). 它给了我一个解决方案，那么当它回溯时它会进入无限循环。老实说，这让我很困惑，因为我已经运行这个程序在我脑海里想了一千遍了，但我仍然找不到答案。

一种可能是 Prolog 在树的左侧添加了无限多的节点，但它没有意识到这实际上导致树的阶数大于 2。

但如果是这样的话，我如何告诉 prolog 停止向树中添加 2 个以上的节点？我考虑过使用 CLP，但我知道的唯一方法是关于数字域和列表而不是谓词。

提前致谢！

Answer 1

最好限制涉及的每个自由变量：

/*  File:    tree_order.pl
    Author:  Carlo,,,
    Created: Oct 19 2021
    Purpose: 
*/

:- 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).

产量

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

Answer 2

tree_order(T, 2).未终止的原因如下failure-slice:

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*

为了终止此程序，您需要以某种方式专门化此程序。就像在查询前面添加T = tree(_,empty,empty)。

或者通过添加冗余约束 Right_Subtree_Order #>=0.

请注意，严格来说，这不再是 有限域 的示例，而是（可能）无限域。并非所有 clpfd 实现都支持这一点。 SICStus、Scryer 和 SWI 都支持它。但只有在 Scryer 和 SWI 中，此类术语的统一才会终止。

无限循环的树方法

Tree methods going on infinite loop

prolog

clpfd