recursion - 你如何证明递归列表长度的终止？

Question

假设我们有一个列表：

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) 首先是从 of 的终止而来的Length。

你如何证明，在（或等效的，更好定义的谓词）列表Length上终止并且是非负的？NonCircular

我在这里错过了一个重要的概念吗？

score 0 · Accepted Answer

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

对于单链表，使用Tortoise and hare 算法来确定在cdr.

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

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

score 0 · Accepted Answer

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

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

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

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

2 回答 2