如何证明一个递归列表长度的终止

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

除非长度函数有周期检测，否则不能保证它会停止!

对于单链表，我们使用乌龟和野兔算法来确定cdr中有可能存在圆的长度。

这只是两个光标，乌龟从第一个元素开始，兔子从第二个元素开始。乌龟每次移动一个指针，而兔子每次移动两个指针(如果可以的话)。兔子最终会和乌龟一样，这表明了一个循环，或者它会知道长度是2*步骤或2*步骤+1。

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

Answer 2

上面的List定义似乎不允许循环列表。每次调用"构造函数"Cons都会创建一个新的指针，并且以后不允许修改指针来创建循环。

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

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

另一件事，非循环的定义不需要终止。这不是一个程序，这是一个证明。如果它成立，那么你可以检查证明，看看为什么它成立，并在其他证明中使用它。编辑:感谢Necto指出我的错误