История изменений
Исправление AndreyKl, (текущая версия) :
Здесь всего 100000000000 состояний. То есть можно гарантированно считать функцию не завершающейся, если она не завершилась за 100000000000 итераций, даже если не запоминать предыдущие.
Причём, если проверять снизу вверх, то любое падение ниже того, из которого началась рекурсия, завершает доказательство. Также как и любой вылет выше 100000000000. То есть две трети диапазона проверяются тривиально.
понял спасибо. в таком случае просто передаём число итераций и говорим что по нему завершаемся.
Fixpoint f (k : Z) fuel {struct fuel} : Z :=
match fuel with
| O => 0
| S fuel =>
if k =? 1 then 1
else if k >? 100000000000 then 0
else if k mod 2 =? 0 then f (k/2) fuel
else f (3*k+1) fuel
end.
Запускать как то так
Compute f 3 100000000000.не знаю, будет ли работать (в браузере точно нет) - числа большие.
Исправление AndreyKl, :
Здесь всего 100000000000 состояний. То есть можно гарантированно считать функцию не завершающейся, если она не завершилась за 100000000000 итераций, даже если не запоминать предыдущие.
Причём, если проверять снизу вверх, то любое падение ниже того, из которого началась рекурсия, завершает доказательство. Также как и любой вылет выше 100000000000. То есть две трети диапазона проверяются тривиально.
понял спасибо. в таком случае просто передаём число итераций и говорим что по нему завершаемся.
Fixpoint f (k : Z) fuel {struct fuel} : Z :=
match fuel with
| O => 0
| S fuel =>
if k =? 1 then 1
else if k >? 100000000000 then 0
else if k mod 2 =? 0 then f (k/2) fuel
else f (3*k+1) fuel
end.
Запускать как то так
Compute f 3 100000000000.не знаю, будет ли работать (в браузере точно нет) - числа большие.
Исходная версия AndreyKl, :
Здесь всего 100000000000 состояний. То есть можно гарантированно считать функцию не завершающейся, если она не завершилась за 100000000000 итераций, даже если не запоминать предыдущие.
Причём, если проверять снизу вверх, то любое падение ниже того, из которого началась рекурсия, завершает доказательство. Также как и любой вылет выше 100000000000. То есть две трети диапазона проверяются тривиально.
понял спасибо. в таком случае просто передаём число итераций и говорим что по нему завершаемся.
Fixpoint f (k : Z) fuel {struct fuel} : Z :=
match fuel with
| O => 0
| S fuel =>
if k =? 1 then 1
else if k >? 100000000000 then 0
else if k mod 2 =? 0 then f (k/2) fuel
else f (3*k+1) fuel
end.