你如何證明遞歸列表長度的終止？

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 *步或2 *步+ 1。

與在樹中查找週期相比，這非常便宜，並且作爲沒有周期檢測的函數在終止列表上執行也是如此。

Answer 2

頂部的List定義似乎不允許循環列表。對「構造函數」Cons的每次調用都會創建一個新指針，並且不允許稍後修改指針以創建圓形。

如果你想處理循環，你需要一個更復雜的List定義。您可能需要定義包含數據值和地址的Cell，以及包含Cell和指向前一節點的地址的Node，然後您需要定義取消引用運算符以從地址返回到單元格。您也可以嘗試在此對象上定義非圓形。

我的直覺是，你還需要定義一個從上面的「簡單」列表定義到我已概述的複雜列表的內射函數，然後然後終於你能夠證明你的結果。

另一件事，NonCircular的定義不需要終止。這不是一個程序，它是一個證明。如果它成立，那麼你可以檢查證明，看看它爲什麼持有，並在其他證明中使用。 編輯：感謝Necto指出我錯了。