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

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

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

flang не выбирает. Он делит программы на два класса, и — это важнее самого деления — класс проверяется компилятором, а не декларируется в документации. Формулировка из flang/SPEC.md, раздел 1, приведена там же в виде таблицы:

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

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

Без пометки — принимается:

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

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

$ node flang/bin/flang.mjs check проба.flang --pretty
{
  "valid": true,
  "module": "Проба",
  "functions": [ { "name": "Обратный счёт", "total": false } ],
  "types": [],
  "diagnostics": []
}

Добавляем тотальная — и та же программа перестаёт собираться:

$ node flang/bin/flang.mjs check проба.flang --pretty
{
  "code": "FLANG_NOT_TOTAL",
  "message": "тотальная функция «Обратный счёт»: рекурсивный вызов «Обратный счёт»
    не убывает — аргумент 1 («н» sub 1) не выведен ни из одного параметра.
    Передавайте часть аргумента: хвост списка из образца «голова и хвост»,
    поле варианта из образца, поле записи или элемент коллекции",
  "severity": "error",
  "span": { "line": 8, "column": 18 }
}

Обратите внимание на характер отказа. Функция «Обратный счёт» очевидно завершается: н убывает на единицу и упирается в ноль. Анализ этого не видит — он знает только структурное убывание, «часть значения», а не «число поменьше». Отказ здесь консервативный: анализ никогда не признаёт тотальной функцию, которая может зациклиться, и платит за это отказом части действительно завершающихся программ. Механика разобрана в главе «Тотальность».

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

Деление имело бы мало смысла, если бы за ним ничего не следовало. Следует три вещи.

Факт-чекинг

Встраиваемый режим (flang/src/factcheck.mjs, раздел 8 спецификации) отвечает на вопрос «утверждение подтверждается данными или нет». Система, дающая такой ответ, не имеет права зависнуть — поэтому режим допускает только тотальные функции, и это проверяется до вычисления, по транзитивному замыканию вызовов.

Тотальная функция считается:

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

Обычная — отклоняется, и в ответе написано почему:

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

Ответ «не могу проверить, вот причина» здесь честнее, чем попытка и таймаут. Формулировка из шапки модуля: «Не „попробуем и посмотрим“: попытка исполнить нетотальную функцию и есть тот риск, ради которого введены два класса».

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

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

Печать в целевые языки

Спецификация связывает класс с возможностью кодогенерации. Здесь стоит быть точным, потому что реальность отличается от таблицы в SPEC.md.

Таблица обещает, что тотальные программы печатаются «на C/Rust/Java/…», а обычные — «только JS/TS». На практике бэкендов пять (c, go, js, python, rust), и они печатают функции обоих классов; разница в том, что у напечатанного кода нет лимита шагов. Из шапки flang/src/emit/c.mjs:

Лимита шагов [нет]. Незавершающаяся обычная функция здесь крутится вечно, как и в напечатанном JS. А вот предел ГЛУБИНЫ есть, и это не прихоть: в JS переполнение стека даёт исключение, в C — падение процесса.

То есть класс не запрещает печать, а определяет, что вы получаете на выходе: для тотальной функции завершение доказано и вне интерпретатора, для обычной — нет. Подробнее в главе «Кодогенерация».

Цена решения

Она реальная и видна в стандартной библиотеке. Модуль flang/stdlib/strings.flang открывается признанием:

Главное ограничение, которое здесь видно в каждой функции: строку нельзя разобрать структурно. Образцы «пусто» и «голова и хвост» работают только со списком […] Поэтому всё, что идёт по строке посимвольно, — обычная функция: её завершение обеспечено лимитом шагов интерпретатора, а не доказательством.

То же в решениях задач: в flang/examples/leetcode/index.json из 26 решённых задач тотальны 20. Шесть — обычные, и почти всегда по одной причине: понадобился посимвольный обход строки.

Второй вид цены — обходные приёмы. Чтобы остаться в тотальном классе, авторы stdlib и core заменяют посимвольный обход свёрткой по заранее известному списку. Экранирование JSON в flang/core/json.flang сворачивается по таблице из 34 замен; подпись слова в задаче про анаграммы — по списку из 26 букв алфавита. Работает, но это именно приём, а не естественная запись.

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

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

Насколько это удобно в работе, судить рано: пользователей за пределами репозитория у языка пока нет. Но само устройство развилки читается ясно, и это хороший повод разобрать её на живом коде.

Дальше — глава «Инструмент», чтобы получить инструмент в руки.