SWI-Prolog: Understanding Infinite Loops

2019-07-14 04:20发布

问题:

I am currently trying to understand the basics of prolog.

I have a knowledge base like this: p(a). p(X) :- p(X). If I enter the query p(b), the unification with the fact fails and the rule p(X) :- p(X) is used which leads the unification with the fact to fail again. Why is the rule applied over and over again after that? Couldn't prolog return false at this point? After a certain time I get the message "Time limit exceeded". I'm not quite sure why prolog uses the rule over and over again, but since it is, I don't understand why I get a different error message as in the following case. To be clear, I do understand that "p(X) if p(X)" is an unreasonable rule, but I would like to understand what exactly happens there.

If I have a knowledge base like this: p(X) :- p(X). p(a). There is no chance to come to a result even with p(a) because the fact is below the rule and the rule is called over and over again. For this variant I receive a different error message almost instantly "ERROR: Out of local stack" which is comprehensible.

Now my question - what is the difference between those cases? Why am I receiving different error messages and why is prolog not returning false after the first application of the rule in the above case? My idea would be that in the above case the procedure is kind of restarted each time the rule gets called and in the below case the same procedure calls the rule over and over again. I would be grateful if somebody could elaborate this.

Update: If I query p(a). to the 2nd KB as said I receive "Out of local stack", but if I query p(b). to the same KB I get "Time limit exceeded". This is even more confusing to me, shouldn't the constant be irrelevant for the infinite loop?

回答1:

Let us first consider the following program fragment that both examples have in common:

p(X) :- p(X).

As you correctly point out, it is obvious that no particular solutions are described by this fragment in isolation. Declaratively, we can read it as: "p(X) holds if p(X) holds". OK, so we cannot deduce any concrete solution from only this clause.

This explains why p(b) cannot hold if only this fragment is considered. Additionally, p(a) does not imply p(b) either, so no matter where you put the fact p(a), you will never derive p(b) from these two clauses.

Procedurally, Prolog still attempts to find cases where p(X) holds. So, if you post ?- p(X). as a query, Prolog will try to find a resolution refutation, disregarding what it has "already tried". For this reason, it will try to prove p(X) over and over. Prolog's default resolution strategy, SLDNF resolution, keeps no memory of which branches have already been tried, and also for this reason can be implemented very efficiently, with little overhead compared to other programming languages.

The difference between an infinite deduction attempt and an out of local stack error error can only be understood procedurally, by taking into account how Prolog executes these fragments.

Prolog systems typically apply an optimization that is called tail call optimization. This is applicable if no more choice-points remain, and means that it can discard (or reuse) existing stack frames.

The key difference between your two examples is obviously where you add the fact: Either before or after the recursive clause.

In your case, if the recursive clause comes last, then no more choice-points remain at the time the goal p(X) is invoked. For this reason, an existing stack frame can be reused or discarded.

On the other hand, if you write the recursive clause first, and then query ?- q(X). (or ?- q(a).), then both clauses are applicable, and Prolog remembers this by creating a choice-point. When the recursive goal is invoked, the choice-point still exists, and therefore the stack frames pile up until they exceed the available limits.

If you query ?- p(b)., then argument indexing detects that p(a) is not applicable, and again only the recursive clause applies, independent of whether you write it before or after the fact. This explains the difference between querying p(X) (or p(a)) and p(b) (or other queries). Note that Prolog implementations differ regarding the strength of their indexing mechanisms. In any case, you should expect your Prolog system to index at least on the outermost functor and arity of the first argument. If necessary, more complex indexing schemes can be constructed manually on top of this mechanism. Modern Prolog systems provide JIT indexing, deep indexing and other mechanisms, and so they often automatically detect the exact subset of clauses that are applicable.

Note that there is a special form of resolution called SLG resolution, which you can use to improve termination properties of your programs in such cases. For example, in SWI-Prolog, you can enable SLG resolution by adding the following directives before your program:

:- use_module(library(tabling)).

:- table p/1.

With these directives, we obtain:

?- p(X).
X = a.

?- p(b).
false.

This coincides with the declarative semantics you expect from your definitions. Several other Prolog systems provide similar facilities.



回答2:

It should be easy to grasp the concept of infinite loop by studying how standard repeat/0 is implemented:

repeat.
repeat :- repeat.

This creates an infinite number of choice points. First clause, repeat., simply allows for a one time execution. The second clause, repeat :- repeat. makes it infinitely deep recursion.

Adding any number of parameters:

repeat(_, _, ..., _).
repeat(Param1, Param2, ..., ParamN) :- repeat(Param1, Param2, ..., ParamN).

You may have bodies added to these clauses and have parameters of the first class having meaningful names depending on what you are trying to archive. If bodies won't contain cuts, direct or inherited from predicates used, this will be an infinite loop too just as repeat/0.



标签: prolog