I am starting Prolog, courtesy of Seven Languages in Seven Weeks, and struggling a bit with understanding how Prolog is handling recursion.
Given the following code:
sum(0, []).
sum(Total, [Head|Tail]) :- sum(Sum,Tail), Total is Head + Sum.
% executed in the Prolog interpreter:
sum(X, [1,2,3])
X = 6
I understand what this code is doing, but I am a little hung up on how the Prolog is resolving the recursive calls of sum. Mainly, it is strange to me that there is no explicit "return" within sum.
My understanding is that something like this happens:
A. The interpreter attempts to unify the rule sum(X, [1,2,3]) by calling sum:
0 Sum(X, [1, 2, 3])
1 Sum(Y, [2,3]
2 Sum(Z, [3])
3 Sum(0, []) % our recursive base
B. Once we hit the base fact, it climbs back up the recursive "stack":
3 Sum(0, []), Total = 0 % we start at our base fact
2 Sum(1, [3]), Total = 3
1 Sum(2, [2, 3]), Total = 5
0 Sum(X, [1, 2, 3]) Total = 6 % sweet, sweet unification
Is my understanding of how this is functioning correct? Or is there a better way for my imperative mind to think about/express what is going on above?
Yup, your thinking is correct. I'll reword slightly what you said just so that it's maybe a bit clearer.
The first thing to do to understand Prolog execution is to realize that Prolog is like a weak theorem prover. It will try to make your queries true. So, when you enter the query ?- sum(X, [1,2,3])., Prolog will do its best to make it true. In that case, as we'll see, it will require binding X to 6, let's see how.
The only elements you gave Prolog to prove that sum(X, [1, 2, 3]) is true are
sum(0, []).
and
sum(Total, [Head|Tail]) :- sum(Sum,Tail), Total is Head + Sum.
Obvisouly, Prolog can't do anything with the first clause, because it can't unify [] and [1, 2, 3]. So it tries to prove your query by using the second clause.
Then what happens is that it tries to prove sum(Sum,Tail) and Total is Head + Sum sequentially. Proving the first of those two options will induce the recursive call and ultimately it will be called with Tail = []. At this point, Prolog will use the first clause you gave it and will deduce that Sum is therefore 0. It will now have the elements to prove the second part (Total is Head + Sum) at the last step of the recursion. Then the recursion is worked back up to the initial predicate as you guessed.