Я работаю над доказательством теоремы более высокого порядка, единство которого представляется самой сложной подзадачей.
Если алгоритм Huet по-прежнему считается самым современным, есть ли у кого-нибудь ссылки на его объяснения, которые написаны для понимания программистом, а не математиком?
Или даже какие-либо примеры того, где он работает, и обычный алгоритм первого порядка не работает?
Современное состояние; да, насколько я знаю, все алгоритмы более или менее принимают ту же форму, что и Huet (я следую теории логического программирования, хотя мой опыт тангенциальный), если вам нужно полное соответствие более высокого порядка: такие подзадачи, как сопоставление высшего порядка (унификация где одно слагаемое закрыто) и исчисление шаблона Дейла Миллера разрешимы.
Обратите внимание, что алгоритм Huet является лучшим в следующем смысле:— это похоже на алгоритм полупринятого решения, поскольку он найдет унификаторы, если они существуют, но не гарантируется, что они прекратятся, если они этого не сделают. Поскольку мы знаем, что унификация высшего порядка (действительно, объединение второго порядка) неразрешима, вы не можете добиться большего успеха.
Пояснения: Первые четыре главы кандидатской диссертации Конала Эллиотта Расширения и приложения унификации высшего порядка должны соответствовать законопроекту. Эта часть весит почти 80 страниц, с некоторой плотной теорией типов, но ее хорошо мотивированная и самая читаемая учетная запись, которую я видел.
Примеры. В этом примере алгоритм Huet найдет товар: [X (o), Y (succ (0))]; который по необходимости будет озадачивать алгоритм унификации первого порядка.
Пример объединения высшего порядка (действительно совпадение второго порядка): f 3 == 3 + 3, где == - это модуляция альфа, бета и эта-преобразование (но не присвоение значения "+" ). Существует четыре решения:
\ x -> x + x
\ x -> x + 3
\ x -> 3 + x
\ x -> 3 + 3
Напротив, унификация/совпадение первого порядка не даст решения.
HOU очень удобен при использовании с HOAS (абстрактный синтаксис более высокого порядка), чтобы кодировать языки с привязкой к переменной, избегая при этом сложности захвата переменных и т.д.
Мое первое знакомство с этой темой - документ "Доказательство и применение программных преобразований, выраженных с помощью шаблонов второго порядка" Джерарда Уэта и Бернарда Ланга. Насколько я помню, этот документ был "написан для понимания программистом". И как только вы понимаете совпадение второго порядка, HOU не намного дальше идти. Ключевым результатом Huet является то, что гибкий/гибкий случай (переменные как глава термина и единственный случай, не встречающийся в совпадении) всегда разрешимы.
Я бы добавил в список чтения главу в томе 2 Справочник по автоматическому обоснованию. Эта глава, вероятно, более доступным для новичка и заканчивается λΠ-исчислением, где Бумага Коналла Эллиотта начинается.
Препринт находится здесь:
Унификация и соответствие высшего порядка
Жиль Довек, 2001
http://www.lsv.fr/~dowek/Publi/unification.ps
Бумага Коналла Эллиотта более формальна и относится к одному варианту, а также вводит λΠΣ-исчисление в конце, которое также имеет типы сумм кроме типов продуктов.
Bye
Существует также статья Тобиаса Нипкова 1993 Функциональная унификация шаблонов более высокого порядка (всего 11 страниц, 4 из которых являются библиографией и добавлением кода), Резюме:
Представлена полная разработка алгоритма унификации для так называемых шаблонов более высокого порядка, подкласса $\ lambda $-terms. Отправной точкой является формулировка унификации путем трансформации, результатом которой является непосредственно исполняемая функциональная программа. На конечном этапе разработки результат адаптируется к $\ lambda $-термам в обозначении Bruijn. Алгоритмы работают как для типизированных, так и для нетипизированных терминов.