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

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

Одно замечание вперёд, потому что оно объясняет, почему эта глава почти не изменилась, пока остальные переписывались наполовину. За сутки в язык приехали функции первого класса и параметрический полиморфизм — то есть ровно те две вещи, которые обычно ломают анализ завершаемости. Анализ не изменился ни на строку. Полиморфизма он не заметил вовсе (объявленных типов totality.mjs не читает: слова «тип» в нём нет ни разу вне шапки), а высший порядок изменил не анализ, а то, чем он питается. Разбор — в главе «Система типов».

Идея

Значения 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 для функции «Символы с позиции». Комментарий в решении объяснял разделение:

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

Прошедшее время здесь не стилистическое. На срезе, по которому писалась прошлая редакция трека, у strings.flang было восемь обычных функций из двадцати — мы пересчитали тот же файл на том же коммите: «Символы с позиции», «Символы», «Обратить строку», «Палиндром», «Обрезать слева», «Обрезать справа», «Обрезать пробелы» и «Повторить». Сегодня осталась одна, «Повторить», и причина у неё уже не про строки: там убывает счётчик повторов, то есть число. Что случилось с остальными семью — в следующем разделе.

Самая дорогая недостача закрыта — и вот чем это обернулось

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

В index.json «разложение строки» было названо самой дорогой недостачей языка: «она одна делает нетотальными задачи 13, 14, 20, 125». Логика была такая: образцы пусто и голова и хвост работают только со списком, поэтому любой посимвольный проход идёт по индексу, а убывает при этом число — то есть то, чего анализ не признаёт.

Недостачу закрыли одной встроенной формой. Проверяем:

тотальная функция «Сколько букв»
  принимает текст: строка
  возвращает число
  пример «Три»
    дано текст равно "мир"
    ожидается 3
  «Длина списка» от (разложить текст на символы)

check — valid: true, обе функции total: true, test — 1 из 1. Строка раскладывается в список, обход становится рекурсией по хвосту, и убывание доказывается как обычно.

Именно этого не хватало, и лучший измеритель — не рассуждение, а то, что стало с файлами.

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

Статистика решений LeetCode из flang/examples/leetcode/index.json: решено 26 задач, тотальны 24. В прошлой редакции этой главы стояло 20 из 26 — четыре задачи перешли в тотальный класс, не изменившись по существу.

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

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

А вот компилятор самого flang, написанный на flang в flang/self/, держится заметно хуже — и это самая полезная цифра во всей главе, потому что она сознательная. Приводим её вместе с прошлой редакцией трека, потому что движение за сутки здесь и есть содержание:

Числа в таблице мы считали по самим файлам (grep -c '^\(тотальная \)\?функция «'), а не по ответу flang check: тот показывает функции уже после связывания модулей и потому насчитывает больше — свои плюс импортированные. У лексера разрыв как раз виден: в файле 84 объявления, а check отвечает 88, добавляя четыре функции из stdlib/strings. Обе цифры верные, и обе полные — важно только не смешивать.

Лексер самоприменения стал тотальным целиком. Ни одной обычной функции: 84 из 84. Это прямое следствие закрытой недостачи — слои перестали ходить по строке позицией. Печать в C прибавила 33 доказанных функции по той же причине, парсер — 41.

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

Разница не в мастерстве авторов, а в том, что́ каждый из этих файлов обещает вызывающему. Ядро FTS обязано быть тотальным, потому что через него отвечает факт-чекер. Компилятор такого обещания не давал и имеет право упереться в лимит шагов — так прямо и записано в flang/self/SPEC.md. Поэтому там, где доказательство убывания стоило бы дороже пользы, пометка не ставится, а причина уходит в список долгов.

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

Вывод из таблицы стоит сформулировать явно, потому что он не тот, которого ждёшь. Тотальность здесь — не оценка кода, а тип обязательства. Читая чужой файл на flang, полезнее спросить не «почему тут мало тотального», а «что эта программа обещает тому, кто её вызывает».

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

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

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

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

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