Consider the following Prolog rules:
foo(0). foo(1). bar(X, Y) :- foo(X), foo(Y).
How does this program behave?
This is an example of a program that has exactly two solutions.
a(2). a(2).
After the first solution is generated for the query a(1) the user types s semicolon at the prompt. Prolog answers "yes".
a(2). true ? ; (1 ms) yes
Note that the user only had to type one semicolon in this interactive session, even though there are two solutions.
Now consider another example of a program that has exactly two solutions.
b(2). b(2). b(3).
Again, after the user types a semicolon gprolog answers "yes" immediately. It knows that the third rule won't apply. Why? Because gprolog indexes the heads of rules.
?- b(2). true ? ; yes
Now consider yet another example of a program that has exactly two solutions. This one has a third rule involving a variable.
c(2). c(2). c(X) :- X=3.
Even though the third rule will fail for the query c(2), gprolog does not determine the third rule will fail until trying it. The user must enter another semicolon to tell gprolog to continue searching. But when it expands the RHS of the clause gprolog concludes that 2=3 must fail, so it answers "no".
?- c(2). true ? ; true ? ; (1 ms) no
After the 2nd (last) solution is found, GProlog has to continue searching before it can conclude definitively that there are no more solutions to the query c(2).
Consider the following Prolog rules:
del([X|Xs], X, Ys) :- del(Xs, X, Ys).del([L|Ls], X, [L|Ys]) :- del(Ls, X, Ys).
del([], _, []).
Before we explore how backtracking behaves, reviewing some simple queries will help gain familiarity with this program, which by the way is named "del" because the third argument has an element (the second argument) deleted from the list which is the first argument.
Now consider this query.
?- del([], b, []).
Intuitively there were no b's to delet from the empty list, so the 1st and 3rd arugemnts are [].
The mechanics of the prolog engine considers each of the three rules in order. Rule 1 is rejected because it fails to unify. Then rule 2 is considered, and it also fails to unify. The query resolves by unifying the query term using rule 3 and so answers yes.
Another query.
?- del([b], b, []).
Both rule 1 and rule 2 can unify with this goal. The prolog resolver uses depth first search and so tries rule 1 first, saving the exploration of whether rule 2 might lead to a solution for later. When the head of rule 1 fires, the following bindings are established:
X=b Xs=[] Ys=[]
The resolver uses rule 1 to issue the subgoal:
del([],b,[]).
which succeeds. Unlike before, prolog prints:
true ?
awaiting user input.
![[Note]](images/note.png) | Note |
|---|---|
In gnuprolog, typing ";" tells the resolver to look for more solutions, whereas just hitting ENTER tells gnuprolog to terminate the search, now. |
L=b Ls=[] X=b Ys=[]The resolver uses rule 2 to issue the subgoal:
del([],b,[b]).which fails. The prolog interaction looks like this:
| ?- del([b], b, []). true ? ; no
As with the previous example query, there is only one way to "prove" that the query is true. However, in the previous example, Prolog found a soultion (succeeded) and determined that it was the only solution, so Prolog printed "yes" without prompting for user input. In this example, the Prolog resolver searches and finds a solution, but because it did not completely search all possible proof constructions, reports this (by answering "true ?"). If you type ";" Prolog resumes the search, concludes there are no other solutions, and reprots "no". If you type ENTER, you tell Prolog to terminate the search. Prolog answers "yes" since it found a solution just before terminating.
Now consider this query.
?- del([b], b, [b]).
Intuitively you might guess that this says starting with the list [b], what is the list with a "b" deleted? do we get the list [b]?
But really the program "del" is written non-deterministicly. Inotherwords, it really answers whether the reluting list has zero or more b's deleted non-deterministicly. Of course the Prolog engine considers these non-deterministic choices in a particular order, so let's see how Prolog does that.
Both rule 1 and rule 2 can unify with this goal. The prolog resolver uses depth first search and so tries rule 1 first, saving the exploration of whether rule 2 might lead to a solution for later. When the head of rule 1 fires, the following bindings are established:
X=b Xs=[] Ys=[b]
The resolver uses rule 1 to issue the subgoal:
del([],b,[b]).
which fails. Prolog then tries rule 2 since it could also unify with the query goal. When rule 2 fires, the following bindings are established.
L=b Ls=[] X=b Ys=[]
The resolver uses rule 2 to issue the subgoal:
del([],b,[]).
which unifies with rule 3 and succeeds. No other solutions are possible, so Prolog answers,
yes
We consider in two ways: first the mechanics of the resolver's behavior and then logically.
The prolog resolver attempts to unify the heads of these rules with the active query (goal).
Now let's turn our attention to a concrete example.
| Note |
|---|---|
Note the use of the anonymous variable |
The query,
?- del([a,b,c,b], b, R).
produces four solutions: here's the output when typing "a" to generate all solutions,
| ?- del([a,b,c,b], b, R). R = [a,c] ? a R = [a,c,b] R = [a,b,c] R = [a,b,c,b]
Need to redraw this as a tree to emphasis DFS behavior. Also to show the order of backtracking.
GOAL: del([a,b,c,b], b, R).
del([X|Xs], X, Ys) Fails to unify X=a X=b
del([L|Ls], X, [L|Ys]) L=a Ls=[b,c,b] X=b Ys=R
SUBGOAL: del([b,c,b], b, Ys).
del([], _, []) Fails to unify
Below shows Ys' to differentiate between the new binding for Ys introduced when entering a new scope for the subgoal.
GOAL: del([b,c,b],b,Ys).
del([X|Xs], X, Ys) X=b Xs=[c,b] Ys'=Ys
SUBGOAL: del([c,b], b, Ys').
del([L|Ls], X, [L|Ys]) L=b Ls=[c,b] X=b [b|Ys']=Ys
SUBGOAL: del([c,b], b, Ys').
del([], _, []) Fails to unify
Note Ys'' below.
GOAL: del([c,b], b, Ys').
del([X|Xs], X, Ys) Fails to unify X=c X=b
del([L|Ls], X, [L|Ys]) L=c Ls=[b] X=b [c|Ys'']=Ys'
SUBGOAL: del([b], b, Ys'').
del([], _, []) Fails to unify
GOAL: del([b], b, Ys'').
del([X|Xs], X, Ys) X=b Xs=[] Ys'''=Ys''
SUBGOAL: del([], b, Ys''').
del([L|Ls], X, [L|Ys]) L=x Ls=[] X=b [b|Ys''']=Ys''
SUBGOAL: del([], b, Ys''').
del([], _, []) Fails to unify
GOAL: del([], b, Ys''').
del([X|Xs], X, Ys) Fails to unify
SUBGOAL: del([], b, Ys''').
del([L|Ls], X, [L|Ys]) Fails to unify
SUBGOAL: del([], b, Ys''').
del([], _, []) unifies with Ys'''=[]
This is a tree without the bindings shown. Bracketed numbers indicate which rule is attempted.
del([a,b,c,b],b,Ys)
* * *
* * *
[1] FAILS [2] del([b,c,b],b,Ys) [3] FAILS
* * *
* * *
[1] del([c,b],b,Ys) [2] del([c,b],b,Ys) [3] FAILS
* * * * * *
* * * * * *
[1] FAILS [2] del([b],b,Ys) [3] FAILS [1] FAILS [2] del([b],b,Ys) [3] FAILS
* * * * * *
* * * * * *
[1] del([],b,Ys) [2] del([],b,Ys) [3] FAILS [1] del([],b,Ys) [2] del([],b,Ys) [3] FAILS
Below is a transcript of the same query issued after entering trace mode.
trace.
| ?- del([a,b,c,b], b, R).
1 1 Call: del([a,b,c,b],b,_24) ?
2 2 Call: del([b,c,b],b,_57) ?
3 3 Call: del([c,b],b,_57) ?
4 4 Call: del([b],b,_109) ?
5 5 Call: del([],b,_109) ?
5 5 Exit: del([],b,[]) ?
4 4 Exit: del([b],b,[]) ?
3 3 Exit: del([c,b],b,[c]) ?
2 2 Exit: del([b,c,b],b,[c]) ?
1 1 Exit: del([a,b,c,b],b,[a,c]) ?
R = [a,c] ? a
1 1 Redo: del([a,b,c,b],b,[a,c]) ?
2 2 Redo: del([b,c,b],b,[c]) ?
3 3 Redo: del([c,b],b,[c]) ?
4 4 Redo: del([b],b,[]) ?
5 5 Call: del([],b,_136) ?
5 5 Exit: del([],b,[]) ?
4 4 Exit: del([b],b,[b]) ?
3 3 Exit: del([c,b],b,[c,b]) ?
2 2 Exit: del([b,c,b],b,[c,b]) ?
1 1 Exit: del([a,b,c,b],b,[a,c,b]) ?
R = [a,c,b]
1 1 Redo: del([a,b,c,b],b,[a,c,b]) ?
2 2 Redo: del([b,c,b],b,[c,b]) ?
3 3 Call: del([c,b],b,_84) ?
4 4 Call: del([b],b,_111) ?
5 5 Call: del([],b,_111) ?
5 5 Exit: del([],b,[]) ?
4 4 Exit: del([b],b,[]) ?
3 3 Exit: del([c,b],b,[c]) ?
2 2 Exit: del([b,c,b],b,[b,c]) ?
1 1 Exit: del([a,b,c,b],b,[a,b,c]) ?
R = [a,b,c]
1 1 Redo: del([a,b,c,b],b,[a,b,c]) ?
2 2 Redo: del([b,c,b],b,[b,c]) ?
3 3 Redo: del([c,b],b,[c]) ?
4 4 Redo: del([b],b,[]) ?
5 5 Call: del([],b,_138) ?
5 5 Exit: del([],b,[]) ?
4 4 Exit: del([b],b,[b]) ?
3 3 Exit: del([c,b],b,[c,b]) ?
2 2 Exit: del([b,c,b],b,[b,c,b]) ?
1 1 Exit: del([a,b,c,b],b,[a,b,c,b]) ?
R = [a,b,c,b]
yes
{trace}
The mechanics of Prolog resolution become tedious when backtracking even for simple queries such as this example. Nevertheless, the mechanism is simple. The main points to consider are:
- Prolog tries rules in order.
- All rules whose head can unify are eventually tried in backtracking.
- Backtracking explores subgoals in DFS order.
- Each subgoal introduces a new scope and thus create new bindings for varibles. Also, variable can be bound to other variables defined in dynamically enclosing scopes or to stuctures made up of ground terms intermixed with ground and unground varibles. During a variable's lifetime it may become more ground.
- Backtracking discards previous subgoals, their results and their bindings.
We can reason about prolog programs by considering truths or falsehoods. For example, the query,
?- del([a,b,c,b], b, R).
Could be interpreted, " is there an R such that del([a,b,c,b], b, R) is true?
The rules can be considered as axiomatic statements of truth. For example, rule 3, means "del([], X, []) for any value X is true". And rule 1 means "del([X|Xs], X, Ys)" is true if "del(Xs, X, Ys)." can be shown to be true for values X, Xs, and Ys.
So our original query,
del([a,b,c,b], b, R).
is true in four different ways with four different solutions. Specifically, here is the reasoning that it is true for the first solution,
- The query, del([a,b,c,b],b,R)
- is true if del([b,c,b],b,Ys) where R=[a|Ys]
- is true if del([c,b],b,Ys') where Ys'=Ys
- is true if del([b],b,Ys'') where Ys''=[c|Ys'']
- is true if del([],b,Ys'') where Ys'''=Ys''
- which is true when Ys'''=[] --Q.E.D.
The value computed for R is thus a side-effect of proving the query to be true. By substitution you shuld verify that R=[a|[c|[]]] which is the same as R=[a,c].