Объявить нат и снять проверку из напечатанного кода удаётся только там, где вызывающий уже даёт натуральное: один случай из шести

Рекурсия «число минус 1 с проверкой на дно» доказывается двумя разными способами, и разница видна не в ведомости, а в напечатанном коде:

• постоянным шагом — доказательство полное для вещественных чисел, но на IEEE-754 х минус 1 при большом |х| равен самому х, поэтому на рекурсивный вызов ставится проверка во время работы;
• точным шагом — если довод объявлен нат, дно (0) и потолок (2⁵³−1) даёт сам тип, внутри потолка шаг точен, и проверки в напечатанном коде нет вовсе.

Соблазн переводить первое во второе объявлением типа упирается в проверку типов: нат требуется НА ВЫЗОВЕ, а вызывающий обычно передаёт число.

Чем подтверждено. Ветка vypusk/zavershaemost, коммит a06d3bed. Шесть функций корпуса доказывались постоянным шагом. Попытка объявить довод нат у всех шести: у пяти flang check отвечает FLANG_TYPE, «ожидался нат, получен число» — «Башня из» (вызывающий даёт число дисков), «Повторить знак» (счёт лежит в накопителе свёртки), «Номера аргументов» (арность приезжает полем записи) и их английские близнецы. Прошла одна — «Пробелы» в self/emit-c.flang: вызывающий передаёт длина «начало», а длина уже натуральная. Ведомость корпуса: точный шаг 29 → 30, постоянный шаг 12 → 11, мест проверок в рантайме 110 → 109.

Два ограничения точного шага, о которые спотыкаются заново. Первое: он доказывает только ПРЯМУЮ рекурсию — функция зовёт себя саму; на цикле из двух и более функций он не срабатывает, там нужна общая убывающая позиция. Второе: дно обязано читаться как «не больше 0» или «меньше 0», а НЕ как «равен 0». Равенство границы не даёт по делу: «Ф» от (−5) при базе если н равен 0 уходит в минус бесконечность и не останавливается никогда. Ровно на этом стоят три «крутить» корпуса (conc/examples/budget.flang, examples/web/shortener/server.flang, …/handler-without-budget.flang) — база у них написана равенством, и они обычны по делу, а не по недосмотру.

Чему учит. Правило «объявляй нат там, где значение неотрицательно» верно, но применять его надо СВЕРХУ ВНИЗ — от того, кто число рождает, к тому, кто его считает. Объявление у одного получателя ничего не даёт и только ловит отказ типов; чтобы проверка ушла, натуральным должен стать весь путь числа, включая поля записей, через которые оно едет.

Связано: only-293-of-2242-functions-lacked-a-mark-the-rest-lack-rules, integer-division-does-not-give-the-kernel-nat