Объединение высшего порядка
Я работаю над программой автоматического доказательства теоремы высшего порядка, которой объединение, кажется, самая трудная подпроблема.
Если алгоритм Huet все еще считают современным, у кого-либо есть какие-либо ссылки на объяснения его, которые записаны, чтобы быть понятыми под программистом, а не математиком?
Или даже какие-либо примеры того, где это работает и обычный алгоритм первого порядка, не делают?
2 ответа
Современное состояние - да, насколько я знаю, все алгоритмы более или менее имеют ту же форму, что и алгоритмы Хуэ (я следую теории логического программирования, хотя мои знания касаются) при условии , что вам необходимо полное сопоставление более высокого порядка: подзадачи, такие как сопоставление более высокого порядка (объединение, где один член замыкается) и исчисление шаблонов Дейла Миллера, разрешимы.
Обратите внимание, что алгоритм Хьюэ является лучшим в следующем смысл - это похоже на алгоритм полурешения, в котором он найдет объединители, если они существуют, но не гарантированно завершится, если они не будут. Поскольку мы знаем, что объединение высшего порядка (действительно, объединение второго порядка) неразрешимо, вы не можете сделать лучше этого.
Пояснения: Первые четыре главы докторской диссертации Конала Эллиотта, Расширения и приложения унификации высшего порядка должны соответствовать всем требованиям. Эта часть весит почти 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 не так уж много осталось. Ключевым результатом работы Хуэта является то, что случай гибкий/негибкий (переменные как глава термина, и единственный случай, не появляющийся в согласовании) всегда разрешим.