An infinite success tree, or not?

Question

I'm given the following program:

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

path(N,M):- path(N,New),edge(New,M).
path(N,M):- edge(N,M).

And asked if when applying a proof tree algorithm to the following query:

?- path(a,X). 

the proof tree is an infinite success tree, or an infinite failure tree?

Now as I see it, during the building of the tree, you get stuck in applying rule 1 of path over and over again, creating an infinite tree and never getting to rule 2 of path..

thus creating an infinite failure tree. but the solution I have says it is an infinite success tree, my question is: am I right or is my professor right? :]

Answer 1

I would call that an infinite loop. Look at the trace:

?- trace, path(a,X).
Call: (7) path(a, _G394) ? 
Call: (8) path(a, _G511) ? 
Call: (9) path(a, _G511) ? 
Call: (10) path(a, _G511) ? 
...
Call: (147) path(a, _G511) ? 
Call: (148) path(a, _G511) ? 
...
ERROR: Out of local stack

I'm not familiar with these terms, but I might be able to wing it. No solutions are produced, so it would be hard for me to argue that this is an infinite success tree. Even given infinite time and space it would never produce a successful solution. At the same time, failure in the Prolog sense is immediate, and that isn't happening either. I'm not sure such a thing as an infinite failure tree could exist, unless you'd call that something that generates an infinite number of choice points, all of which fail. But there aren't any failures here. It would be more honest to just call this what it really is: an infinite loop. Such things exist outside the realm of success and failure. This is why in Haskell, ⊥ belongs to every type. Maybe in that sense you're both right.

Answer 2

Not sure what terminology you are using, but the common terminology - as used by Lloyd, Foundations of Logic Programming, is SLD-tree which may contain success, infinite, and failure branches. And I assume you use the standard Prolog computation rule (= select the leftmost atom).

The SLD-tree in your example is infinite and contains finitely many success branches corresponding to the three answer substitutions: X = b ; X = c ; X = d. What is important to note is that while this tree has an infinite failure branch, it nevertheless contains all solutions!

The very choice of computation rule may influence the size and structure of the SLD-tree. But the nice thing is : Whatever your computation rule, we will get our success branches! Guaranteed! Ehm, guaranteed for those who draw an infinite SLD-tree in a clever manner, and who know how to use ... wisely. But for people with infinite resource and sagacity, no problem.

Another observation is that the shape of this SLD-tree is pretty independent of the order of the clauses. So whether or not the non-recursive rule is written last (as in your case) or first, makes no big difference to the shape of the tree: It will be of the same size (either both infinite or both finite), will contain the same number of nodes, but some branches will appear in a different order.

Prolog tries to produce that SLD-tree incrementally, but it uses the most primitive way to do so. It starts to explore a branch, and explores it completely, before expanding the other branches. That means, that Prolog can use an extremely space-efficient representation of the SLD-tree (or to be precise: of a part of the SLD-tree only), in fact it is essentially a stack, but the price to pay is that once an infinite branch is encountered, you are stuck - unless you are of infinite resource, indeed. And the order of clauses will have an effect whether or not the success branches (= answers) will be found or whether they will be buried by some infinite branch.

In practice, it is quite difficult to visualize all these infinite trees, we are not so well accustomed to them.

But there are other ways how you can better understand how Prolog performs its proofs.

A central notion is here the universal termination of a query/goal which speaking in SLD-trees means: the finiteness of all branches.

It is very easy to observe universal termination of a goal: Simply execute Goal,false instead.

So what did this false do with our SLD-tree? Essentially, we have now an infinite or finite failure branch only. All answers are gone.

Now, things get even better: We may even introduce false into your program. The resulting program is called a failure-slice. Although this program is no longer the same as the original program, the following property holds: If the failure-slice does not terminate (= has an infinite branch), also the original program does not terminate (= has an infinite branch).

Failure-slices are often much shorter, so they are much faster to understand. Take your program:

?- path(a,X), false.

edge(a,b) :- false.
edge(b,c) :- false.
edge(a,d) :- false.

path(N,M):- path(N,New), false, edge(New,M).
path(N,M):- false, edge(N,M).

Experienced Prolog programmers just see this tiny little fragment of the program, which is much easier to understand. They don't spend their time imagining infinite branches, nor do they imagine actual Prolog execution — well, maybe a bit, but only for the fragment, not for the entire program.

In a sense, the false already shows us the computation rule: Everything on the right-hand side of false is stroked through.

You can learn to "see" this too, just follow this link.