如何根据这个递归函数确定度量函数

Question

在ACL2中定义了一个函数，我们的任务是创建一个度量函数来帮助证明终止。下面是函数定义:

(defunc f (x a)
  :input-contract (and (integerp x) (listp a))
  :output-contract (integerp (f x a))
  (cond
   ((endp a)                 68)
   ((equal (len a) x)        71)
   ((equal (len a) (+ x 1))  74)
   ((< x (len a))            (f (+ x 1) (rest a)))
   (t                        (f (- x 1) (cons 1 a)))))

一个解度量函数是这样的(简写):

(m x a) = (if (equal (len a) (+ x 1))
              0
              (abs (- (len a) x)))

基于函数中的两个递归调用，我们能够确定将包含度量函数的else情况。然而，我们不了解它的其余部分，以及计算这个测量函数的过程。

作为参考，一个度量函数:

1. m是定义在f参数上的可容许函数;
2. m与f具有相同的输入合约;
3. m有一个输出合约，声明它总是返回一个自然数;和
4. 在每次递归调用时，应用于该递归调用的参数的m减小，

决定这个度量函数的过程是什么?

Answer 1

在确定度量函数时，要问自己的问题是:每次迭代中消耗的"势能"是多少，直到在某个点上它全部消失并且迭代停止?

首先要看的通常是终止条件。在这种情况下有三个，但最后两个是最有趣的:它们说如果x和(len a)之间的差异太小，我们就停止迭代。

这给了我们一个想法:如果(len a)和x之间的势能是差的呢?要看这是否有意义，我们需要检查递归情况，并确保它们中的每一个都消耗了一些能量，即减少了差值。这里看起来很不错:

• 如果x小于(len a)，则x增大1,(len a)减小1。因此，如果它们之间的差值是n，那么在下一次迭代中，它将是n-2，除非x = (len a) - 1。
• 如果x大于(len a)，则x减小1,(len a)增大1。同样，如果它们之间的差值是n，那么在下一次迭代中，它将是n-2，除非x = (len a) + 1。

从这里很容易看出，我们应该选择x = (len a) + 1作为我们的"低能态"，因为它处理了那两个除非子句的烦人细节。