Тотальность: как доказывается завершение

Пометка тотальная ничего не значила бы, если бы её не проверяли. Проверяет flang/src/totality.mjs — 418 строк, из которых первые шестьдесят представляют собой развёрнутое объяснение метода. Это самая нестандартная часть языка, и разбирать её стоит подробно.

Идея

Значения flang — конечные деревья: список, запись, вариант, скаляр. Значит, отношение «часть значения» вполне обосновано: бесконечной убывающей цепочки частей не бывает. Достаточно показать, что вдоль любой цепочки рекурсивных вызовов один и тот же аргумент строго убывает по этому отношению.

Из шапки модуля:

Задача модуля: превратить обещание «эта функция завершается» в проверенный факт.

Происхождение значений

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

null                                      — про значение ничего не известно
{ param: i, name: "элементы", depth: 0 }  — это сам параметр i
{ param: i, name: "элементы", depth: k }  — часть параметра i, k разборов вглубь

Происхождение растёт вглубь там, где значение достаётся из значения: хвост и голова от списка, привязки образца голова и хвост, поля варианта в образце, поле записи, элемент коллекции в отобразить / отфильтровать / свёртка.

Происхождение теряется там, где значение строится: конструктор варианта, литерал списка, добавить … к …, арифметика, результат любого вызова.

пусть переносит происхождение значения на имя. если и разбор объединяют ветви, беря минимальную глубину при совпадающем параметре.

Вызов убывает на позиции j, если j-й аргумент имеет происхождение { param: j, depth ≥ 1 } — то есть на месте j-го параметра стоит собственная часть j-го параметра вызывающей функции.

Отсюда канонический вид тотальной рекурсии:

тотальная функция «Длина»
  принимает элементы: список числа
  возвращает число
  разбор элементов
    случай пусто
      то 0
    случай голова и хвост
      то 1 плюс «Длина» от хвоста

хвост пришёл из образца, значит его глубина на единицу больше, чем у элементы. Убывание доказано.

Единая позиция в цикле

Взаимная рекурсия разбирается через компоненты сильной связности графа вызовов. Компонента с внутренним циклом принимается, если существует одна и та же позиция аргумента, убывающая на каждом ребре компоненты.

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

«А»(a, b) вызывает «Б»(хвост a, добавить x к b)   — убывает на позиции 1
«Б»(a, b) вызывает «А»(добавить x к a, хвост b)   — убывает на позиции 2

Каждое ребро где-то убывает, но пара (a, b) по кругу растёт, и цикл бесконечен. Правило «каждое ребро убывает хоть где-нибудь» неверно; единая позиция даёт настоящую убывающую цепочку частей одного значения, а она обязана оборваться.

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

Что анализ отвергает

Список записан в самом модуле, в разделе «Чего анализ не умеет (сознательно)»:

• лексикографическое убывание (функция Аккермана);
• убывание по числовому счётчику (n − 1);
• убывание через результат другой функции (хвост от «Отсортировать» от списка);
• разные убывающие позиции у разных рекурсивных вызовов одной функции.

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

Самый частый случай на практике — второй. Проверяем:

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

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

Диагностика заслуживает похвалы: она называет функцию, номер аргумента, выражение и — главное — перечисляет, что именно считается допустимым убыванием.

Как с этим живут

В репозитории видно три приёма обхода.

Свёртка по заранее известному списку

Самый частый. Вместо цикла «пока есть символы» берётся конечный список и сворачивается. Из решения про анаграммы (flang/examples/leetcode/049-group-anagrams.flang):

свёртка ["a", "b", "c", …, "z"] начиная с "" как акк и буква
  соединить (соединить акк с (к строке («Счёт буквы» от слово и буква))) с ","

Свёртка по литеральному списку конечна по построению, поэтому функция остаётся тотальной, хотя «по смыслу» это цикл.

То же в flang/core/json.flang: экранирование строки не обходит её по символам, а сворачивается по таблице из 34 замен.

Стек как список

В flang/core/lexer.flang стек отступов — список чисел, и закрытие нескольких уровней сразу становится рекурсией по хвосту стека. В комментарии к файлу записано, что это сняло «единственное место, где напрашивалась бы рекурсия по числу».

Список-топливо

Когда убывание по мере всё-таки нужно, в сигнатуру добавляется список, длина которого ограничивает число шагов. В index.json этот приём назван честно: «Обход есть (список-топливо), но он засоряет сигнатуру».

Или отказ от тотальности

Последний вариант — просто не ставить пометку. Так поступает flang/stdlib/strings.flang для всего, что идёт по строке посимвольно, и решение LeetCode 20 для функции «Символы с позиции». Комментарий в решении объясняет разделение:

«Скобки в списке» принимает список символов и тотальна: стек живёт в накопителе свёртки […] «Скобки в строке» принимает строку, как в условии, и тотальной быть не может: чтобы получить символы, строку надо обойти, а убывание строки анализ завершаемости не признаёт.

Сколько это стоит в цифрах

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

В том же файле «разложение строки» названо самой дорогой недостачей языка: «она одна делает нетотальными задачи 13, 14, 20, 125».

Ядро FTS, переписанное на flang, держится лучше: в flang/core/SPEC.md слова «Тотальность: долгов нет» стоят под каждым из четырёх слоёв — лексером, печатью JSON, вычислителем и парсером. Все 300 функций ядра помечены и доказаны totality.mjs. Особенно показателен парсер: в нём 208 функций, он разбирает обе поверхности FTS — и отступную, и скобочную, — и всё равно обходится без рекурсивного спуска по потоку токенов, потому что «остаток потока стал короче» анализ убыванием не считает. Скобочный диалект спускается не по потоку, а по дереву скобок, где поддерево — поле варианта, то есть честно меньшая часть значения.

Достигнуто это ценой упомянутых приёмов, и одно расхождение с оригиналом (нормализация NFC) осталось именно потому, что выразить её через разделить и подстрока нельзя.

Стоит ли оно того

Аргумент за — глава «Два класса программ»: тотальность даёт факт-чекингу право отвечать, а не гадать. Аргумент против виден в тех же файлах: чтобы остаться в классе, код местами пишется не так, как думает автор, а так, как примет анализ. Свёртка по алфавиту вместо обхода строки — приём умный, но это приём.

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

Дальше — глава «Стандартная библиотека», где все эти приёмы видны в работе.