Proving the correctness of a square summing algorithm

Question

int sumHelper(int n, int a) {
   if (n==0) return a;
   else return sumHelper(n-1, a + n*n);
}

int sumSqr(int n) { 
    return sumHelper(n, 0); 
}

I am supposed to prove this piece of code which uses tail recursion to sum up the squares of numbers. That is, I need to prove that for $n ≥ 1$, $sumsqr(n)=1^2+2^2+\dots+n^2$. I have figured out the base case but I am stuck at the induction step. Any hints or help will be appreciated.

Answer 1

Assuming $n ≥ 0$, let $$ P(n) \;≡\; ∀ a.\, sumHelper(n, a) = a + ∑_{i = 0}^n i² $$

Then we prove this is always true by induction on $n$.

The base case, n = 0:

  sumHelper(n, a)
={ Case n = 0 }
  sumHelper(0, a
={ Definition }
  a
={ Arithmetic }
  a + 0²
={ Arithmetic }
  a + ∑_{i = 0}^0 i²
={ Case n = 0 }
  a + ∑_{i = 0}^n i²

The induction step, assuming P(n) let us show P(n+1),

 sumHelper(n+1, a)
={ Definition }
  if   (n+1==0) a  
  else sumHelper(n+1-1, a + (n+1)*(n+1))
={ Since we assumed n ≥ 0, we have n+1 ≠ 0.
   Hence we have the else-branch. }
  sumHelper(n+1-1, a + (n+1)*(n+1))
={ Arithmetic }
  sumHelper(n, a + (n+1)*(n+1))
={ Apply the inductive hypotheis with a ≔ a + (n+1)*(n+1) }
  (a + (n+1)*(n+1))) + ∑_{i = 0}^n i²
={ Arithmetic: Bringing the `n+1` term back into the sum }
  a + ∑_{i = 0}^{n+1} i²

We're done :-)

Answer 2

The function sumHelper implements the recurrence

$$a_n=a_{n-1}+n^2,\\ a_0=0,$$

the solution of which is

$$a_n=\sum_{k=1}^n k^2.$$