Comments 5
Самое сложное, как я понимаю, именно заказать эквивалентность? Фибоначчи(100) совсем не тоже самое, что Фибоначчи(100,5), т.к. досчитать не успеет. Нужно каким-то образом выставить нижнюю границу fuel, как это можно сделать? В статье не раскрыт этот момент.
Да, подсчет больших чисел - это проблема, он занимает время.
Мы по сути идем индукцией по fuel. Поэтому мы делаем определение fuel непрозначным. Заменяем fuel какой-нибудь константой. Просто, чтобы развернуть ее в нужный момент и доказать, что она соответствует каким-то ограничениям. Поэтому от fibonacci(100,5) все, что нам нужно, это только знать, что это не ноль (что это (S n)). Можно вместо большого числа поставить маленькое число только для того, чтобы проверить некоторые предположения относительно кода.
Не ноль недостаточно. Функция не досчитает, если поставить, например, 5. Если при остановке по fuel вернуть текущий промежуточный результат, то и ответ будет неверным. Это Coq сам отлавливает или каким образом выбирается размер fuel?
Извините, пожалуйста, что ответ пишу столько дней спустя! Я изменила настройки уведомлений и теперь, надеюсь, буду реагировать на вопросы быстрее.
Привожу дистиллированный пример.
Мы имеем функцию, которая не тотальна, кок не может понять, когда эта функция остановится
в своих вычислениях. И отказывается ее компилировать.
Fail Fixpoint run_forever (i : Z) : Z := run_forever (i + 1).
Мы вводим дополнительный параметр n - натуральное число.
Натуральные числа
Inductive nat : Type :=
| O
| S (n : nat).
и говорим коку, что
первое: n на каждом шаге рекурсии уменьшается.
второе: остановить работу функции, когда n станет равным нулю.
Fixpoint run_forever (i : Z) (n : nat) : Z :=
match n with
| O => 1
| S n => run_forever (i + 1) n
end.
Вуаля, функция компилируется. Кок видит, что рекурсия остановится. Теперь мы можем с ней работать дальше, и верифицировать ее другие свойства. Внимание, мы не доказали, что исходная функция тотальна. Мы применили трюк, чтобы иметь возможность с ней работать дальше.
Есть и другие способы, которые прямо внутри кока реализованы, например добавть параметр measure, этот способ описывается тут
https://www.codewars.com/kumite/5d5c0d111d19740029f8b385?sel=5d5c0d111d19740029f8b385
P.S. Я не понимаю фраз "не ноль не достаточно" и "ответ будет неверным", размер fuel тоже не имеет значения. Мы ведь доказываем вопрос "остановится ли функция в своих вычислениях или нет" для математической индукции не важен размер fuel: у нас есть базовый случай (fuel = 0), индукционная гипотеза (fuel + 1), индуктивный переход. В коке это автоматизировано. Мы не ищем конкретного ответа (не сейчас, не в этом доказательстве, не с этим вопросом). Далее, верифицируя эту функцию дальше, мы можем писать о ней новым леммы: ...для всех входных параметров, будет выполняться то-то и то-то. И доказывать их. Вот тогда мы уже будем проверять "верность-неверность" ответа.
Дайте знать, пожалуйста, ответила ли я на ваш вопрос.
Верификация рекурсивных функций в Coq. Проблема остановки. Горючее