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