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

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

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

我是不是漏掉了一个重要的概念？

Answer 1

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

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

只是两个光标，乌龟从第一个元素开始，兔子从第二个元素开始。乌龟一次移动一个指针，而兔子一次移动两个指针（如果可以的话）。兔子最终要么与乌龟相同，这表示一个循环，要么知道长度为 2*steps 或 2*steps+1 后终止。

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

Answer 2

您在顶部的 List 定义似乎不允许循环列表。每次调用 "constructor" Cons 都会创建一个新指针，以后不允许修改指针来创建循环。

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

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

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

How do you prove termination of a recursive list length?