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

тотальная перед словом функция — обещание компилятору: функция завершается на любом входе. Два способа из трёх компилятор доказывает при сборке и без доказательства файл не собирает; у третьего проверка переезжает в запуск, и об этом ниже отдельный раздел. Функция без признака пишется как угодно, но её нельзя позвать ни из проверки фактов (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. Объявленная мера `убывает`

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

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

flang test examples/measure/binary-search.flang

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

`убывает` — это проверка при запуске, а не при сборке

Первые два способа компилятор доказывает. Третий — нет: объявленную меру он принимает на слово и вставляет проверку в код. Это видно на программе, которая заведомо не кончается:

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

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

flang check nt6.flang

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

Сборка прошла. Запуск — нет:

flang run nt6.flang --function "Вечность" --args '{"н": 1}'

FLANG_MEASURE: тотальная функция «Вечность»: мера на вызове «Вечность» — «н» — не убыла. Завершение доказано тем, что она строго убывает; равенство цепочку не обрывает, а значит этот вызов может не кончиться никогда

Отчёт о доказательствах говорит это прямым текстом — где доказано, а где проверяется по ходу:

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 («предел») — это сам параметр «предел», а не его часть. Передавайте часть аргумента: хвост списка из образца «голова и хвост», поле варианта из образца, поле записи или элемент коллекции

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

Строковые задачи эту границу перешли иначе: встроенная форма разложить … на символы раскладывает строку в список односимвольных строк по кодовым точкам, и посимвольный проход становится рекурсией по хвосту. Благодаря ей 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.

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

проверено НЕ ВСЁ: в программе объявлено то, чего бинарник не судит вовсе — processes.
…
examples/web/shortener/handler-without-budget.flang: проверено НЕ ДО КОНЦА — разбор, типы, завершаемость, ядро и примеры прошли

Код возврата 2, но FLANG_HANDLER_NOT_TOTAL не выдан. Правило живёт в спецификации; проверка на него в компиляторе не написана.

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