[SOLVED] How do you prove termination of a recursive list length?

How do you prove termination of a recursive list length?

Suppose we have a list:

List = nil | Cons(car cdr:List).

Note that I am talking about modifiable lists! And a trivial recursive length function:

recursive Length(List l) = match l with
   | nil => 0
   | Cons(car cdr) => 1 + Length cdr
end.

Naturally, it terminates only when the list is non-circular:

inductive NonCircular(List l) = {
   empty: NonCircular(nil) |
   \forall head, tail: NonCircular(tail) => NonCircular (Cons(head tail))
}

Note that this predicate, being implemented as a recursive function, also does not terminate on a circular list.

Usually I see proofs of list traversal termination that use list length as a bounded decreasing factor. They suppose that Length is non-negative. But, as I see it, this fact (Length l >= 0) follows from the termination of Length on the first place.

How do you prove, that the Length terminates and is non-negative on NonCircular (or an equivalent, better defined predicate) lists?

Am I missing an important concept here?

Solution

Unless the length function has cycle detection there is no guarantee it will halt!

For a singly linked list one uses the Tortoise and hare algorithm to determine the length where there is a chance there might be circles in the cdr.

It's just two cursors, the tortoise starts at first element and the hare starts at the second. Tortoise moves one pointer at a time while the hare moves two (if it can). The hare will eventually either be the same as the tortoise, which indicates a cycle, or it will terminate knowing the length is 2*steps or 2*steps+1.

Compared to finding cycles in a tree this is very cheap and performs just as well on terminating lists as a function that does not have cycle detection.