0

リストがあるとします：

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

ここで重要な概念が欠けていますか?

4

2 に答える 2

0

長さ関数にサイクル検出がない限り、停止する保証はありません!

単方向リストの場合、うさぎと亀のアルゴリズムを使用して、 内に円が存在する可能性がある長さを決定しcdrます。

2 つのカーソルだけです。亀は最初の要素から始まり、ウサギは 2 番目の要素から始まります。カメは一度に 1 つのポインターを移動しますが、ウサギは 2 つ移動します (可能な場合)。ウサギは最終的にカメと同じになるか、サイクルを示します。または、長さが 2*steps または 2*steps+1 であることを認識して終了します。

ツリー内のサイクルを見つけるのに比べて、これは非常に安価であり、サイクル検出を持たない関数と同様に終了リストでうまく機能します。

于 2015-09-07T23:15:51.823 に答える