Like rev , sum-a processes the numbers on the list one by one. The goal is to add up these numbers. When we apply sum-a we must use 0 as the value of accumulator , because it hasn't processed any of the numbers on alon yet. Given a precise invariant, the rest is straightforward again. If alon is empty , sum-a returns accumulator because it represents the sum of all numbers on alon now.
Figure contains the final definition of the accumulator-style version of sum .
On the left side, we see how the plain recursive function descends the list of numbers all the way to the end and sets up addition operations on the way. On the right side, we see how the accumulator-style version adds up the numbers as it goes. Furthermore, we see that for each application of sum-a the invariant holds with respect to the application of sum . A second difference between the two functions concerns the order of addition. While the original version of sum adds up the numbers from left to right, the accumulator-style version adds them up from right to left.