recursionprolog# Understanding recursive rules in Prolog

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?

Solution

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.

- Codility OddOccurrencesInArray Problem - Recursion and Python
- Understanding recursive rules in Prolog
- How do I recursively disable my components in Swing?
- How do you recursively unzip archives in a directory and its subdirectories from the Unix command-line?
- Recursive Lambda to join full parent-child hierarchy
- Recursive items in JSON schema
- Recursive euclidean distance
- Recursion Binary to Decimal
- How to a create recursive variable per group in data frame?
- getting TLE in leetcode question 212- word search 2 using backtrcaking even after pruning, how do i optimize it more
- Way to go from recursion to iteration
- lazily calling functions for infinite sequence clojure
- How to create or convert from input to output optimized way?
- Does this criteria prove that Y calls X in infinite recursion?
- SQL Server recursive query in a CTE issue
- Why <slot item={child} /> is needed for the nested object to be displayed if <slot item={item} /> is present?
- How to loop over a multidimensional objectArray with Smarty?
- TypeScript recursive union function type
- Time complexity for recursive binary search that also prints current subarray
- How can I fix an error the error `Cannot build rewrite system for generic signature; rule length limit exceeded` in swift?
- Find the parent element of an array by the id of its child
- recursion on nested list need some support
- How do you prove termination of a recursive list length?
- python recursion i dont understand this output pls help me
- Why does recursively running `joblib.Parallel` increases the computation time?
- How to get Vivado to properly respect recursive module instantiation?
- I'm trying to understand recursion in Tcl, but every time the recursion finishes it throws errors
- How to remove all numbers from a list in Lisp
- Calculate the total weight of segments
- Why does the expression !(cin>>word) cause infinite recursion?