This is a part of a general problem in logic programming which is the detection and trapping of infinite loops; that is, infinite branches in search space
which under unbounded depth-first search create non-terminating programs. In general this problem is not solvable. It is solvable for a certain class
of infinite loops where the goal repeats. This is called subsumption testing and it says that if you reave a search path
g1
|
|
V
g2
|
|
V
g3
where g1 .. g3 are each a series of Prolog goals each derived form the predecessor by resolution with a program clause
then if g1 subsumes g3 i.e. there is a substition s of the variables in g1 such that s(g1) = g3
then you can discontinue the search down this path. Prolog + subsumption allows you to have rules like
brother(X,Y) :- brother(Y,X).
w.o. looping. AFAIK, if you augment Prolog with subsumption it is complete for Datalog; i.e. function-free Prolog.
However there is another form of looping involving functions which cannot be reliably trapped.
jewish(X) : jewish(mother(X)).
creates a loop which is not trapped by subsumption.
The same holds for Shen derivation rules except the subumption test would be formulated differently.
If you have an expansive rule you can always trap it like this - by raising a flag that signifies the rule is not to be used again.
(datatype jewish
!; fail;
____________________
(- dont-use-me) >> P;
dont-use-me >> (jewish (mother X));
__________________________________
(jewish X);)
But of course you lose completeness by so doing.
M.