К README · Указатель документации
Что даёт признак тотальная
Полнота по Тьюрингу и гарантированная завершаемость несовместимы, поэтому flang не выбирает между ними: он делит программы на два класса, а к какому классу относится ваша — решает компилятор.
тотальная | обычная | |
|---|---|---|
| рекурсия | убывающая: по части значения или по числовой мере со сторожем | любая |
| завершаемость | доказана компилятором | не гарантируется |
| её примеры | гарантированно завершаются | могут упереться в лимит шагов |
| допускается в факт-чекинг | да | нет |
тотальная требует, чтобы каждый рекурсивный вызов получал убывающий аргумент, и убывания принимаются двух видов: структурное — хвост списка, поле варианта, поле записи — и числовое, по мере. Мера — это н минус <число> при условии, что параметр в точке вызова ограничен снизу проверкой-неравенством (если н не больше 0). Оба условия обязательны: без постоянного шага цепочка может не убывать вовсе, без границы она уходит в минус бесконечность. Шагом годится и ПАРАМЕТР (н минус ш) — если он приходит в вызов на своём месте неизменным и про него известно строго ш больше 0: тогда вдоль всей цепочки вычитается одно и то же число. Без строгой границы шаг может оказаться нулевым, а меняющийся шаг не доводит до дна вовсе — ш, ш делить на 2, … в сумме меньше 2ш. Если анализ не доказал убывание, вы получаете FLANG_NOT_TOTAL и файл не компилируется: это ошибка, а не предупреждение. Любая существующая модель .fts попадает в тотальный класс по построению.
Счёт ВВЕРХ мерой не является и остаётся вне тотального класса: «Числа от и до» от 1 и н наращивает начало, а конец — параметр, не число, и границей быть не может. Строковые задачи границу перешли раньше и по-другому: встроенная форма разложить … на символы раскладывает строку в список односимвольных строк по кодовым точкам, и посимвольный проход становится рекурсией по хвосту. Благодаря ей flang/examples/rosetta/reverse-string.flang тотален целиком — вместе с кириллицей и эмодзи.
Это не педантизм, и причина вполне конкретная. Встроенный режим факт-чекинга ([flang/src/factcheck.mjs](../../flang/src/factcheck.mjs)) отвечает на вопрос «верно ли это утверждение об этих данных» — а система, обязанная ответить «да» или «нет», не имеет права зависнуть. Поэтому она отказывается запускать функцию, завершаемость которой не доказана, ещё до того, как что-либо вычислит: flang facts отвечает holds: false и называет причину.
У режима нет доступа ни к файлам, ни к сети, ни к часам, и есть жёсткий бюджет шагов: ответ зависит только от четвёрки «программа, факты, утверждения, лимиты» — и потому воспроизводится.