Как вы подтверждаете завершение рекурсивной длины списка?

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

Определение списка, которое у вас есть сверху, похоже, не разрешает круговые списки. Каждый вызов конструктора Cons создает новый указатель, и вам не разрешается изменять указатель позже, чтобы создать округлость.

Вам нужно более сложное определение списка, если вы хотите обрабатывать округлость. Вероятно, вам нужно определить ячейку, содержащую значение данных и адрес, и узел, который содержит ячейку, и адрес, указывающий на предыдущий узел, а затем вам нужно будет определить оператора разыменования, чтобы вернуться от адресов к ячейкам. Вы также можете попытаться определить некруглый объект на этом объекте.

Чувство кишки заключается в том, что вам также необходимо определить инъективную функцию из «простого» определения списка, которое у вас выше, до сложного, которое я наметил, и , а затем, наконец, вы сможете доказать свою результат.

Другое дело, определение NonCircular не нужно прекращать. Это не программа, это доказательство. Если оно выполнено, вы можете проверить доказательство, чтобы узнать, почему оно выполнено, и использовать его в других доказательствах. Редактировать: Благодаря Necto для указания, я ошибаюсь.