Введение 3
Постановка задачи 5
1. Обзор литературы 6
2. Основные понятия 7
3. Полиномиальные теории 10
3.1. Синтаксическая эквивалентность 10
3.2. Теория U 11
3.3. Теория I 13
3.4. Теория A 14
3.5. Теория AIU 16
3.6. Теория ADU 18
4. NP Теории 25
4.1. Теория C 25
4.2. Теория ACUI 32
5. Полиномиальное сравнение типов нормальных форм 42
Заключение 44
Список литературы 45
Задача вывода типов актуальна для языков программирования с неявной типизацией, где типы в большинстве случаев выводятся самим компилятором, чтобы пользователю не приходилось явно указывать тип каждой
переменной или выражения. Помимо этого вывод типов является основой
для систем интерактивных доказательств, таких как Сoq [18] или Agda [19].
При выводе типов часто требуется выбирать новые имена переменных,
обозначающие типовые атомы. При этом новое имя может либо возникнуть
при работе самого алгоритма типизации, либо изначально быть задано пользователем, например это может быть имя шаблонного типа класса. Но в любом случае, конкретно выбранное имя не имеет значения, при условии, что
оно уникально определяет типовой атом, поэтому имя может выбираться
произвольным образом. Впоследствии, например при соотнесении двух выражений, может потребоваться сравнить два типа между собой. При этом
сравнение должно быть по модулю выбранных имен переменных. Иными словами, возникает задача поиска переименования переменных внутри одного
типа в переменные другого, так чтобы типы стали эквивалентны. Отметим,
что изначально до применения переименования, сами типы не являются эквивалентными. Они становятся эквивалентными уже после того, как к одному
из этих типов применяется переименование.
Данная задача сравнения типов с переименованием имеет простой линейный алгоритм, когда речь идет о синтаксической эквивалентности. Однако,
если начать сравнивать типы не только по модулю переименования переменных, но и по модулю некоторой системы аксиом для равенства двух типов,
которую в дальнейшем будем называть теорией эквивалентности, то задача
становится NP-полной уже при простых теориях эквивалентности.
Эта задача является частным случаем задачи сопоставления (matching)
типов, в которой S может быть не только переименованием, но и подстановкой. То есть разрешается не просто давать переменным другие имена, но
еще и подставлять вместо любой переменной произвольный тип. Такая задача
подробно рассматривается в статье Benanav, Kapur, Narendran [1], где авторы доказывают ее NP полноту для ассоциативных и коммутативных теорий
3эквивалентности. Задача сопоставления, в свою очередь, является частным
случаем задачи унификации типов, где подстановка применяется не только к
типу слева, но и к типу справа.
Выведены классы сложности для задачи сравнения типов пересечений с
переименованием. Доказана NP полнота данной задачи для теории C и C2.
Был адаптирован эффективный NP алгоритм для теории ACUI. Стоит
отметить, что этот алгоритм легко расширить и на другие NP-полные
теории. Например, на ACUID. Достаточно просто добавить приведение
типов к нормальное форме для дистрибутивности nfD.
Также было подробно рассмотрено несколько улучшений, которые можно
применить для ускорения данного алгоритма. И наконец, были произведены
замеры времени работы на случайно сгенерированных типах для наивного
алгоритма, алгоритма 5, а также его улучшений.
В качестве бонуса, был описан способ полиномиального сравнения типов
пересечений нормальных форм в теории ACU.
Все реализованные NP алгоритмы для теории ACUI доступны на
гитхаб.
