Объединение высшего порядка

Question

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

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

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

Answer 1

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

Обратите внимание, что алгоритм Хьюта является лучшим в следующем смысле & mdash; он похож на алгоритм полуопределения, в котором он найдет объединители, если они существуют, но он не гарантированно завершится, если они не будут. Так как мы знаем, что объединение высшего порядка (действительно, объединение второго порядка) неразрешимо, вы не можете добиться большего успеха, чем это.

Пояснения: первые четыре главы кандидатской диссертации Конала Эллиотта, Расширения и применения объединения высшего порядка должны соответствовать требованиям. Эта часть весит почти 80 страниц, с некоторой плотной теорией типов, но она хорошо мотивирована и является самой читаемой учетной записью, которую я когда-либо видел.

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

Answer 2

Пример объединения более высокого порядка (на самом деле сопоставление второго порядка): f 3 == 3 + 3, где == - по модулю альфа, бета и эта-конверсия (но без присвоения какого-либо значения "+"). Есть четыре решения:

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

Напротив, объединение / сопоставление первого порядка не дало бы решения.

HOU очень удобен при использовании с HOAS (абстрактный синтаксис высшего порядка) для кодирования языков с привязкой переменных, избегая при этом сложности захвата переменных и т. Д.

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

Answer 3

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

Препринт находится здесь:

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

Работа Конала Эллиота более формальна и согласована в одном варианте, а также вводит λΠΣ-исчисление в конце, которое также имеет суммы типов помимо видов продукции.

Bye

Answer 4

Существует также статья Тобиаса Нипкова 1993 года Функциональная унификация паттернов высшего порядка (только 11 страниц, 4 из которых - библиография и добавление кода). Автореферат:

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