# Proving the correctness of a square summing algorithm

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.

• You need to prove by induction what sumHelper(n, a) returns. sumSqr is then just trivial. – gnasher729 May 15 '18 at 21:37

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 :-)

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.$$