Два класса программ: тотальная и обычная

Есть старая развилка. Язык, на котором можно выразить любое вычисление, не позволяет доказать про произвольную программу, что она остановится, — это проблема остановки. Язык, где завершение доказуемо всегда, неизбежно чего-то не выражает.

Промышленные языки берут полноту и отказываются от гарантий. Помощники доказательств вроде Coq, Agda или Lean берут гарантии и требуют доказать завершение каждой рекурсии.

flang делит функции на два класса, и класс проверяет компилятор. Обещание записывается одним словом перед функция:

Как это выглядит в коде

Возьмём функцию, про которую никто не знает, завершается ли она на всех входах, — число шагов в гипотезе Коллатца. Без пометки она принимается:

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

функция «Шаги Коллатца»
  принимает н: число
  возвращает число
  если н не больше 1
    то 0
    иначе
      если (н остаток от 2) равно 0
        то 1 плюс «Шаги Коллатца» от (н делить на 2)
        иначе 1 плюс «Шаги Коллатца» от (3 умножить на н плюс 1)

$ flang check collatz.flang
модуль «Проба»: функций 1, из них с доказанным завершением 0; типов 0
без доказанного завершения: «Шаги Коллатца»
collatz.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет
$ flang run collatz.flang --function "Шаги Коллатца" --args '{"н":27}'
доказано: утверждений 0
111

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

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

тотальная функция «Шаги Коллатца»
  принимает н: число
  возвращает число
  если н не больше 1
    то 0
    иначе
      если (н остаток от 2) равно 0
        то 1 плюс «Шаги Коллатца» от (н делить на 2)
        иначе 1 плюс «Шаги Коллатца» от (3 умножить на н плюс 1)

$ flang check collatz.flang
FLANG_NOT_TOTAL в файле collatz.flang, строка 10, столбец 19: тотальная функция «Шаги Коллатца»: рекурсивный вызов «Шаги Коллатца» не убывает — аргумент 1 («н» div 2) не выведен ни из одного параметра. Передавайте часть аргумента: хвост списка из образца «голова и хвост», поле варианта из образца, поле записи или элемент коллекции
FLANG_NOT_TOTAL в файле collatz.flang, строка 11, столбец 22: …
collatz.flang: не проверено — замечаний 2

Отказ консервативный: анализ никогда не признаёт тотальной функцию, которая может зациклиться, и платит за это отказом части функций, которые на деле завершаются. Но признаёт он больше, чем одну структурную рекурсию. Обратный отсчёт н минус 1 с проверкой если н не больше 0 проходит как тотальный — flang check --proof пишет «доказано постоянным шагом», и рядом ставит проверку во время работы на тот редкий случай, когда у дробного числа шаг не меняет значение. А там, где убывает не аргумент, а выражение, автор называет его сам строкой убывает:

модуль «Euclid»

тотальная функция «НОД»
  принимает а: число, б: число
  возвращает число
  убывает б
  пример «Классическая пара»
    дано а равно 1071
    дано б равно 462
    ожидается 21
  если б равен 0
    то а
    иначе «НОД» от б и (а остаток от б)

Убывание такой меры ядро доказательств само не выводит: --proof честно пишет, что мера объявлена автором и считается при работе на каждом витке. Если мера перестанет убывать, функция откажет с кодом FLANG_MEASURE, а не зациклится. Подробно об этом — в главе «Тотальность».

Зачем это нужно

Факт-чекинг

flang facts отвечает на вопрос «подтверждается ли утверждение данными». Такая проверка не имеет права зависнуть, поэтому вызывает только функции с доказанным завершением, и это проверяется до вычисления:

$ flang facts facts.flang --facts f.json \
    --claims '["«Сумма больше порога» от суммы, порог равно да"]' --pretty
{
  "ok": true,
  "results": [
    {
      "claim": "«Сумма больше порога» от суммы, порог равно да",
      "holds": true,
      "why": "«Сумма больше порога» от факта «суммы», факта «порог» = да; требование «равно да» выполнено",
      …
      "status": "verified"
    }
  ]
}

Функция без пометки отклоняется, и в ответе написано почему:

$ flang facts facts.flang --claims '["«Шаги Коллатца» от 6 равно 8"]' --pretty
{
  "ok": false,
  "results": [
    {
      "claim": "«Шаги Коллатца» от 6 равно 8",
      "holds": false,
      "why": "функция «Шаги Коллатца» не помечена как «тотальная»; факт-чекинг допускает только тотальные функции — иначе ответ может не наступить",
      …
      "status": "refused"
    }
  ]
}

Ответ «не могу проверить, вот причина» честнее, чем попытка и тайм-аут.

Примеры-тесты

Примеры лежат внутри функции и исполняются flang check и flang test. У тотальной функции они гарантированно завершатся. У обычной их останавливает предел шагов.

Перевод в другие языки

flang emit печатает функции обоих классов во все десять целей (c, cpp, csharp, elixir, go, java, js, python, rust, ts). Разница в том, что стоит за результатом. У тотальной функции завершение доказано и вне flang. У обычной — только предел шагов, который flang emit вписывает в программу: в каждой из десяти целей по умолчанию 1 000 000 шагов (ключ --max-steps). Функция, которая зовёт себя вечно, в напечатанном JavaScript и Python останавливается с тем же кодом, что и в flang:

{"ok":false,"code":"FLANG_RECURSION_LIMIT","message":"функция «Вечно» исчерпала лимит шагов (1000000) на глубине вызовов 1"}

У самого flang run предел больше — 40 000 000 шагов, и поднимается он ключом --step-limit.

Цена решения

Раньше главной ценой был посимвольный обход строки: убывает в нём не часть значения, а «длина минус позиция», и анализ такую функцию не принимал. Встроенная форма разложить … на символы превращает строку в список, и проход по нему доказывается как рекурсия по хвосту. Сегодня цена видна в числах: в стандартной библиотеке (flang/stdlib/) 2139 функций, и обычных среди них 7 — «НОД», «НОК», «Цифры», «Сумма цифр» и ещё три в math-classics.flang. Из 82 решённых задач LeetCode (docs/examples/leetcode/index.json) нетотальна главная функция ровно одной — «Счастливое число» (202): цикл «пока не единица и пока число не повторилось» не убывает ни по одной мере, которую язык умеет записать.

Вторая цена — обходные приёмы. Чтобы остаться в тотальном классе, иногда приходится менять запись: мера убывает, свёртка по заранее известному списку, список-«топливо». Работает, но это приём, а не естественная запись.

Кому тотальность обязательна, а кому нет

Из деления легко сделать неверный вывод: раз тотальный класс лучше, надо стремиться в него всегда. Репозиторий отвечает своим кодом.

Разбор старых моделей (flang/core/) тотален целиком: 300 функций, все с доказанным завершением. Он отвечает факт-чекеру, и зависнуть не вправе. Компилятор, написанный на flang (flang/self/), тотален не весь: из 11 183 объявленных функций тотальных 8520. Это решение, записанное в первых строках docs/flang/self/SPEC.md:

Компилятору тотальность не обязательна: он вправе упереться в предел шагов и сказать об этом.

Факт-чекер обещает ответ и не имеет права его не дать. Компилятор обещает разобрать или отказать, и «отказ по пределу шагов» — тоже честный ответ.

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

Что здесь стоит запомнить

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

Дальше — глава «Инструмент»: команды flang и их вывод.