prologprolog-metainterpreter

Dealing with complicated prolog loops


I am using Prolog to encode some fairly complicated rules in a project of mine. There is a lot of recursion, including mutual recursion. Part of the rules look something like this:

pred1(X) :- ...
pred1(X) :- someguard(X), pred2(X).

pred2(X) :- ...
pred2(X) :- othercondition(X), pred1(X).

There is a fairly obvious infinite loop between pred1 and pred2. Unfortunately, the interaction between these predicates is very complicated and difficult to isolate. I was able to eliminate the infinite loop in this instance by passing around a list of objects that have been passed to pred1, but this is extremely unwieldy! In fact, it largely defeats the purpose of using Prolog in this application.

How can I make Prolog avoid infinite loops? For example, if in the course of proving pred1(foo) it tries to prove pred1(foo) as a sub-goal, fail and backtrack.

Is it possible to do this with meta-interpreters?


Solution

  • One feature that is available in some Prolog systems and that may help you to solve such issues is called tabling. See for example the related question and .

    If tabling is not available, then yes, meta-interpreters can definitely help a lot with this. For example, you can change the executation strategy etc. with a meta-interpreter.

    In SWI-Prolog, also check out call_with_inference_limit/3 to robustly limit the execution, independent of CPU type and system load.

    Related and also useful are termination analyzers like cTI: They allow you to statically derive termination conditions.