I am trying to understand Prolog lists, and how values are 'returned' / instantiated at the end of a recursive function.
I am looking at this simple example:
val_and_remainder(X,[X|Xs],Xs).
val_and_remainder(X,[Y|Ys],[Y|R]) :-
val_and_remainder(X,Ys,R).
If I call val_and_remainder(X, [1,2,3], R).
then I will get the following outputs:
X = 1, R = [2,3];
X = 2, R = [1,3];
X = 3, R = [1,2];
false.
But I am confused as to why in the base case (val_and_remainder(X,[X|Xs],Xs).
) Xs
has to appear as it does.
If I was to call val_and_remainder(2, [1,2,3], R).
then it seems to me as though it would run through the program as:
% Initial call
val_and_remainder(2, [1,2,3], R).
val_and_remainder(2, [1|[2,3]], [1|R]) :- val_and_remainder(2, [2,3], R).
% Hits base case
val_and_remainder(2, [2|[3]], [3]).
If the above run through is correct then how does it get the correct value for R
? As in the above case the value of R should be R = [1,3]
.
In Prolog, you need to think of predicates not as functions as you would normally in other languages. Predicates describe relationships which might include arguments that help define that relationship.
For example, let's take this simple case:
same_term(X, X).
This is a predicate that defines a relationship between two arguments. Through unification it is saying that the first and second arguments are the same if they are unified (and that definition is up to us, the writers of the predicate). Thus, same_term(a, a)
will succeed, same_term(a, b)
will fail, and same_term(a, X)
will succeed with X = a
.
You could also write this in a more explicit form:
same_term(X, Y) :-
X = Y. % X and Y are the same if they are unified
Now let's look at your example, val_and_remainder/3
. First, what does it mean?
val_and_remainder(X, List, Rest)
This means that X
is an element of List
and Rest
is a list consisting of all of the rest of the elements (without X
). (NOTE: You didn't explain this meaning right off, but I'm determining this meaning from the implementation your example.)
Now we can write out to describe the rules. First, a simple base case:
val_and_remainder(X,[X|Xs],Xs).
This says that:
Xs
is the remainder of list[X|Xs]
withoutX
.
This statement should be pretty obvious by the definition of the [X|Xs]
syntax for a list in Prolog. You need all of these arguments because the third argument Xs
must unify with the tail (rest) of list [X|Xs]
, which is then also Xs
(variables of the same name are, by definition, unified). As before, you could write this out in more detail as:
val_and_remainder(X, [H|T], R) :-
X = H,
R = T.
But the short form is actually more clear.
Now the recursive clause says:
val_and_remainder(X, [Y|Ys], [Y|R]) :-
val_and_remainder(X, Ys, R).
So this means:
[Y|R]
is the remainder of list[Y|Ys]
withoutX
ifR
is the remainder of listYs
without the elementX
.
You need to think about that rule to convince yourself that it is logically true. The Y
is the same in second and third arguments because they are referring to the same element, so they must unify.
So these two predicate clauses form two rules that cover both cases. The first case is the simple case where X
is the first element of the list. The second case is a recursive definition for when X
is not the first element.
When you make a query, such as val_and_remainder(2, [1,2,3], R).
Prolog looks to see if it can unify the term val_and_remainder(2, [1,2,3], R)
with a fact or the head of one of your predicate clauses. It fails in its attempt to unify with val_and_remainder(X,[X|Xs],Xs)
because it would need to unify X
with 2
, which means it would need to unify [1,2,3]
with [2|Xs]
which fails since the first element of [1,2,3]
is 1, but the first element of [2|Xs]
is 2.
So Prolog moves on and successfully unifies val_and_remainder(2, [1,2,3], R)
with val_and_remainder(X,[Y|Ys],[Y|R])
by unifying X
with 2, Y
with 1, Ys
with [2,3]
, and R
with [Y|R]
(NOTE, this is important, the R
variable in your call is NOT the same as the R
variable in the predicate definition, so we should name this R1
to avoid that confusion). We'll name your R
as R1
and say that R1
is unified with [Y|R]
.
When the body of the second clause is executed, it calls val_and_remainder(X,Ys,R).
or, in other words, val_and_remainder(2, [2,3], R)
. This will unify now with the first clause and give you R = [3]
. When you unwind all of that, you get, R1 = [Y|[3]]
, and recalling that Y
was bound to 1, the result is R1 = [1,3]
.