How to use call_with_depth_limit/3

Question

I'm trying to use call_with_depth_limit/3 in SWI-Prolog to implement iterative deepening and either I don't understand how it works or it's misbehaving. I have an example where the following happens:

?- 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.

According to the documentation it should succeed if the goal can be proved with Limit max recursion or less. In the first call with limit 30 we see results where the Result is 25, therefore I would expect that calling it with a limit of 26 it would succeed. I'm using constraint handling rules in the module, in case there can be some interaction there that makes it misbehave.

EDIT: After playing with Isabelle's answer I think I understand how it behaves:

• It runs a depth first search like usual but if it gets to Limit+1 depth it acts as if it failed.
• Failed branches count towards the Result.
• Every time it backtracks after a successful answer, it resets Result to the current depth of the stack.

See this example:

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

I'm not convinced that SWI-Prolog even implements its own specification for call_with_depth_limit/3. At least I read:

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

as implying that Result will never be greater than Limit. But with this program:

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

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

I observe (SWI-Prolog 7.6.4):

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

Proving the shallower goal results in a deeper recursion. A recursion that exceeds the limit but still succeeds.

Personally, reading the documentation I would expect to get the same depth for proving succeed_with_depth(1) on backtracking as when calling it directly:

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

Or maybe add 1 depth for backtracking at the outermost level of succeed_with_depth? That should still give Result = 4 and not 6.

Edit: As pointed out by rajashekar in the comments, adding a cut in the first clause of succeed/1 changes the unexpected behavior the the expected one. I see this as further indication that SWI-Prolog's behavior is broken: The only difference is cutting away a choice that on backtracking will immediately fail. There is no actual deeper recursion in any succeeding computation.

Edit 2: To illustrate that the semantics I am imagining for this is simple, and that it can actually be used to implement iterative deepening, here is a small meta-interpreter that is just strong enough to execute my program from above:

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

This doesn't retain depth information across backtracking, so behavior on backtracking is the same as when calling more specific instances of the goal:

?- 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.

Iterative deepening, finding each answer exactly once and in the proper order (i.e., shallowest proofs first), is then:

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

Test:

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

I don't think anything can be done about the nontermination; you would usually use this on goals that have an infinite number of answers.

Answer 2

I've tried to understand how call_with_depth_limit/3 works by using this program:

%           a        <- 1st call
%         /   \
%        b     g     <- 2nd call
%       /
%      c             <- 3rd call
%     / \
%    g   d           <- 4th call
%        |
%        e           <- 5th call

arc(a, b).
arc(a, g).
arc(b, c).
arc(c, g).
arc(c, d).
arc(d, e).

path(X, X, [X]).
path(X, Z, [X|R]) :- arc(X, Y), path(Y, Z, R).

Results obtained:

?- call_with_depth_limit(path(a,g,P), 4, D).
P = [a, b, c, g],
D = 4 ;
P = [a, g],
D = 5 ;
false.

It seems that the answer:

• P = [a, b, c, g], D = 4 means 4 calls to obtain the first solution.
• P = [a, g], D = 5 means 5 calls to obtain the second solution (notice that, before obtain this second solution, the failure path [a,b,c,d,e] must be explored and the 5th call causes a failure - this fact justifies the answer D = 5).

Another query:

?- call_with_depth_limit(path(a,g,P), 3, D).
P = [a, g],
D = 4 ;
false.

We can see that the search backtracks after 4 calls (D = 4), but the fourth call needed to obtain the solution [a,b,c,g] causes a failure (because depth_limit is 3) and does not produce a result.

[EDIT] Another scenario: In this new scenario, a cut was added in the first clause of the predicate path/3 to avoid the extension of a path which is already a solution (otherwise, the search will try one more step downward in this same path and will fail with depth 5 before finding the second solution).

%           a        <- 1st call
%         /   \
%        b     g     <- 2nd call
%       /
%      c             <- 3rd call
%     /
%    g               <- 4th call
%
%                    <- 5th call

arc(a, b).
arc(a, g).
arc(b, c).
arc(c, g).

path(X, X, [X]) :- !.
path(X, Z, [X|R]) :- arc(X, Y), path(Y, Z, R).

In this new scenario, we have:

?- call_with_depth_limit(path(a,g,P), 4, D).
P = [a, b, c, g],
D = 4 ;
P = [a, g],
D = 2.

We observe that:

• In this second scenario, the deepest recursion level reached to find the second solution is 2.

• However, in the first scenario, the deepest recursion level to find the second solution is 5 because, before finding the second solution, the search must try to extend path [a,b,c,g] and also explore the path [a,b,c,d,e] (hence, the deepest recursion level used during the proof of solution [a,g]is 5).

It is important to notice that, as stated in SWI-Prolog documentation, the Result is bound to the deepest recursion level used during the proof of a particular solution, not to the level in which this solution is found.

call_with_depth_limit(:Goal, +Limit, -Result) 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, or the entire predicate fails if Goal fails without exceeding Limit.

Iterative deepening depth-first search

Find a shallowest solution for Goal, without exceeding Limit:

ids(Goal, Limit) :-
    between(1, Limit, Depth),
    call_with_depth_limit(Goal, Depth, Result),
    Result \= depth_limit_exceeded,
    !.

Here are some examples (same answers for both scenarios):

?- ids(path(a,g,P), inf).
P = [a, g].

?- ids(path(a,g,P), 10).
P = [a, g].

?- ids(path(a,g,P), 2).
P = [a, g].

?- ids(path(a,g,P), 1).
false.

Answer 3

Isn't it just that for the first successful result you need a depth of 29, which is evidently excessive, and then it blows? Then the next result for which you need a depth of 25 will never be attempted.