Формальная верификация алгоритма унификации рациональных термов

Формальная верификация алгоритма унификации рациональных термов

Доморацкий Э.А. (СПбГУ, Санкт-Петербург, Россия)
Булычев Д.Ю. (СПбГУ, Санкт-Петербург, Россия)

Аннотация

Мы представляем алгоритм унификации рациональных термов первого порядка, формально верифицированный в системе автоматической проверки доказательств Rocq. Алгоритм основан на подходе Мартелли и Росси, но переформулирован для удобства практической реализации. В работе описаны основные понятия, связанные с рациональными термами, системами уравнений как промежуточным состоянием работы алгоритма, и сам алгоритм, а также доказательства их основных свойств. Все утверждения из текста формально верифицированы в Rocq без использования дополнительных аксиом. Для определения отношения наибольшей бисимуляции на коиндуктивных типах в Rocq используется подход, основанный на индукции, позволяющий избежать проблем с проверкой продуктивности. Из реализации алгоритма в Rocq автоматически получена программа на Haskell. Это первая работа, предлагающая формально верифицированную спецификацию для алгоритма унификации рациональных термов.

Ключевые слова

рациональные термы; унификация; коиндукция; бисимуляция.

Издание

Труды Института системного программирования РАН, том 38, вып. 6, часть 1, 2026, стр. 23-40.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2026-38(6)-2

Для цитирования

Доморацкий Э.А., Булычев Д.Ю. Формальная верификация алгоритма унификации рациональных термов. Труды Института системного программирования РАН, том 38, вып. 6, часть 1, 2026, стр. 23-40. DOI: 10.15514/ISPRAS-2026-38(6)-2.

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома