prologbacktrackingfailure-slicenon-termination

Prolog doesn't terminate after goal reordering


I'm currently working through the Learn Prolog Now examples and for the one exercise I have a KB that runs out of local stack if I just have a tiny change in one rule. this is the KB:

byCar(auckland,hamilton). 
byCar(hamilton,raglan). 
byCar(valmont,saarbruecken). 
byCar(valmont,metz). 

byTrain(metz,frankfurt). 
byTrain(saarbruecken,frankfurt). 
byTrain(metz,paris). 
byTrain(saarbruecken,paris). 

byPlane(frankfurt,bangkok). 
byPlane(frankfurt,singapore). 
byPlane(paris,losAngeles). 
byPlane(bangkok,auckland). 
byPlane(singapore,auckland). 
byPlane(losAngeles,auckland).

travel(X,Y) :- byCar(X,Y).
travel(X,Y) :- byTrain(X,Y).
travel(X,Y) :- byPlane(X,Y).

and the relevant rule:

travel(X,Y) :- travel(X,Z), travel(Z,Y).

and this is the query in question which runs out of stack:

?- travel(valmont,losAngeles).

But if I change the rule to

travel(X,Y) :- travel(Z,Y), travel(X,Z).

Then it works.

If I trace the query I get quickly stuck like this:

   Redo: (17) travel(raglan, _6896) ? creep
   Call: (18) byPlane(raglan, _6896) ? creep
   Fail: (18) byPlane(raglan, _6896) ? creep
   Redo: (17) travel(raglan, _6896) ? creep
   Call: (18) travel(raglan, _6896) ? creep
   Call: (19) byCar(raglan, _6896) ? creep
   Fail: (19) byCar(raglan, _6896) ? creep
   Redo: (18) travel(raglan, _6896) ? creep
   Call: (19) byTrain(raglan, _6896) ? creep
   Fail: (19) byTrain(raglan, _6896) ? creep
   Redo: (18) travel(raglan, _6896) ? creep
   Call: (19) byPlane(raglan, _6896) ? creep
   Fail: (19) byPlane(raglan, _6896) ? creep
   Redo: (18) travel(raglan, _6896) ? creep
...

But I don't see why. Shouldn't it just understand that raglan is an endstation and thus it has to backtrack one level more?

Thanks!

Edit: I use SWI Prolog

Edit: I found the problem after going through it step by step. In the case of raglan, there is no rule to anywhere at all. Therefore, after trying byPlane, byTrain, byCar, it tries travel(raglan, X) again (the first goal of the last rule), thus looping. But I don't see how the other rule is any better.


Solution

  • Obviously, goal ordering is really important in this case. As you figured out, your first formulation allows for finding another hypothetical connection from raglan to anywhere by going via a hypothetical another city Z, whose nonexistence is never proven because you keep looking for it be recursing infinitely. Really, the trace is your best friend here, but this is not trivial to get right. You also have to think about all the cases where one, both or none of the arguments are bound.

    Your second formulation is not better at all, it just happens to fail on different cases:

    travel(losAngeles, valmont).
    ERROR: Out of local stack
    

    I would propose to make your logic safer by distinguishing between a direct connection and a multi-stop journey:

    connection(X,Y) :- byCar(X,Y).
    connection(X,Y) :- byTrain(X,Y).
    connection(X,Y) :- byPlane(X,Y).
    
    travel(X,Y) :- connection(X,Y).
    travel(X,Y) :- connection(X,Z), travel(Z,Y).
    

    Goal order doesn't matter now because travel always requires some physical connection to exist (rather than a recursion) in order to proceed.

    This also makes it easier to record the journey, which you would want anyway (right?):

    connection(X,Y, car(X,Y))   :- byCar(X,Y).
    connection(X,Y, train(X,Y)) :- byTrain(X,Y).
    connection(X,Y, plane(X,Y)) :- byPlane(X,Y).
    
    travel(X,Y,[Part])       :- connection(X,Y,Part).
    travel(X,Y,[Part|Parts]) :- connection(X,Z,Part), travel(Z,Y,Parts).
    
    ?- travel(valmont, losAngeles, Journey).
    Journey = [car(valmont, saarbruecken), train(saarbruecken, paris), plane(paris, losAngeles)] 
    

    And for the case where there is no valid trip:

    travel(losAngeles, valmont, Journey).
    false.