Подстановка без копирования и вставки

Основная информация

• ID статьи: 2510.12304
• Название: Substitution Without Copy and Paste
• Авторы: Thorsten Altenkirch (University of Nottingham), Nathaniel Burke (Imperial College London), Philip Wadler (University of Edinburgh and Input Output)
• Классификация: cs.LO (Логика в информатике)
• Конференция: LFMTP 2025 (International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice)
• Ссылка на статью: https://arxiv.org/abs/2510.12304

Аннотация

При определении операции подстановки для языков с связывающими операторами (таких как просто типизированное λ-исчисление) традиционно требуется отдельное определение операций подстановки и переименования, что приводит к значительному дублированию кода. Для верификации категориальных свойств исчисления необходимо многократно повторять одни и те же аргументы. В данной работе предложен легковесный подход для избежания такого дублирования и построена просто типизированная CwF, изоморфная семейству начальных просто типизированных категорий с семействами (CwF). Статья представлена в виде литературного программного скрипта на языке Agda.

Исследовательский контекст и мотивация

Основная проблема

При механизированной верификации определения операции подстановки для языков со связывающими операторами традиционный подход требует:

1. Раздельного определения переименования переменных (∆ ⊩v Γ) и подстановки термов (∆ ⊩ Γ)
2. Повторной реализации четырёх различных операций подстановки: переменная на переменную, переменная на терм, терм на переменную, терм на терм
3. Повторной верификации всех комбинаций функториальных законов, что приводит к 8 различным случаям доказательства

Исследовательская мотивация

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

Ограничения существующих подходов

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

Основные вклады

1. Унифицированная структура: предложена единая операция подстановки на основе параметризации Sort, объединяющая обработку переменных и термов в одно определение
2. Гарантия завершаемости: умелое использование структурной рекурсии Agda и проверки завершаемости по лексикографическому порядку обеспечивает корректность определения
3. Категориальная верификация: доказано, что рекурсивно определённая подстановка удовлетворяет всем законам просто типизированной CwF
4. Результат начальности: установлено изоморфное соответствие между рекурсивно определённым синтаксисом подстановки и начальной CwF
5. Теорема нормализации: стандартная форма подстановки λ-термов соответствует λ-термам без явной подстановки

Методологическое описание

Постановка задачи

Построение унифицированной системы подстановки, такой что:

• Входные данные: произвольная комбинация термов/переменных и подстановок/переименований
• Выходные данные: соответствующий результат подстановки
• Ограничения: сохранение типобезопасности и завершаемости

Основная техника: система Sort

Определение типа Sort

data Sort : Set where
  V : Sort
  T>V : (s : Sort) → IsV s → Sort

data IsV : Sort → Set where
  isV : IsV V

pattern T = T>V V isV

Это определение умело делает V структурно меньше T, удовлетворяя требованиям проверки завершаемости Agda.

Унифицированное определение термов и подстановок

data _ ⊢ [_]_ : Con → Sort → Ty → Set where
  zero : Γ ▷ A ⊢ [ V ] A
  suc : Γ ⊢ [ V ] A → (B : Ty) → Γ ▷ B ⊢ [ V ] A
  `_ : Γ ⊢ [ V ] A → Γ ⊢ [ T ] A
  _ ·_ : Γ ⊢ [ T ] A ⇒ B → Γ ⊢ [ T ] A → Γ ⊢ [ T ] B
  λ_ : Γ ▷ A ⊢ [ T ] B → Γ ⊢ [ T ] A ⇒ B

где Γ ⊢ [ V ] A соответствует переменным, а Γ ⊢ [ T ] A соответствует термам.

Решёточная структура на Sort

data _ ⊑ _ : Sort → Sort → Set where
  rfl : s ⊑ s
  v⊑t : V ⊑ T

_⊔_ : Sort → Sort → Sort
V ⊔ r = r
T ⊔ r = T

Унифицированная операция подстановки

Основная функция подстановки

_[_] : Γ ⊢ [ q ] A → ∆ ⊩ [ r ] Γ → ∆ ⊢ [ q ⊔ r ] A

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

Обработка завершаемости

Разрешение проблемы завершаемости через полиморфную по Sort функцию тождества:

id-poly : Γ ⊩ [ q ] Γ
id : Γ ⊩ [ V ] Γ
id = id-poly {q = V}

Технические инновации

1. Структурированная рекурсия: использование структурного порядка Sort и лексикографической меры для обеспечения завершаемости
2. Параметрический полиморфизм: унификация различных случаев переменных и термов через параметризацию Sort
3. Применение теории решёток: элегантная обработка повышения типов с использованием операции ⊔
4. Правила переписывания: использование функциональности REWRITE в Agda для упрощения рассуждений о равенстве

Теоретическая верификация

Доказательство категориальных законов

Закон единицы

[id] : x [ id ] ≡ x

Доказывается структурной индукцией; ключевым является лемма о естественности для случая переменных.

Закон ассоциативности

[◦] : x [ xs ◦ ys ] ≡ x [ xs ] [ ys ]

Требует взаимной рекурсии с левым законом единицы, отражая внутреннюю связь категориальной структуры.

Верификация структуры CwF

Статья доказывает, что рекурсивно определённая подстановка удовлетворяет всем аксиомам просто типизированной CwF:

• Категориальная структура: контексты и подстановки образуют категорию
• Предпучковая структура: каждый тип соответствует предпучку
• Терминальный объект: пустой контекст
• Расширение контекста: структура, аналогичная произведению в категории

Теорема начальности

Установлены отображения в обе стороны:

1. Нормализация norm : Γ ⊢I A → Γ ⊢ [ T ] A
2. Вложение ⌜_⌝ : Γ ⊢ [ q ] A → Γ ⊢I A

и доказано, что они являются взаимными обратными:

• Стабильность norm ⌜ t ⌝ ≡ t
• Полнота ⌜ norm t ⌝ ≡ t

Детали реализации

Использование особенностей Agda

1. Индуктивно-индуктивные типы: взаимное определение Sort и IsV
2. Завершаемость по лексикографическому порядку: поддержка сложных рекурсивных паттернов
3. Правила переписывания: автоматизация рассуждений о равенстве
4. Синонимы паттернов: упрощение использования сложных типов

Анализ завершаемости

Завершаемость доказана анализом графа вызовов; мера для каждой функции:

• _[_]: (r, t)
• id: (r, Γ)
• _+_: (r, σ)
• suc[_]: (q)

Во всех циклах либо Sort строго уменьшается, либо Sort сохраняется при уменьшении других параметров.

Сравнение с существующими работами

Различия с существующими подходами

1. Метод Kit18,5: абстрагирует общие паттерны переименования и подстановки через kit, но всё ещё требует повторной верификации
2. Монадический взгляд6,9: кодирует подстановку как функцию из переменных в термы, но сложно расширяется на зависимые типы
3. Инструменты автоматизации21,22: библиотека Autosubst автоматически генерирует леммы о подстановке, но базовый уровень всё ещё содержит дублирование

Анализ преимуществ

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

Заключение и обсуждение

Основные выводы

1. Методологический вклад: доказано, что параметризация Sort позволяет элегантно унифицировать операции подстановки
2. Теоретический вклад: установлена начальность рекурсивно определённого синтаксиса подстановки
3. Практический вклад: предоставлено конкретное техническое решение для избежания дублирования

Ограничения

1. Зависимость от особенностей Agda: требует поддержки проверки завершаемости по лексикографическому порядку
2. Перенос сложности: хотя дублирование избегается, сложность переносится в систему Sort
3. Вызовы расширения: расширение на зависимые типы требует дальнейших исследований

Направления будущих работ

1. Расширение на зависимые типы: применение метода к полной теории зависимых типов
2. Высшая согласованность: применение в высших категориях
3. Перенос на другие системы доказательств: адаптация для Lean, Coq и других систем

Глубокая оценка

Достоинства

1. Техническая инновативность: дизайн системы Sort умело решает проблемы завершаемости и унификации
2. Теоретическая полнота: полное теоретическое развитие от базовых определений к начальности
3. Практическая ценность: предоставляет практическое решение для распространённых проблем в формальной верификации
4. Ясность изложения: как литературный программный скрипт хорошо сочетает код и объяснения

Недостатки

1. Зависимость от платформы: серьёзная зависимость от специфических особенностей Agda ограничивает переносимость
2. Компромисс в сложности: хотя дублирование избегается, вводится новая концептуальная сложность
3. Неизвестная расширяемость: расширение на более сложные системы типов требует дальнейшей верификации

Влияние

1. Теоретический вклад: предоставляет новый подход к механизированной верификации теории типов
2. Практическое руководство: предоставляет полезный инструмент для практиков формальной верификации
3. Исследовательское вдохновение: закладывает основу для дальнейших исследований теории зависимых типов

Области применения

1. Формальная верификация: определение языков, требующих обработки связывающих операторов
2. Исследование теории типов: исследование CwF и начальных алгебр
3. Теория языков программирования: механизированная верификация λ-исчисления и его расширений

Библиография

Статья ссылается на важные работы в данной области, включая:

• Оригинальные работы De Bruijn12
• Метод kit McBride18
• Типобезопасный подход Allais и соавторов5
• Серию работ Autosubst21,22
• Исследования относительных монад6

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