prolog - 如何使用 call_with_depth_limit/3

Question

我正在尝试使用 call_with_depth_limit/3 在 SWI-Prolog 中实现迭代深化，要么我不明白它是如何工作的，要么它行为不端。我有一个发生以下情况的示例:

?- call_with_depth_limit(mygoal, 29, Result).
Result = 29 ;
Result = 25 ;
Result = 27 ;
Result = 27 ;
false.

?- call_with_depth_limit(mygoal, 26, Result).
Result = depth_limit_exceeded ;
false.

根据文档，如果可以使用 Limit max recursion 或更少来证明目标，它应该会成功。在第一个限制为 30 的调用中，我们看到 Result 为 25 的结果，因此我希望以 26 的限制调用它会成功。
我在模块中使用约束处理规则，以防那里可能存在一些使其行为不端的交互。
编辑:玩过伊莎贝尔的回答后，我想我明白它的行为方式:

它像往常一样运行深度优先搜索，但如果它达到 Limit+1 深度，它就像失败一样。

失败的分支计入结果。

每次它在成功回答后回溯时，都会将 Result 重置为堆栈的当前深度。

看这个例子:

loop :- loop.

succeed(0).
succeed(N) :- N > 0, N1 is N - 1, succeed(N1).

fail(N) :- N > 0, N1 is N - 1, fail(N1).

?- call_with_depth_limit(succeed(0), 1000, Result).
Result = 1 ;
false.

?- call_with_depth_limit(fail(50);succeed(0), 1000, Result).
Result = 53 ;
false.

% It tries loop until Limit+1 and therefore this is the Result
?- call_with_depth_limit(loop;succeed(0), 1000, Result).
Result = 1001 ;
false.

% In the second result it has to unroll the stack from 100 before trying the next, so Result is 100.
?- call_with_depth_limit(loop;succeed(100);succeed(0), 1000, Result).
Result = 1001 ;
Result = 103 ;
false.

?- call_with_depth_limit(loop;succeed(0);succeed(0), 1000, Result).
Result = 1001 ;
Result = 3 ;
false.

% If it gets to the end, and it has reached Limit+1 since the last successful result it returns depth_limit_exceeded.
?- call_with_depth_limit(loop;succeed(100);succeed(0);loop, 1000, Result).
Result = 1001 ;
Result = 103 ;
Result = depth_limit_exceeded.

Answer 1

我不相信 SWI-Prolog 甚至实现了自己的 call_with_depth_limit/3 规范。 .至少我读到:

If Goal can be proven without recursion deeper than Limit levels, call_with_depth_limit/3 succeeds, binding Result to the deepest recursion level used during the proof. Otherwise, Result is unified with depth_limit_exceeded if the limit was exceeded during the proof...

暗示 Result永远不会大于 Limit .但是有了这个程序:

succeed_with_depth(3) :-
    succeed(3).
succeed_with_depth(1) :-
    succeed(1).

succeed(0).
succeed(N) :-
    N > 0,
    N1 is N - 1,
    succeed(N1).

我观察到(SWI-Prolog 7.6.4):

?- call_with_depth_limit(succeed_with_depth(N), 5, Result).
N = 3,
Result = 5 ;
N = 1,
Result = 6 ;
false.

证明更浅的目标会导致更深的递归。超出限制但仍然成功的递归。
就个人而言，阅读文档我希望获得相同的深度来证明 succeed_with_depth(1)在直接调用时回溯:

?- call_with_depth_limit(succeed_with_depth(1), 5, Result).
Result = 3 ;
false.

或者可以在 succeed_with_depth 的最外层添加 1 个深度用于回溯?那仍然应该给 Result = 4而不是 6 .
编辑:正如 rajashekar 在评论中指出的那样，在 succeed/1 的第一条中添加了一个删减。将意外行为更改为预期行为。我认为这进一步表明 SWI-Prolog 的行为已被破坏:唯一的区别是删除了一个在回溯时将立即失败的选择。在任何后续计算中都没有实际的更深层次的递归。
编辑 2 :为了说明我为此想象的语义很简单，并且它实际上可以用于实现迭代深化，这里有一个小的元解释器，它的强度足以从上面执行我的程序:

interpret_with_depth_limit(Goal, Limit, Result) :-
    interpret_with_depth_limit(Goal, 0, Limit, Result).

interpret_with_depth_limit(_Goal, Current, Limit, depth_limit_exceeded) :-
    Current >= Limit,
    !.
interpret_with_depth_limit(Builtin, N, _Limit, N) :-
    builtin(Builtin),
    !,
    call(Builtin).
interpret_with_depth_limit((A, B), N, Limit, Result) :-
    !,
    interpret_with_depth_limit(A, N, Limit, ResultA),
    integer(ResultA),
    interpret_with_depth_limit(B, N, Limit, ResultB),
    integer(ResultB),
    Result is max(ResultA, ResultB).
interpret_with_depth_limit(Goal, N, Limit, Result) :-
    N1 is N + 1,
    N1 < Limit,
    clause(Goal, Body),
    interpret_with_depth_limit(Body, N1, Limit, Result).

builtin(true).
builtin(_ > _).
builtin(_ is _).

这不会在回溯中保留深度信息，因此回溯的行为与调用更具体的目标实例时相同:

?- interpret_with_depth_limit(succeed_with_depth(N), 6, Result).
N = 3,
Result = 5 ;
N = 1,
Result = 3 ;
false.

?- interpret_with_depth_limit(succeed_with_depth(3), 6, Result).
Result = 5 ;
false.

?- interpret_with_depth_limit(succeed_with_depth(1), 6, Result).
Result = 3 ;
false.

迭代深化，以正确的顺序准确地找到每个答案一次(即，首先是最浅的证明)，然后是:

call_succeedingdepth(Goal, Depth) :-
    between(1, infinite, Limit),
    Depth is Limit - 1,
    interpret_with_depth_limit(Goal, Limit, Depth).

测试:

?- call_succeedingdepth(succeed_with_depth(N), Depth).
N = 1,
Depth = 3 ;
N = 3,
Depth = 5 ;
% nontermination

我不认为关于不终止的事情可以做任何事情。你通常会在有无数个答案的目标上使用它。