Reasoning with Accumulators
---------------------------

Here is an accumulator style definition of sum:
;; LoN Number -> Number
(defun sum-acc (xs acc)
  (cond ((endp xs) acc)
	((consp xs) (sum-acc (cdr xs) (+ (car xs) acc)))))

;; LoN -> Number
(defun sum (xs) (sum-acc xs 0))

For reference, here is the structurally recursive version:

;; LoN -> Number
(defun sum-sr (xs)
  (cond ((endp xs) 0)
	((consp xs) (+ (car xs) (sum-sr (cdr xs))))))

Let's try to show that sum behaves the same as sum-sr.

Theorem 1:  all xs:LoN, (sum xs) = (sum-sr xs).
Proof:  Structural induction on xs.

The base case is easy, and so we focus on the inductive case.  Take any x:LoN and assume (sum x) = (sum-sr x).  We must show (sum (cons n x)) = (sum-sr (cons n x)) for an arbitrary n:Number.  Using the definitions:

(sum (cons (n x)))
 = (sum-acc (cons n x) 0)
 = (sum-acc x n)

We're stuck here, so let's try to simplify the RHS:

(sum-sr (cons n x))
 = (+ n (sum-sr x))

We claim that it is indeed the case that (sum-acc x n) = (+ n (sum-sr x)).  (See the next lemma.)
Q.E.D.

Lemma 1:  all x:LoN, n:Number, (sum-acc x n) = (+ n (sum-sr x))
Proof:  Structural induction on x.

Base case:  We must show all n:Number, (sum-acc nil n) = (+ n (sum-sr nil)).

Choose an arbitrary number k.  Then
  (sum-acc nil k) = k = (+ k 0) = (+ k (sum-sr nil)).

Since k was arbitrary, we have all k.(sum-acc nil k) = (+ k (sum-sr nil)) which is equivalent to what we had to show (renaming k to n).  

Inductive case:
Take any x:LoN and assume all n:Number. (sum-acc x n) = (+ n (sum-sr x)).  

We must show: 
  all n,k:Number (sum-acc (cons k x) n) = (+ n (sum-sr (cons k x))) 
So choose two arbitrary numbers a and b and plug them in for n and k, respectively:

  (sum-acc (cons b x) a)
  = (sum-acc x (+ b a))

We can use the induction hypothesis here by plugging (+ b a) in for n to obtain:

 = (+ (+ b a) (sum-sr x))
 = (+ a (+ b (sum-sr x)))
 = (+ a (sum-sr (cons b x)))

But since we chose a and b arbitrarily, we have
  all n,k:Number (sum-acc (cons k x) n) = (+ n (sum-sr (cons k x)))

Q.E.D.

Phew.  Finally, we have proved that sum and sum-sr behave the same, even though they compute differently.  But the payoff for all this work is high.  Since sum = sum-sr, any property that we prove about sum-sr automatically transfers over to sum.  And, as we have seen, it is easier to reason about functions that do not use accumulators.  For example, some time ago we proved:

Theorem 2:  all xs, ys:LoN. (sum-sr (append xs ys)) = (+ (sum-sr xs) (sum-sr ys))
Proof:  Structural induction on xs.  
Q.E.D.

Let's prove the analogue for sum:

Theorem 3:  all xs, ys:LoN. (sum (append xs ys)) = (+ (sum xs) (sum ys)).
Proof:  We apply Theorem 1 to change sum into sum-sr:

  all xs, ys:LoN. (sum-sr (append xs ys)) = (+ (sum-sr xs) (sum-sr ys)).

But this is exactly Theorem 2.  
Q.E.D.

This exemplifies a pattern that you should keep in mind for reasoning about accumulator style functions:

 (1) Restate the definition of the accumulator style function without the accumulator.
 (2) Prove that the accumulator style function is equal to the simpler one (e.g., sum = sum-sr).
 (3) Prove whatever theorem you're interested in on the simpler one (e.g., Theorem 2 above).
 (4) Use the equivalence from (2) to conclude that the theorem you're interested in holds for the accumulator style function too.

In practice, step (2) is the where most of the work is.  Go back and look at the end of the proof for Theorem 1 again.  We had to discover a lemma in the inductive case that allowed us to move the accumulator around.  This always happens when you prove that an accumulator style function is equivalent to it's non-accumulating counterpart, and becoming comfortable with this step is the key to dealing with accumulators.

(More examples were on HW 8).