确定递归函数的循环不变式：数组长度差递归函数分析

嘿，我来帮你理清这个递归函数的循环不变式问题～首先得说一句：虽然这是个递归函数，但递归里的“不变式”和循环的不变式本质是一样的——都是在每一步操作（这里是递归调用）前后都保持成立的断言，用来验证函数的正确性。

先把你给出的代码格式化一下，方便查看：

function func (int arr1_length, int arr2_length) { 
    if (arr1_length == 0 && arr2_length == 0) 
        return 0; 
    if (arr1_length == 0) 
        return arr2_length; 
    if (arr2_length == 0) 
        return arr1_length; 
    return func (arr1_length-1, arr2_length-1); 
}

首先，我们先搞懂这个函数到底在做什么：它其实是在计算两个输入值的绝对差值——也就是|arr1_length - arr2_length|。比如输入3和5，会递归减到0和2，返回2；输入5和3，减到2和0，返回2，结果都是两者的差的绝对值。

现在来说它的循环（递归）不变式：

核心不变式断言 #

在每一次递归调用func(a, b)的入口和返回后，以下断言始终成立：

func(a, b)的返回值等于|a - b|（即a和b的绝对差值）

为什么这个断言是不变式？我们可以分情况验证： #

• 基础情况（递归终止条件）：
  • 当a=0且b=0：返回0，而|0-0|=0，断言成立。
  • 当a=0且b≠0：返回b，而|0 - b|=b，断言成立。
  • 当b=0且a≠0：返回a，而|a - 0|=a，断言成立。
• 递归步骤（迭代/递归调用）：
  当a>0且b>0时，函数会调用func(a-1, b-1)。根据不变式的假设，func(a-1, b-1)的返回值等于|(a-1)-(b-1)|，而这个值化简后就是|a - b|。所以当前调用func(a, b)返回这个结果，自然也满足func(a,b)=|a-b|，断言在递归调用前后都保持成立。
• 初始调用：
  最开始调用func(arr1.length, arr2.length)时，这个断言就是我们最终要验证的结论——函数会返回两个数组长度的绝对差值，而整个递归过程中这个断言一直成立，直到终止条件触发返回结果。

简单来说，这个不变式就是保证了每一次递归调用都在朝着“计算绝对差值”的目标前进，而且每一步的结果都符合我们的预期，不会偏离正确逻辑。

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