Унификация более высокого порядка

Question

Я работаю над теоретикой высшего порядка, единство которой представляется сложнейшей подзадачей.

Если алгоритм Huet по-прежнему считается самым современным, имеет ли кто-либо ссылки на его объяснения, которые должны быть поняты программистом, а не математиком?

Или даже любые примеры того, где это работает и обычный алгоритм первого порядка, нет?

Answer 1

Современное состояние — да, насколько я знаю, все алгоритмы более или менее взять ту же форму, что и HUET в (я следую теории логического программирования, хотя мой опыт тангенциально) при условии вам нужно полный выше порядка Соответствие: подзадачи, такие как согласование более высокого порядка (объединение, когда одно слово закрыто) и исчисление шаблона Дейла Миллера, разрешимы.

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

Пояснения: Первые четыре главы докторской диссертации Конала Эллиота, Extensions and Applications of Higher-Order Unification должны соответствовать законопроекту. Эта часть весит почти 80 страниц, с некоторой плотной теорией типов, но ее хорошо мотивированная и самая читаемая учетная запись, которую я видел.

Примеры: В этом примере алгоритм Уэта придет с товаром: [X (o), Y (succ (0))]; которая по необходимости будет озадачивать алгоритм унификации первого порядка.

Answer 2

Пример объединения более высокого порядка (действительно соответствие второго порядка): f 3 == 3 + 3, где == - это modulo alpha, beta и eta-conversion (но не присвоение значения «+»). Существует четыре решения:

\ x -> x + x 
\ x -> x + 3 
\ x -> 3 + x 
\ x -> 3 + 3 

Напротив, унификация/согласование первого порядка не даст никакого решения.

ХУ очень удобно при использовании с ОСМД (абстрактный синтаксис более высокого порядка), для кодирования языков с переменной связывания, избегая при этом сложность захвата переменной и т.д.

Моя первая экспозиция на тему была статья «Доказывание и применение программных преобразований, выраженных с помощью шаблонов второго порядка "Джерардом Уэтом и Бернардом Лангом. Насколько я помню, этот документ был «написан для понимания программистом». И как только вы понимаете совпадение второго порядка, HOU не намного дальше идти. Ключевым результатом Huet's является то, что гибкий/гибкий случай (переменные как глава термина и единственный случай, не встречающийся в совпадении) всегда разрешима.

Answer 3

Я бы добавил к списку чтений главу в томе 2 из Справочник по автоматическому обоснованию. Эта глава, вероятно, , более доступная для новичка и заканчивается λΠ-исчислением, где начинается Бумага Коналла Эллиотта.

препринт можно найти здесь:

высшего порядка унификация и Matching
Жиль Dowek, 2001
http://www.lsv.fr/~dowek/Publi/unification.ps

Conal Elliott бумага носит более формальный характер и concerntrated на одном варианте, , а также вводит λΠΣ-исчисление в конце, которое также имеет типы сумм , кроме типов продуктов.

Bye

Answer 4

Существует также Tobias Нипкова в 1993 бумага Functional Unification of Higher-Order Patterns (всего 11 страниц, 4 из которых являются библиография и код приложения). Аннотация:

Полная разработка алгоритма унификации так называемых моделей высшего порядка, подкласс $ \ Lambda $ -терминов, представлена. Отправной точкой является формулировка унификации путем трансформации, результатом которой является непосредственно исполняемая функциональная программа. На заключительном этапе разработки результат адаптируется к $ \ lambda $ -термам в обозначениях Брейна. Алгоритмы работают как для типизированных, так и для нетипизированных терминов.