RFC-027a: Явные меры для проверки завершаемости

Резюме

RFC-027 §7 устанавливает критерий проверки завершаемости как уточняющий тип (уточнение переходит в верификационный режим), §6.9 задаёт языковую форму явных мер (встроенный предикат Terminates, относящийся к тем же базовым примитивам, что Int и Never). Оба пункта — вопросы дизайна языка, относящиеся к базовому RFC, и уже утверждены.

Данный под-RFC определяет механизмы реализации: откуда берутся обязательства из вычислительной структуры, как упорядочивается конвейер верификации, как диагностика даёт направление, когда доказать не удаётся, как разделяются меры при взаимной рекурсии (оптимизация SCC), как регистрируются коды ошибок. Языковая семантика не дублируется, определяются только механизмы.

Мотивация

Зачем нужен под-RFC

Критерий (уточняющий тип переходит в верификационный режим) и форма (Terminates записывается в позиции типа) уже утверждены в RFC-027 на уровне языка. Остающиеся вопросы слишком детальны, и включение их в базовый RFC раздуло бы основной текст:

• Откуда берутся обязательства (точки рекурсивных вызовов, обратные рёбра циклов, охранные условия путей)
• Как сравнивать, когда мера возвращает кортеж (лексикографическая развёртка)
• Являются ли обоснованность (well-foundedness) и строгое убывание двумя независимыми обязательствами или одним
• Как автоматический поиск и явные меры сосуществуют в одном конвейере
• Как избежать дублирования записи и верификации одной и той же меры при взаимной рекурсии
• Как дать направление, а не просто отказать, когда доказать не удаётся

Триггер

Направление инициировано задачей #318: неструктурная рекурсия (непрямое убывание в стиле gcd, взаимная рекурсия, сортировка слиянием) выходит за пределы шаблонных последовательностей поиска мер (четыре стратегии RFC-027 §6.2–6.5 принимают на вход «переменную ограниченного типа» или «целевой тип + операцию перестановки»), и невозможно переписать её в анализируемый итеративный шаблон без потери читаемости. Здесь активируется пункт повторного обсуждения из раздела «Открытые вопросы» RFC-027.

Предложение

Отношение к автоматическому поиску

Явная мера — не отдельный конвейер, а входные данные для него после неудачи поиска. После указания меры используется тот же SMT для проверки того же набора обязательств; при недоказуемости выдаётся ошибка с контрпримером. Приоритет полной автоматизации сохраняется: поиск всегда запускается первым, вмешательство пользователя происходит только после неудачи поиска.

Это означает, что оба пути разделяют весь нижестоящий механизм — генерация обязательств, SMT-верификация, лексикографическая развёртка, формат диагностики реализованы единожды.

Генерация обязательств

Для функции f и меры m генерируются два независимых обязательства, раскрываемых по каждой точке рекурсивного вызова (включая межфункциональные вызовы внутри SCC):

1. Обоснованность (well-foundedness): m(args) >= 0 — мера попадает в натуральные числа; если мера возвращает ненатуральный тип, берётся нижняя граница подходящего порядка на этом типе. Выводится из уточнений параметров; при невозможности вывода переходит в остаточное обязательство.
2. Строгое убывание: в каждой точке вызова m(callee_args) < m(caller_args), проверяется при охранных условиях пути — они берутся из условий ветвления в точке вызова, повторно используя сбор путевых условий из RFC-009a.

Эти два обязательства независимы, а не объединены, поскольку направления отказа различаются: неудача обоснованности указывает на неверную область значений меры (например, Int может быть отрицательным), неудача убывания — что рекурсивный аргумент не движется в ожидаемом направлении. Диагностика должна их различать, чтобы дать корректное направление проверки (см. раздел «Диагностика»).

Для циклов — аналогично, «точка вызова» заменяется на «обратное ребро»: на каждом пути исполнения тела цикла m(состояние_след_итерации) < m(состояние_текущей_итерации), охранные условия берутся из условия цикла и ветвлений внутри тела.

Лексикографическая развёртка: когда m возвращает кортеж (m₁, …, mₖ), обязательство разворачивается в дизъюнктивную цепочку по лексикографическому порядку — (m₁' < m₁) ∨ (m₁' == m₁ ∧ m₂' < m₂) ∨ …. Развёртка выполняется на стороне генерации обязательств, на стороне SMT сохраняется линейный фрагмент без зависимости от нативной поддержки лексикографического порядка в решателе.

Сама мера должна быть вычислимой в момент компиляции: m должна быть функцией, доказуемой через постоянное свёртывание или структурную рекурсию — запрещено рекурсивно перекладывать задачу завершаемости на другую недоказанную функцию (защита от бесконечной регрессии). Патологические меры отсекаются существующими E4012 (слишком глубокая константная рекурсия) и структурными проверками.

Конвейер верификации

1. Структурная рекурсия (убывание по формальным параметрам, самый сильный путь, пробуется первым)
2. Поиск меры: последовательность шаблонов четырёх стратегий (RFC-027 §6.2–6.5), останавливается на первом успехе
3. Поиск успешен → генерация обязательств → SMT-верификация → Proved
4. Поиск неуспешен → проверка наличия явной меры в позиции типа (Terminates)
     Есть → взять эту меру, сгенерировать обязательства → SMT-верификация
     Нет → E4021 (завершаемость не доказуема, с предложенным направлением проверки)
5. Обязательство опровергнуто SMT → E4022 (мера не выполняется, с контрпримером)

Уровни 1–3 — существующий путь RFC-027, данный RFC добавляет уровень 4 и два кода ошибок. Весь конвейер запускается только при срабатывании уточняющих типов (RFC-027 §7) — обычные типы без уточнений не генерируют никаких обязательств.

Точка привязки: унарная и бинарная формы

RFC-027 §6.9 определяет две арности, данный RFC уточняет их точки привязки:

Форма	Точка привязки	Назначение
Terminates(m)	Имя привязки	Форма по умолчанию в определении — саморекурсивные функции, циклы
Terminates(FnType, m)	Явный функциональный тип	Когда нужно явно указать, к какому функциональному типу относится мера (мера определена в другом месте, обслуживает несколько вычислений)

Это не две разные конструкции, а две арности одного предиката: обязательство завершаемости всегда привязывается к «тому вычислению, которое аннотировано в позиции типа, где находится уточнение». Для взаимной рекурсии не требуется бинарная форма — обе функции могут иметь свою унарную форму, а их связь распознаётся через SCC (см. следующий раздел).

SCC: оптимизация разделения меры

Если группа функций в взаимной рекурсии (сильно связная компонента на графе вызовов) разделяет одну меру, обязательство на межфункциональном ребре принимает вид m_callee(callee_args) < m_caller(caller_args), сводясь к убыванию по той же мере при совместном использовании.

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

Требуется создать граф вызовов на уровне функций и сбор SCC — текущий TypeDepGraph фиксирует зависимости аннотаций типов между переменными (триггер VC из RFC-027 §6.1), это граф на уровне переменных, его использовать нельзя.

Примеры

gcd: неструктурная рекурсия

// Мера: обычная функция, тестируемая и переиспользуемая
gcd_measure: (a: Int, b: Int) -> Int = { b }

gcd: Terminates((a: Int, b: Int) -> Int, gcd_measure) = {
    if b == 0 { return a }
    return gcd(b, a % b)
}

Генерация обязательств:

1. Обоснованность: gcd_measure(a, b) >= 0, т.е. b >= 0 — выводится напрямую из уточнения формального параметра NonNegative(b)
2. Строгое убывание: единственная точка рекурсивного вызова gcd(b, a % b), охранное условие пути b != 0, обязательство gcd_measure(b, a % b) < gcd_measure(a, b); подстановка тела меры даёт a % b < b
3. SMT: проверить, что отрицание b != 0 ∧ a % b >= b невыполнимо → Proved

Цикл: получение денотата через анонимную конструкцию

loop: (n: Int) -> Int = {
    mut i = 0
    acc: Terminates(n - i) = while i < n {
        i = i + 1
    }
    return acc
}

Уточнение Terminates(m) применяется к типу значения хвостового выражения тела цикла, точка привязки задаётся именем привязки acc — таким образом, цикл получает денотат, устраняя «мёртвую зону» анонимных конструкций. Это также объясняет единство двух арностей: обязательство всегда лежит на том вычислении, которое аннотировано в позиции типа, где находится уточнение, функции и циклы не различаются.

Обязательство: на обратном ребре (n - i') < (n - i), охранное условие i < n, подстановка i' = i + 1 даёт 1 > 0, что тавтологически истинно → Proved.

Взаимная рекурсия: разделение меры через SCC

nat: (n: Int) -> Int = { n }

is_even: Terminates(nat) = {
    if n == 0 { return true }
    return is_odd(n - 1)
}
is_odd: Terminates(nat) = {
    if n == 0 { return false }
    return is_even(n - 1)
}

Обе функции несут унарную форму Terminates(nat). После сбора SCC распознаётся, что они разделяют одну меру, обязательство на межфункциональном ребре nat(n - 1) < nat(n) тавтологически выполняется при охранном условии n != 0, обе функции верифицируются за один проход.

Без распознавания SCC каждая функция по-прежнему проходит верификацию того же обязательства — просто повторно. Это подтверждает позиционирование SCC как оптимизации.

Диагностика

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

Неудача	Направление предложения
Обоснованность не выводится	Проверить, выполняется ли нижняя граница на возможных значениях (например, нужна ли >= 0 для меры типа Int)
Строгое убывание опровергнуто	Действительно ли рекурсивный аргумент движется в направлении убывания меры; с контрпримером от SMT
Нет меры, поиск неуспешен	Указать, что вычислению можно присвоить имя и указать меру в позиции типа (RFC-027 §6.9)

Представление контрпримеров соответствует спецификации диагностических сообщений RFC-013. При нелинейных охранных условиях пути Sat-контрпримеры могут быть неинтуитивными — это зафиксировано как известное ограничение, итерируемое вместе с RFC-013.

Коды ошибок

Выровнено по семейству ошибок верификации E4xxx (E4018 нарушение уточняющего предиката, E4020 требуется доказывающая функция):

Предлагаемый код	Имя	Триггер
E4021	Завершаемость не доказуема	Поиск неуспешен и в позиции типа нет явной меры (с подсказкой указать меру через Terminates)
E4022	Мера не выполняется	Обязательство меры опровергнуто SMT (с контрпримером)

Финальная нумерация определяется реальным состоянием реестра RFC-013 на момент реализации (корректность сегмента гарантируется порогом build.rs).

Существующий дефект диагностического слоя

В текущей реализации ошибки завершаемости в пределах области видимости выдаются как E8001 «внутренняя ошибка компилятора» (Unproven форматируется как ICE) — проверка завершаемости не является ICE, занятие этого кодового слота одновременно вводит пользователя в заблуждение и маскирует реальные сбои. Данный RFC исправляет это: ошибки завершаемости в пределах области видимости идут по E4021/E4022, кодовый слот ICE возвращается для подлинных внутренних ошибок.

Изменения в компиляторе

Компонент	Изменение
typecheck/layers/termination.rs	Унификация интерфейса (общие генерация обязательств и верификация для путей поиска и явной меры); подключение Z3 (инъекция в производственный конвейер, в настоящее время with_z3 существует только в юнит-тестах)
Граф вызовов функций + SCC (новый)	В репозитории нет межфункционального графа вызовов — TypeDepGraph отражает зависимости типов на уровне переменных, его использовать нельзя. Создаются граф вызовов на уровне функций и сбор SCC для разделения мер при взаимной рекурсии
Генерация обязательств	Добавляется: два обязательства (обоснованность / строгое убывание), инъекция охранных условий пути, лексикографическая развёртка
Конвейер верификации (RFC-009a / #292)	Повторное использование цепочки ConstExpr → SMTLib и отображения операторов вроде Mod, без изменений в бэкенде
util/diagnostic/codes/e4xxx.rs	Регистрация E4021/E4022 (через реестр RFC-013, порог build.rs)
locales ×6	Шаблоны для двух новых кодов на шести языках
Диагностический слой	Ошибки завершаемости в пределах области видимости переносятся с E8001 в семейство ошибок верификации

Обратная совместимость

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

Компромиссы

Преимущества

• Нулевая новая синтаксика: мера записывается в позиции типа, повторно используя механизм применения уточняющих предикатов; нет позиций синтаксиса вроде decreases.
• Согласованность поведения доменов верификации: домен завершаемости получает тот же обходной канал, что и домен корректности, но с иной точкой приложения — недоказуемые утверждения в домене корректности записываются как доказывающие функции в теле, неподдающиеся поиску меры в домене завершаемости объявляются в позиции типа. Оба используют один механизм (применение уточняющего типа).
• Повторное использование инфраструктуры: обязательства представляют собой линейную арифметику с охранными условиями пути, проходя по подключённому конвейеру #292, без нового бэкенда.
• Циклы получают денотат: имя привязки служит точкой привязки, циклы и функции полностью изоморфны в генерации обязательств, специальных случаев для циклов проектировать не нужно.

Недостатки и риски

• Объём предварительной инфраструктуры не меньше «подключения»: граф вызовов на уровне функций и сбор SCC требуют создания, Z3 также не подключён к производственному конвейеру. Часть SCC можно отложить (это оптимизация), часть с графом вызовов имеет тот же источник; при отсрочке взаимная рекурсия сможет использовать только раздельные меры — всё равно проходит, но с дублированием верификации.
• Явная мера —书写负担 (бремя записи) на редком пути: пара (функция-мера + объявление в позиции типа) многословнее встроенной аннотации. Принимается — обходной путь используется редко, и换来 возможность повторного использования и юнит-тестирования меры.
• Шум обязательства обоснованности: при типе возврата Int необходимо каждый раз доказывать >= 0. Смягчение: если уточнение параметра уже задаёт нижнюю границу, вывод выполняется автоматически; только при невозможности вывода обязательство становится остаточным, и даже тогда выдаётся только направление, без отказа.
• Качество контрпримеров: Sat-контрпримеры при нелинейных охранных условиях неинтуитивны. Известное ограничение.
• Terminates — единственный предикат, тело которого генерируется компилятором: отступление от чистоты «все тела предикатов могут быть написаны пользователем». Обоснование: его утверждения (убывание меры в каждой точке вызова / обратном ребре) заключены в вычислительной структуре, к которой пользовательский предикат обратиться не может. Встроенная поверхность сводится к одному имени, механизмов без新增 (新增) ноль.

Альтернативы

• Встроенный синтаксис аннотации with decreases (b): раннее предложение в этом issue, отозвано. «Проверка завершаемости не оставляет лазейки в виде синтаксиса аннотаций» — утверждённое решение RFC-027; встроенная аннотация превратила бы неподдерживаемые режимы завершаемости в позиции синтаксиса, а не типа, что противоречит мировоззрению «всё есть функция YaoXiang, всё верифицируется проверкой типов».
• Отдельная доказывающая функция (gcd_proof возвращает Terminates(f, m), обнаруживается сканированием возвращаемого типа): ранний дизайн. Отменено — это вводит четыре класса сложности: «механизм обнаружения», «соглашение об именовании», «выбор первого из нескольких кандидатов», «как разрешаются имена в теле доказывающей функции» — и все они возникают из-за вынесения доказательства наружу. После переноса в позицию типа все четыре класса исчезают.
• Только Terminates(m), отказ от бинарной формы: короче, но теряется позиция для «явного указания принадлежности меры» (когда мера определена в другом месте, обслуживает несколько вычислений). Две арности — это две арности одного предиката, стоимость сохранения практически нулевая.
• Никакого обходного пути, требовать от пользователя переписать в анализируемый итеративный шаблон: текущее положение дел. gcd / сортировка слиянием / взаимная рекурсия не могут быть переписаны без потери читаемости — именно это и является триггером пункта повторного обсуждения.

Вне области задач

• Не新增 синтаксис / ключевые слова / позиции аннотаций.
• Не выполняется обобщённое расширение автоматического синтеза мер (четыре стратегии остаются в рамках утверждённого плана RFC-027, за пределами射程 — путь явных мер). Универсальный вывод мер находится на неразрешимой стороне «обнаружения», можно лишь约定 (оговорить) границы шаблонов, но не обещать полноты.
• Не объединяется с RFC-009a для совместного решения пропозиций (каждое верифицируется независимо, общий бэкенд).
• Не выполняется верификация полноты (totality checking) на уровне зависимых типов.
• Мера не обязана возвращать натуральный тип (без стремления к механизму классов типов WellFoundedRelation из Lean) — тип возврата меры не ограничивается, обоснованность передаётся как независимое обязательство выводу уточнений или SMT.

Этапы и приёмка

• [ ] Генерация обязательств (обоснованность / строгое убывание, инъекция охранных условий пути, лексикографическая развёртка)
• [ ] Подключение явных мер (разбор точек привязки унарной и бинарной форм Terminates, извлечение меры из позиции типа)
• [ ] Подключение SMT-верификации (повторное использование конвейера #292, инъекция Z3 в производственный конвейер)
• [ ] Граф вызовов на уровне функций + сбор SCC (оптимизация разделения мер)
• [ ] Регистрация E4021/E4022 + locales для шести языков
• [ ] Исправление диагностического слоя: ошибки завершаемости в пределах области видимости переносятся с E8001 в семейство ошибок верификации
• [ ] E2E: положительные примеры (gcd / цикл Terminates(n - i) / взаимная рекурсия is_even-is_odd) / отрицательные (мера не выполняется → E4022; нет меры → E4021) / нулевая регрессия структурной рекурсии
• [ ] Регрессия критерия: рекурсия и циклы без уточняющих аннотаций более не отвергаются проверкой завершаемости; при наличии уточняющих аннотаций обязательства触发ются как обычно
• [ ] Демонстрация приёмки: написать объявление с невыполнимой мерой → ошибка компиляции с читаемым контрпримером; исправить → успех

Связанные документы

• #318 (issue, инициировавшее данный RFC), #251 (родительский этап P1)
• RFC-027 (базовый: §7 критерий уточняющих типов, §6.1–6.5 четыре стратегии поиска мер, §6.9 явные меры, раздел «Открытые вопросы» — пункт повторного обсуждения)
• RFC-009a / #292 (общий SMT-конвейер и сбор путевых условий — предпосылка инфраструктуры)
• RFC-013 (реестр кодов ошибок и семантическое семейство ошибок верификации)