When is the Redo-port called with new variables in

Question

During my implementation of the Adventure game in Prolog I was wondering when the redo-port is called with new variables during backtracking and when it is called with the same ones?

For example, I have the following knowledge base:

location(desk,office).
location(apple,kitchen).
location(flashlight,desk).
location('washing machine',cellar).
location(nani,'washing machine').
location(broccoli,kitchen).
location(crackers,kitchen).
location(computer,office).

door(office,hall).
door(kitchen,office).
door(hall,'dining room').
door(kitchen,cellar).
door('dining room',kitchen).

When tracing the query ?-(location(X,Y),door(kitchen,Y)). I get this:

   Call: (9) location(_7998, _8000) ? creep
   Exit: (9) location(desk, office) ? creep
   Call: (9) door(kitchen, office) ? creep
   Exit: (9) door(kitchen, office) ? creep
X = desk,
Y = office ;
   Redo: (9) door(kitchen, office) ? creep      <==== 1
   Fail: (9) door(kitchen, office) ? creep
   Redo: (9) location(_7998, _8000) ? creep
   Exit: (9) location(apple, kitchen) ? creep
   Call: (9) door(kitchen, kitchen) ? creep
   Fail: (9) door(kitchen, kitchen) ? creep
   Redo: (9) location(_7998, _8000) ? creep
   Exit: (9) location(flashlight, desk) ? creep
   Call: (9) door(kitchen, desk) ? creep
   Fail: (9) door(kitchen, desk) ? creep
   Redo: (9) location(_7998, _8000) ? creep
   Exit: (9) location('washing machine', cellar) ? creep
   Call: (9) door(kitchen, cellar) ? creep
   Exit: (9) door(kitchen, cellar) ? creep
X = 'washing machine',
Y = cellar ;
   Redo: (9) location(_7998, _8000) ? creep    <==== 2
   Exit: (9) location(nani, 'washing machine') ? creep
   Call: (9) door(kitchen, 'washing machine') ? creep
   Fail: (9) door(kitchen, 'washing machine') ? creep
   Redo: (9) location(_7998, _8000) ? creep
   Exit: (9) location(broccoli, kitchen) ? creep

   Call: (9) door(kitchen, kitchen) ? creep
   Fail: (9) door(kitchen, kitchen) ? creep
   Redo: (9) location(_7998, _8000) ? creep
   Exit: (9) location(crackers, kitchen) ? creep
   Call: (9) door(kitchen, kitchen) ? creep
   Fail: (9) door(kitchen, kitchen) ? creep
   Redo: (9) location(_7998, _8000) ? creep
   Exit: (9) location(computer, office) ? creep
   Call: (9) door(kitchen, office) ? creep
   Exit: (9) door(kitchen, office) ? creep
X = computer,
Y = office ;
   Redo: (9) door(kitchen, office) ? creep    <==== 3
   Fail: (9) door(kitchen, office) ? creep
false.

I understand how the binding of the variables works, but I do not understand why Prolog returns

Redo: (9) door(kitchen, office) ? creep <==== 1
Redo: (9) door(kitchen, office) ? creep <==== 3

after finding the first solution (and the same for the last solution),

while it immediately looks for a new binding of X and Y after the second solution

Redo: (9) location(_7998, _8000) ? creep <==== 2

Why does it not immediately continue to look for a new binding of X and Y after the first and last solution, instead of resorting to

Redo: (9) door(kitchen, office) ? creep <==== 3

(which fails anyway)?

(I found a similar question here, but unfortunately my reputation does not allow me to comment over there and I think this particular issue does not have to do with my Prolog version (as I tried it with SWI-Prolog and GNUProlog))

Thanks in advance for offering any clarity.

Answer 1

This is just a comment posted as a answer because it has a picture.

If you use the graphical debugger you can see when choice points are created.

?- gtrace.
true.

[trace] ?- (location(X,Y),door(kitchen,Y)).

In the following image of the debugger I highlighted the choice point with a green rectangle.

To exit out of trace mode in top-level enter nodebug.

[trace] ?- nodebug.
true.

?- 

Note: It is the choice points that lead to using the redo port.
Note: Another way to debug prolog is via use of failure slice. Also read questions tagged with failure slice

Answer 2

This answer makes use of SWI-Prolog.

The first thing that can help when using trace for the first time is to make all of the ports visible. By default the unify port is not visible but can be made visible with

?- visible(+unify).

Now since this is such a short running query, instead of having to press the space bar for each port, we can disable the leashing of the leashed ports with

?- leash(-call).
?- leash(-exit).
?- leash(-redo).
?- leash(-fail).

Now if you turn on trace and run the query

?- trace.
[trace] ?- (location(X,Y),door(kitchen,Y)).

you will not have to press the space bar expect for answers.

Doing so will return

   Call: (9) location(_9632, _9634)
   Unify: (9) location(desk, office)
   Exit: (9) location(desk, office)
   Call: (9) door(kitchen, office)
   Unify: (9) door(kitchen, office)
   Exit: (9) door(kitchen, office)
X = desk,
Y = office ;
   Redo: (9) door(kitchen, office)
   Fail: (9) door(kitchen, office)
   Redo: (9) location(_9632, _9634)
   Unify: (9) location(apple, kitchen)
   Exit: (9) location(apple, kitchen)
   Call: (9) door(kitchen, kitchen)
   Fail: (9) door(kitchen, kitchen)
   Redo: (9) location(_9632, _9634)
   Unify: (9) location(flashlight, desk)
   Exit: (9) location(flashlight, desk)
   Call: (9) door(kitchen, desk)
   Fail: (9) door(kitchen, desk)
   Redo: (9) location(_9632, _9634)
   Unify: (9) location('washing machine', cellar)
   Exit: (9) location('washing machine', cellar)
   Call: (9) door(kitchen, cellar)
   Unify: (9) door(kitchen, cellar)
   Exit: (9) door(kitchen, cellar)
X = 'washing machine',
Y = cellar ;
   Redo: (9) location(_9632, _9634)
   Unify: (9) location(nani, 'washing machine')
   Exit: (9) location(nani, 'washing machine')
   Call: (9) door(kitchen, 'washing machine')
   Fail: (9) door(kitchen, 'washing machine')
   Redo: (9) location(_9632, _9634)
   Unify: (9) location(broccoli, kitchen)
   Exit: (9) location(broccoli, kitchen)
   Call: (9) door(kitchen, kitchen)
   Fail: (9) door(kitchen, kitchen)
   Redo: (9) location(_9632, _9634)
   Unify: (9) location(crackers, kitchen)
   Exit: (9) location(crackers, kitchen)
   Call: (9) door(kitchen, kitchen)
   Fail: (9) door(kitchen, kitchen)
   Redo: (9) location(_9632, _9634)
   Unify: (9) location(computer, office)
   Exit: (9) location(computer, office)
   Call: (9) door(kitchen, office)
   Unify: (9) door(kitchen, office)
   Exit: (9) door(kitchen, office)
X = computer,
Y = office ;
   Redo: (9) door(kitchen, office)
   Fail: (9) door(kitchen, office)
false.

which now has the Unify ports visible.

Since this is such a short query I will comment the significant lines of the trace and that in turn should answer your questions.

   % location fact 1: location(desk, office) -------------------------
   % First predicate of query - location(X,Y)

   % The location facts are matched in the order of the source code
   % Since the code is looking for location(X,Y)
   % it matches location fact 1: location(desk, office)
   % Since there are more location facts like location(X, Y),
   % e.g.
   %   location(apple,kitchen).
   %   location(flashlight,desk).
   %   location('washing machine',cellar).
   %   location(nani,'washing machine').
   %   location(broccoli,kitchen).
   %   location(crackers,kitchen).
   %   location(computer,office).
   % a choice point is generated
   % choice point: location 1
   Call: (9) location(_9632, _9634)

   % Unifies with first location fact.
   % X binds with desk
   % Y binds with office
   Unify: (9) location(desk, office)

   Exit: (9) location(desk, office)

   % Second predicate of query - door(kitchen,Y)).
   % Y is bound with office
   % The door facts are matched in the order of the source code
   % Since the code is only looking for door(kitchen,office)
   % it matches door fact 2: door(kitchen,office)
   % Since there are more door facts like door(kitchen,Y),
   % e.g.
   %    door(kitchen,cellar).
   % a choice point is generated
   % choice point: door 1
   Call: (9) door(kitchen, office)

   % Since there is a door(kitchen, office) fact
   % unify with second predicate
   Unify: (9) door(kitchen, office)
   Exit: (9) door(kitchen, office)
   % No more predicates in the query so return result.
X = desk,
Y = office ;

   % Remember choice point: door 1
   % Use the second predicate
   % on the remaining door facts like door(kitchen,Y)
   % e.g.
   %    door(kitchen,cellar).
   Redo: (9) door(kitchen, office)

   % There are no more door facts that unify with door(kitchen, office)
   % so fail.
   Fail: (9) door(kitchen, office)

   % Since the second predicate failed,
   % go back to the first predicate location(X,Y)
   % location fact 2: location(apple, kitchen) -----------------------

   % Remember choice point: location 1
   % Use the first predicate
   % on the remaining location facts like location(X,Y)
   % e.g.
   %   location(apple,kitchen).
   %   location(flashlight,desk).
   %   location('washing machine',cellar).
   %   location(nani,'washing machine').
   %   location(broccoli,kitchen).
   %   location(crackers,kitchen).
   %   location(computer,office).
   Redo: (9) location(_9632, _9634)

   % The second fact unifies with the first predicate location(X,Y)
   % X binds with apple
   % Y binds with kitchen
   Unify: (9) location(apple, kitchen)
   Exit: (9) location(apple, kitchen)

   % Second predicate of query - door(kitchen,Y)).
   % Y is bound with kitchen
   % The door facts are matched in the order of the source code
   % Since the code is only looking for door(kitchen,kitchen)
   % it matches none of the door facts
   % and since it checked all of the door facts
   % no choice point was generated.
   Call: (9) door(kitchen, kitchen)

   % There is no door(kitchen, kitchen) fact so fail.
   Fail: (9) door(kitchen, kitchen)

   % location fact 3: location(flashlight, desk) ---------------------
   % Remember choice point: location 1
   % Use the first predicate
   % on the remaining location facts like location(X,Y)
   % e.g.
   %   location(flashlight,desk).
   %   location('washing machine',cellar).
   %   location(nani,'washing machine').
   %   location(broccoli,kitchen).
   %   location(crackers,kitchen).
   %   location(computer,office).
   Redo: (9) location(_9632, _9634)
   Unify: (9) location(flashlight, desk)
   Exit: (9) location(flashlight, desk)
   Call: (9) door(kitchen, desk)
   Fail: (9) door(kitchen, desk)

   % Since the second predicate failed,
   % go back to the first predicate location(X,Y)
   % location fact 4: location('washing machine', cellar)  -----------
   % Remember choice point: location 1
   % Use the first predicate
   % on the remaining location facts like location(X,Y)
   % e.g.
   %   location('washing machine',cellar).
   %   location(nani,'washing machine').
   %   location(broccoli,kitchen).
   %   location(crackers,kitchen).
   %   location(computer,office).
   Redo: (9) location(_9632, _9634)

   % The forth fact unifies with the first predicate location(X,Y)
   % X binds with 'washing machine'
   % Y binds with cellar
   Unify: (9) location('washing machine', cellar)

   Exit: (9) location('washing machine', cellar)

   % Second predicate of query - door(kitchen,Y)).
   % Y is bound with cellar
   % The door facts are matched in the order of the source code
   % Since the code is only looking for door(kitchen,cellar)
   % it matches door fact 4: door(kitchen,cellar)
   % Since there are NO more door facts like door(kitchen,Y),
   % NO choice point is generated
   Call: (9) door(kitchen, cellar)

   % There is a door(kitchen, cellar) fact so unify.
   Unify: (9) door(kitchen, cellar)
   Exit: (9) door(kitchen, cellar)
   % No more predicates in the query so return result.
X = 'washing machine',
Y = cellar ;

   % location fact 5: location(nani, 'washing machine') --------------
   % Remember choice point: location 1
   % Use the first predicate
   % on the remaining location facts like location(X,Y)
   % e.g.
   %   location(nani,'washing machine').
   %   location(broccoli,kitchen).
   %   location(crackers,kitchen).
   %   location(computer,office).
   Redo: (9) location(_9632, _9634)
   Unify: (9) location(nani, 'washing machine')
   Exit: (9) location(nani, 'washing machine')
   Call: (9) door(kitchen, 'washing machine')
   Fail: (9) door(kitchen, 'washing machine')

   % location fact 6: location(broccoli, kitchen) --------------------
   % Remember choice point: location 1
   % Use the first predicate
   % on the remaining location facts like location(X,Y)
   % e.g.
   %   location(broccoli,kitchen).
   %   location(crackers,kitchen).
   %   location(computer,office).
   Redo: (9) location(_9632, _9634)
   Unify: (9) location(broccoli, kitchen)
   Exit: (9) location(broccoli, kitchen)
   Call: (9) door(kitchen, kitchen)
   Fail: (9) door(kitchen, kitchen)

   % location fact 7: location(crackers, kitchen) --------------------
   % Remember choice point: location 1
   % Use the first predicate
   % on the remaining location facts like location(X,Y)
   % e.g.
   %   location(crackers,kitchen).
   %   location(computer,office).
   Redo: (9) location(_9632, _9634)
   Unify: (9) location(crackers, kitchen)
   Exit: (9) location(crackers, kitchen)
   Call: (9) door(kitchen, kitchen)
   Fail: (9) door(kitchen, kitchen)

   % Since the second predicate failed,
   % go back to the first predicate location(X,Y)
   % location fact 8: location(computer, office) ---------------------
   % Remember choice point: location 1
   % Use the first predicate
   % on the remaining location facts like location(X,Y)
   % e.g.
   %   location(computer,office).
   Redo: (9) location(_9632, _9634)

   % The last fact unifies with the first predicate location(X,Y)
   % X binds with computer
   % Y binds with office
   Unify: (9) location(computer, office)
   Exit: (9) location(computer, office)

   % Second predicate of query - door(kitchen,Y)).
   % Y is bound with office
   % The door facts are matched in the order of the source code
   % Since the code is only looking for door(kitchen,office)
   % it matches door fact 2: door(kitchen,office)
   % Since there are more door facts like door(kitchen,Y),
   % e.g.
   %    door(kitchen,cellar).
   % a choice point is generated
   % choice point: door 2
   Call: (9) door(kitchen, office)

   % Since there is a door(kitchen, office) fact
   % unify with second predicate
   Unify: (9) door(kitchen, office)
   Exit: (9) door(kitchen, office)
   % No more predicates in the query so return result.
X = computer,
Y = office ;
   % Remember choice point: door 2
   % Use the second predicate
   % on the remaining door facts like door(kitchen,Y)
   % e.g.
   %    door(kitchen,cellar).
   Redo: (9) door(kitchen, office)

   % There are no more door facts that unify with door(kitchen, office)
   % so fail.
   Fail: (9) door(kitchen, office)

   % There are no more location facts so end the query.
false.

Supplement

When I created the answer it was in a text editor that can do syntax highlight for Prolog code, and to help me keep things straight I had three panes open for comparing. One pane had the location and door rules. One pane had a comment, and the third pane had a similar comment. As I moved down the code I kept updating the comments in the third pane to match similar comment in the second pane while checking against the facts in the first pane. I note this because it is probably a better way to understand the comments than reading them from this answer as posted.

The editor is Visual Studio Code and for highlighting Prolog the Prolog extension is installed.