2

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 都会减少。

导致确定此测量函数的过程是什么？

4

1 回答 1

1

在确定度量函数时，要问自己的问题是：每次迭代中消耗的“势能”是多少，到了某个时候它全部消失并且迭代停止的程度？

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

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

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

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

于 2013-03-24T15:45:22.580 回答