call_with_depth

Availability:built-in

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.

The depth limit is guarded by the internal machinery. This may differ from the depth computed based on a theoretical model. For example, true/0 is translated into an inline virtual machine instruction. Also, repeat/0 is not implemented as below, but as a non-deterministic foreign predicate.

repeat.
repeat :-
        repeat.

As a result, call_with_depth_limit/3 may still loop infinitely on programs that should theoretically finish in finite time. This problem can be cured by using Prolog equivalents to such built-in predicates.

This predicate may be used for theorem provers to realise techniques like iterative deepening. See also call_with_inference_limit/3. It was implemented after discussion with Steve Moyle smoyle@ermine.ox.ac.uk.