Что даёт признак `тотальная`

тотальная перед словом функция — обещание компилятору: функция завершается на любом входе. Два способа из трёх компилятор доказывает при сборке и без доказательства файл не собирает; у третьего проверка переезжает в запуск, и об этом ниже отдельный раздел. Функция без признака пишется как угодно, но её нельзя позвать ни из проверки фактов (flang facts), ни из обработчика процесса.

Файлы-пробы ниже названы коротко — nt1.flang, nt2.flang и так далее; отказы приведены дословно, вместе с именем файла, которое компилятор в них печатает.

	`тотальная`	обычная `функция`
рекурсия	обязана убывать одним из трёх способов ниже	любая
что при отказе	`FLANG_NOT_TOTAL`, файл не собирается	—
`flang facts`	берёт	отказывает
обработчик процесса	годится	нужен запас витков

Первый отказ, который вы увидите

модуль «Проба»

тотальная функция «Обратный отсчёт»
  принимает н: число
  возвращает число
  если н равен 0
    то 0
    иначе «Обратный отсчёт» от (н минус 1)

flang check nt1.flang

модуль «Проба»: функций 1, из них с доказанным завершением 0; типов 0
без доказанного завершения: «Обратный отсчёт»
FLANG_NOT_TOTAL в файле nt1.flang, строка 8, столбец 11: тотальная функция «Обратный отсчёт»: рекурсивный вызов «Обратный отсчёт» не убывает — аргумент 1 («н» sub 1) уменьшает параметр «н», но снизу «н» ничем не ограничен: добавьте проверку вида «если н не больше 0». Передавайте часть аргумента: хвост списка из образца «голова и хвост», поле варианта из образца, поле записи или элемент коллекции
nt1.flang: не проверено — замечаний 1

Отказ называет и место, и лечение. Разница между равен 0 и не больше 0 тут не стилистическая: на н равном -1 первая проверка не срабатывает, и цепочка уходит в минус бесконечность. Одно слово — и файл собирается:

тотальная функция «Обратный отсчёт»
  принимает н: число
  возвращает число
  пример «Считает до нуля»
    дано н равно 5
    ожидается 0
  если н не больше 0
    то 0
    иначе «Обратный отсчёт» от (н минус 1)

flang test nt2.flang

nt2.flang: примеров 1, прошло 1, не прошло 0

Три способа убывать

1. По части значения

Хвост списка, поле варианта, поле записи. Ничего объявлять не надо — компилятор видит это сам. Так написана половина библиотеки; вот «Длина» из flang/stdlib/lists.flang:

тотальная функция «Длина» от «А»
  принимает элементы: список «А»
  возвращает число
  обеспечивает «счёт звеньев сходится со встроенной длиной» результат равен (длина элементы)
  пример «Три элемента»
    дано элементы равно [7, 8, 9]
    ожидается 3
  разбор элементов
    случай пусто
      то 0
    случай голова и хвост
      то 1 плюс «Длина» от хвоста

хвоста — часть элементов, а не новое значение. Этого достаточно.

2. Постоянный шаг с проверкой снизу

Число, уменьшающееся на константу, и ветвь, которая обрывает спуск. Оба условия обязательны: без шага цепочка может не убывать вовсе, без проверки — уйти в минус. «Факториал» из flang/stdlib/numbers.flang:

тотальная функция «Факториал»
  принимает число: неотрицательное
  возвращает число
  обеспечивает «факториал не меньше единицы» 1 не больше результат
  пример «Пять факториал»
    дано число равно 5
    ожидается 120
  если число не больше 1
    то 1
    иначе число умножить на («Факториал» от (число минус 1))

Шагом годится и параметр (н минус ш) — если он приходит в вызов на своём месте неизменным и про него известно строго ш больше 0. Без строгой границы шаг может оказаться нулевым, а меняющийся шаг до дна не доводит вовсе: ш, ш делить на 2, … в сумме меньше 2ш.

3. Объявленная мера `убывает`

Когда убывает не аргумент, а выражение от аргументов. Строка убывает … стоит сразу после возвращает. Пример целиком — docs/examples/measure/binary-search.flang:

тотальная функция «Поиск в диапазоне»
  принимает элементы: список числа, цель: число, низ: число, верх: число
  возвращает число
  убывает верх минус низ плюс 1
  если низ больше верх
    то -1
    иначе
      пусть сумма равно низ плюс верх
      пусть середина равно (сумма минус (сумма остаток от 2)) делить на 2
      пусть значение равно элемент середина в элементы
      если значение равен цель
        то середина минус 1
        иначе
          если значение меньше цель
            то «Поиск в диапазоне» от элементы и цель и (середина плюс 1) и верх
            иначе «Поиск в диапазоне» от элементы и цель и низ и (середина минус 1)

flang test docs/examples/measure/binary-search.flang

docs/examples/measure/binary-search.flang: примеров 5, прошло 5, не прошло 0

`убывает`: доказано, отказ или проверка при запуске

Первые два способа компилятор доказывает. В третьем он читает каждый рекурсивный вызов по форме аргумента и даёт один из трёх ответов.

Доказано. Мера объявлена на параметре типа неотрицательное, и вызов передаёт этот параметр минус постоянную: дно и потолок даёт тип, шаг точен. Проверки в напечатанном коде не остаётся:

модуль «Проба»

тотальная функция «Через два»
  принимает н: неотрицательное
  возвращает число
  убывает н
  если н не больше 1
    то н
    иначе «Через два» от (н минус 2)

  «Через два»  доказано точным шагом: аргумент 1 («н») объявлен натуральным и убывает на 2; дно и потолок даёт тип, внутри потолка шаг точен — сторожа нет

Отказ. Вызов, который не может уменьшить меру, — само имя, н плюс 1, (3 умножить на н) плюс 1, — отвергается уже при check, и сообщение называет вызов и аргумент:

модуль «Проба»

тотальная функция «Вечность»
  принимает н: число
  возвращает число
  убывает н
  «Вечность» от (н плюс 1)

FLANG_NOT_TOTAL в файле nt7.flang, строка 7, столбец 3: тотальная функция «Вечность»: мера «н» на вызове «Вечность» не убывает — аргумент «н» плюс 1 не меньше меры при любом её неотрицательном значении (Мер✗: само имя, сумма с неотрицательным литералом, произведение на литерал не меньше единицы). Спуск этим вызовом не доказуем, и сторож при работе отказал бы на первом же таком витке; перепишите вызов или меру

Проверка при запуске. Всё остальное компилятор принимает на слово автора и вставляет проверку в код. Сборка проходит:

модуль «Проба»

тотальная функция «Сближение»
  принимает низ: число, верх: число
  возвращает число
  убывает верх минус низ
  если верх не больше низ
    то низ
    иначе «Сближение» от (низ плюс 2) и верх

flang check nt6.flang

модуль «Проба»: функций 1, из них с доказанным завершением 1; типов 0
nt6.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

Запуск — нет. От 0 до 5 шагом два мера идёт 5, 3, 1, −1, и проверка останавливает вызов:

flang run nt6.flang --function "Сближение" --args '{"низ": 0, "верх": 5}'

FLANG_MEASURE: тотальная функция «Сближение»: мера на вызове «Сближение» — «верх» минус «низ» — ушла ниже нуля. Мера обязана оставаться неотрицательной: иначе цепочка уходит в минус бесконечность и убывание ничего не доказывает. Чаще всего это выбор меры, а не ошибка вызова — мере, которая на последнем витке становится −1, обычно не хватает «плюс 1»

Отчёт о доказательствах говорит, какой ответ получила каждая функция:

flang check nt6.flang --proof

чем несётся обещание «тотальная»:
  «Сближение»  доказано объявленной мерой: убывает «верх» минус «низ»; спуск ядром не выведен — на веру: мера объявлена автором, сторож считает её при работе на каждом витке — 1 место

итог:
  функций 1: тотальных 1, обычных 0
  обещание несёт: композиция 0, структура 0, точный шаг 0, постоянный шаг 0, объявленная мера 1
  сторожей в рантайме: 1 место

Практический вывод: если завершение важно доказать, а не проверить, — пишите первым или вторым способом либо мерой на параметре неотрицательное с постоянным шагом. Строка сторожей в рантайме в отчёте показывает, сколько мест в вашей программе доказаны не до конца.

Счёт вверх мерой не является

тотальная функция «Счёт вверх»
  принимает н: число, предел: число
  возвращает число
  если н не меньше предел
    то н
    иначе «Счёт вверх» от (н плюс 1) и предел

FLANG_NOT_TOTAL в файле nt3.flang, строка 8, столбец 11: тотальная функция «Счёт вверх»: рекурсивный вызов «Счёт вверх» не убывает — аргумент 1 («н» add 1) увеличивает параметр «н»; аргумент 2 («предел») — это сам параметр «предел», а не его часть. Передавайте часть аргумента: хвост списка из образца «голова и хвост», поле варианта из образца, поле записи или элемент коллекции

предел границей быть не может: он параметр, а не число, и на каждом витке приходит тем же. Разворачивайте счёт вниз.

Строковые задачи эту границу перешли иначе: встроенная форма разложить … на символы раскладывает строку в список односимвольных строк по кодовым точкам, и посимвольный проход становится рекурсией по хвосту. Благодаря ей docs/examples/rosetta/reverse-string.flang тотален целиком — вместе с кириллицей и эмодзи.

Зачем это нужно: проверка фактов не берёт нетотальные функции

flang facts отвечает на вопрос «верно ли это утверждение об этих данных», и зависнуть на нём права не имеет. Нетотальную функцию он не вычисляет вовсе — вот функция, у которой рекурсия идёт по СВОЕМУ ЖЕ результату, а не по части значения, и доказывать завершение тут нечем:

функция «Цифр в числе»
  принимает число: число
  возвращает число
  если число меньше 10
    то 1
    иначе 1 плюс («Цифр в числе» от («Цифр в числе» от число))

flang facts fc1.flang --claims '["«Цифр в числе» от 5 равно 1"]'

{"ok":false,"results":[{"claim":"«Цифр в числе» от 5 равно 1","holds":false,"why":"функция «Цифр в числе» не помечена как «тотальная»; факт-чекинг допускает только тотальные функции — иначе ответ может не наступить","steps":[…],"status":"refused"}]}

Код возврата 1. У режима нет доступа ни к файлам, ни к сети, ни к часам, и есть жёсткий предел шагов: ответ зависит только от четвёрки «программа, факты, утверждения, пределы» — и потому воспроизводится.

Процессы: правило записано, проверка есть, но код отказа другой

По спецификации сервер в flang — бесконечная последовательность завершающихся витков: бесконечен планировщик, а обработчик, которого он зовёт, обязан завершиться. Обработчик без тотальная и без с запасом N витков программу проходить не должен — код FLANG_HANDLER_NOT_TOTAL.

Двоичный это судит, но отвечает другим кодом. Вот что он отвечает на docs/examples/web/shortener/handler-without-budget.flang, файле, написанном специально для проверки этого правила:

FLANG_UNCOVERED_FAILURE в файле docs/examples/web/shortener/handler-without-budget.flang, строка 13, столбец 1: у процесса «Разборщик» обработчик «шаг разбора» без доказанного завершения — значит отказ «запас витков исчерпан» достижим, — а под надзором этот процесс не стоит: такой отказ уронит программу целиком
…
docs/examples/web/shortener/handler-without-budget.flang: не проверено — замечаний 2

Код возврата 1. FLANG_HANDLER_NOT_TOTAL по-прежнему не выдаётся: нетотальный обработчик без запаса ловится как непокрытый отказ (FLANG_UNCOVERED_FAILURE), а не под именем из спецификации.

Что даёт признак тотальная