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

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

Обычно язык встаёт на одну сторону. Промышленные языки берут полноту и отказываются от гарантий. Помощники доказательств вроде 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. У тотальной функции они гарантированно завершатся. У обычной — как повезёт: спасает только лимит шагов интерпретатора.

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

Строка про печать в таблице стоит с оговоркой «да, но см. ниже», и оговорка эта поучительна сама по себе: в первой редакции спецификации на её месте стояло «только JS/TS», и это оказалось неправдой. Бэкендов восемь (c, csharp, elixir, go, java, js, python, rust), и все восемь печатают функции обоих классов. Запрещать печать обычной функции было бы и неверно по существу — раздел 1 flang/SPEC.md теперь формулирует это прямо:

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

Настоящая разница в другом, и она наблюдаема ровно на тех программах, которые не завершаются: лимит шагов воспроизведён не везде. В семи целях из восьми незавершающаяся функция упирается в тот же миллион шагов, что у интерпретатора, и даёт тот же код с тем же текстом — мы проверили это на собранных C, Rust, Python, Java и Elixir, а в напечатанных Go и C# лимит виден прямо в тексте программы. Печатаемый JS остаётся один: лимита шагов там нет, и функция крутится вечно — но это записанное в шапке flang/src/emit/js.mjs решение, а не долг, потому что на выходе там обычный модуль, а не вычислитель. Предел глубины есть везде, включая C, потому что переполнение стека в C — падение процесса, а не исключение.

Мы это проверили запуском по всем целям, до которых дотянулись инструментами (тулчейнов Go и .NET на машине нет); прогон и его неожиданный побочный результат — в главе «Кодогенерация».

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

Цена решения

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

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

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

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

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

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

Ядро FTS, переписанное на flang (flang/core/), тотально целиком: 300 функций, все доказаны. Компилятор самого языка, уже переписанный на flang (flang/self/), тотален почти на две трети: 797 доказанных функций из 1269 после связывания. И это не отставание, а решение, записанное в первых строках flang/self/SPEC.md:

Главное, что делает её проще ядра: компилятору тотальность не нужна. Тотальность обязательна для факт-чекинга — система, отвечающая «подтверждено или нет», не имеет права зависнуть. Компилятор же имеет право упереться в лимит шагов и честно сказать об этом.

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

Отсюда практическое правило, которое стоит унести из этой главы: пометка тотальная — не знак качества, а обязательство перед тем, кто вызывает. Ставить её надо там, где обязательство есть, и не ставить там, где его нет. Оба каталога — core/ и self/ — разобраны в главе «Ядро FTS на flang».

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

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

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

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