📄Работа №149223
Тема: Эффективная проверка эквивалентности типов-пересечений
Тип работы
Бакалаврская работа
Предмет
информатика
Объем:
46 листов
Год:
2024
Просмотров:
53
4750
руб.
🛒 Купить работу
Не подходит эта работа?
Закажите новую по вашим требованиям
Узнать цену на написание
Закажите новую по вашим требованиям
Представленный материал является образцом учебного исследования, примером структуры и содержания учебного исследования по заявленной теме. Размещён исключительно в информационных и ознакомительных целях.
Workspay.ru оказывает информационные услуги по сбору, обработке и структурированию материалов в соответствии с требованиями заказчика.
Размещение материала не означает публикацию произведения впервые и не предполагает передачу исключительных авторских прав третьим лицам.
Материал не предназначен для дословной сдачи в образовательные организации и требует самостоятельной переработки с соблюдением законодательства Российской Федерации об авторском праве и принципов академической добросовестности.
Авторские права на исходные материалы принадлежат их законным правообладателям. В случае возникновения вопросов, связанных с размещённым материалом, просим направить обращение через форму обратной связи.
Настоящий учебно-методический информационный материал размещён в ознакомительных и исследовательских целях и представляет собой пример учебного исследования. Не является готовым научным трудом и требует самостоятельной переработки.
📋 Содержание
Введение 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
Постановка задачи 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эквивалентности. Задача сопоставления, в свою очередь, является частным
случаем задачи унификации типов, где подстановка применяется не только к
типу слева, но и к типу справа.
переменной или выражения. Помимо этого вывод типов является основой
для систем интерактивных доказательств, таких как С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 доступны на
гитхаб.
переименованием. Доказана NP полнота данной задачи для теории C и C2.
Был адаптирован эффективный NP алгоритм для теории ACUI. Стоит
отметить, что этот алгоритм легко расширить и на другие NP-полные
теории. Например, на ACUID. Достаточно просто добавить приведение
типов к нормальное форме для дистрибутивности nfD.
Также было подробно рассмотрено несколько улучшений, которые можно
применить для ускорения данного алгоритма. И наконец, были произведены
замеры времени работы на случайно сгенерированных типах для наивного
алгоритма, алгоритма 5, а также его улучшений.
В качестве бонуса, был описан способ полиномиального сравнения типов
пересечений нормальных форм в теории ACU.
Все реализованные NP алгоритмы для теории ACUI доступны на
гитхаб.
ИЛИ
Поиск аналога
📕 Список литературы
🛒 Оформить заказ
⚡ Работу высылаем в течении 5 минут после оплаты.