基于归纳法证明尾递归平方和算法的正确性

首先明确我们要分析的代码：

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); 
}

我需证明这段采用尾递归实现平方和计算的代码的正确性，即证明当n≥1时，sumSqr(n) = 1²+2²+…+n²。目前已完成基础步骤，卡在归纳步骤，恳请提供提示或帮助。

别担心，卡在归纳步骤太正常了——尾递归的证明核心是得先给辅助函数sumHelper找个归纳断言（或者说循环不变式），不能只盯着sumSqr看。这里给你一步步拆解：

• 第一步，先定义针对sumHelper的归纳断言：对于任意非负整数k和任意整数a，sumHelper(k, a) = a + 1² + 2² + ... + k²。
  为什么要带上a？因为sumHelper的第二个参数是累加器，它的作用是把之前计算的平方和存起来，所以断言必须包含这个变量才能体现递归的传递逻辑。

• 基础情况你已经验证过了，这里再对应一下：当k=0时，sumHelper(0, a)直接返回a，而断言右边是a + 0（1到0的平方和为0），显然相等，基础情况成立。

• 重点来了，归纳步骤的推导：
  假设对于某个k≥0，我们的归纳断言成立——也就是sumHelper(k, a) = a + 1² + ... + k²（这是归纳假设）。现在要证明sumHelper(k+1, a) = a + 1² + ... + (k+1)²。

  1. 根据代码逻辑，当k+1≠0时，sumHelper(k+1, a)会执行sumHelper(k, a + (k+1)²)；
  2. 把这个调用代入我们的归纳假设：sumHelper(k, a + (k+1)²) = (a + (k+1)²) + 1² + ... + k²；
  3. 整理这个式子，就得到a + 1² + ... + k² + (k+1)²，这正好就是我们要证明的sumHelper(k+1, a)的结果。

• 最后回到sumSqr(n)：它调用的是sumHelper(n, 0)，把a=0代入我们的断言，结果就是0 + 1² + ... + n²，完全符合我们要证明的结论。

如果还有卡壳的地方，不妨把归纳假设和递归调用的每一步都写在纸上，一步步代入，很快就能理清逻辑啦！

内容的提问来源于stack exchange，提问作者Manny