Iterative-deepening execution

This package applies a compiling control technique to implement depth-first iterative deepening execution [Kor85]. It changes the usual depth-first search rule by iterative-deepening on those predicates specifically marked. This is very useful in search problems as an alternative to, e.g., breadth-first search, when a complete proof procedure is needed.

When this search rule is used, first all goals are expanded only up to a given depth. If no solution is found or more solutions are needed by backtracking, the depth limit is incremented and the whole goal is repeated. Although it might seem that this approach is very inefficient because all higher levels are repeated for the deeper ones, it has been shown that it performs only about b/(b - 1) times as many operations than the corresponding breadth-first search (where b is the branching factor of the proof tree), while the memory consumption is the same as depth first.

The usage is by means of the following directive:

:- iterative(Name, FirstCut, Formula).

which states than the predicate 'Name' given in functor/arity form will be executed using the iterative deepening search rule, starting at depth FirstCut, and with depth being incremented by predicate Formula. This predicate computes the new depth using the previous one. It must implement a dilating function i.e., the new depth must be greater than the old one. For example, to start with depth 5 and increment by 10 you can write:

:- iterative(p/1,5,f).

f(X,Y) :- Y is X + 10.

or, alternatively:

:- iterative(p/1,5,(_(X,Y):- Y is X + 10)).

You can also use a fourth parameter to set a limiting depth. Goals that reach the given depth limit simply fail. Thus, with the following directive:

:- iterative(p/1,5,(_(X,Y):- Y is X + 10),100).

all goals deeper than 100 will fail.

This is a simple example using this package:

:- module(example_id, _,[id]).

test(id) :- 
	idchain(a,d).
test(df) :- 
	chain(a,d).   % loops!

:- iterative(idchain/2, 3, ( _(X,Z) :- Z is X + 1) ).

idchain(X,X).
idchain(X,Y) :- 
	arc(X,Z), 
	idchain(Z,Y).

chain(X,X).
chain(X,Y) :- 
	arc(X,Z), 
	chain(Z,Y).

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

The order of solutions is as follows: first, the shallower ones and then the deeper ones in the resolution tree. Solutions between two cutoffs are given in the usual left-to-right order (i.e., the leftmost branch corresponds to the first unifying clause in the program, as in depth-first search). For example:

:- module(_,_,[id]).

% All goals deeper than 2 will fail
:- iterative(p/1,0,(_(X,Z) :- Z is X + 1),2).

% Change the solutions' order to goal p(X). 
%:- iterative(p/1,1,(_(X,Z) :- Z is X + 3)).

p(X) :- q(X).
p(a).

q(X) :- r(X).
q(b).

r(X) :- s(X).
r(c).

s(d).

It is possible to preserve the iterative-deepening behavior for calls to predicates defined in other modules. These modules should obviously also use this package. In addition, all predicates from such modules should be imported, i.e., the directive :- use_module(module), should be used in this case instead of :- use_module(module,[...]). Otherwise calls to predicates outside the module will be treated in the usual way, i.e., by depth-first execution.

Another complete proof procedure is implemented by the bf package(s) (breadth first execution).