Iterative-deepening execution

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

When this computation 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 is 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 waste of memory 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 iterative deepening rule starting at the depth 'FirstCut' with depth being incremented by the predicate 'Formula'. This predicate compute the new depth using the previous one. It must implement a dilating function i.e. the new depth must be greater. 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 if you prefer,

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

You can also use a fourth parameter to set a limiting depth. All goals below 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.

An example of code using this package would be:

:- 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 are first the shallower and then the deeper. Solutions which are between two cutoff are given in the usual left to right order. 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).

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