你如何证明递归列表长度的终止？答案

【问题标题】：How do you prove termination of a recursive list length?你如何证明递归列表长度的终止？
【发布时间】：2015-09-07 17:00:03
【问题描述】：

假设我们有一个列表：

List = nil | Cons(car cdr:List).

请注意，我说的是可修改列表！还有一个简单的递归长度函数：

recursive Length(List l) = match l with
   | nil => 0
   | Cons(car cdr) => 1 + Length cdr
end.

自然，它仅在列表非循环时终止：

inductive NonCircular(List l) = {
   empty: NonCircular(nil) |
   \forall head, tail: NonCircular(tail) => NonCircular (Cons(head tail))
}

请注意，这个谓词作为递归函数实现，也不会在循环列表上终止。

通常我看到使用列表长度作为有界递减因子的列表遍历终止证明。他们认为Length 是非负数。但是，在我看来，这个事实 (Length l >= 0) 首先是 Length 的终止。

您如何证明Length 在NonCircular（或等效的、定义更明确的谓词）列表上终止且为非负数？

我在这里遗漏了一个重要的概念吗？

【问题讨论】：

【解决方案1】：

除非长度函数有循环检测，否则不能保证它会停止！

对于单链表，使用Tortoise and hare algorithm 来确定@987654322@ 中可能存在圆圈的长度。

这只是两个光标，乌龟从第一个元素开始，兔子从第二个元素开始。乌龟一次移动一个指针，而兔子移动两个（如果可以的话）。兔子最终要么和乌龟一样，这表明一个循环，要么它会在知道长度为 2*steps 或 2*steps+1 的情况下终止。

与在树中查找循环相比，这非常便宜，并且在终止列表上的性能与没有循环检测的函数一样好。

【讨论】：

【解决方案2】：

您在顶部的 List 定义似乎不允许循环列表。对“构造函数” Cons 的每次调用都会创建一个新指针，并且以后不允许修改指针以创建循环。

如果你想处理循环，你需要一个更复杂的 List 定义。您可能需要定义一个包含数据值和地址的单元格，以及一个包含单元格和指向前一个节点的地址的节点，然后您需要定义解引用运算符以从地址返回到单元格。您也可以尝试在此对象上定义非圆形。

我的直觉是，您还需要定义一个单射函数，从上面的“简单”列表定义到我概述的复杂列表，然后然后最终你会能够证明你的结果。

~~另外，NonCircular 的定义不需要终止。这不是程序，而是证明。如果它成立，那么您可以检查证明以了解它为什么成立并在其他证明中使用它。~~ 编辑：感谢 Necto 指出我错了。

【讨论】：