Номинальные термины (информатика)

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

В то время как регулярная унификация, найденная в Прологе, линейна по размеру сравниваемых терминов, расширение для точного определения эквивалентности номинальных терминов, называемое номинальной унификацией в литературе основанный на более раннем алгоритме PTIME для номинальной унификации, , является квадратичным (Калвес 2013). AlphaProlog, представляет собой пролог -подобный язык логического программирования со средствами связывания имен в терминах, который был задуман как полезный для программ, действующих на основе синтаксиса программы (Чейни, 2004).

Номинальные вложения терминов можно рассматривать как альтернативу кодировкам де Брёйна и абстрактному синтаксису высшего порядка , где последний использует просто типизированное лямбда-исчисление в качестве метаязыка.

Мотивация

Многие интересные вычисления, логика и языки программирования , которые обычно встречаются в информатике, содержат конструкции привязки имен. Например, квантор универсальности из логики первого порядка , лямбда-связчик из лямбда-исчисления и пи-связчик из пи-исчисления — все это примеры конструкций, связывающих имена.

Ученым-компьютерщикам часто приходится манипулировать абстрактными синтаксическими деревьями . Например, авторы компиляторов выполняют множество манипуляций с абстрактными синтаксическими деревьями на различных этапах оптимизации и разработки выполнения компилятора. В частности, при работе с абстрактными синтаксическими деревьями с конструкциями привязки имен нам часто хочется поработать над классами альфа-эквивалентности, реализовать замены, избегающие захвата, и упростить генерацию новых имен. Вопрос о том, как лучше всего это сделать, не допуская ошибок и надежно, требует большого количества исследований.

Предыдущие попытки решения этой проблемы включали «безымянные подходы», такие как индексы и уровни де Брёйна, а также подходы более высокого порядка, такие как абстрактный синтаксис более высокого порядка. Номинальные термины - это еще один, относительно новый подход, который сохраняет явные имена для связанных переменных, таких как абстрактный синтаксис более высокого порядка, сохраняя при этом разновидность первого порядка (и вычислительные свойства первого порядка) кодировок де Брейна.

Связь с шаблонами более высокого порядка

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

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

В недавних работах исследовались связи между номинальными терминами и шаблонами более высокого порядка и, следовательно, между номинальной унификацией и унификацией шаблонов более высокого порядка. Чейни предложил расширение номинальных терминов, названное номинальными моделями. Затем он обеспечил перевод между номинальными шаблонами и шаблонами более высокого порядка, которые сохранили объединители . Позже Леви и Вилларе продемонстрировали перевод между номинальными терминами и шаблонами более высокого порядка, который сохраняет понятие унификации. То есть, если два номинальных термина унифицированы, то их переведенные аналоги-образцы также унифицированы.

Позже Доук и Габбай усовершенствовали перевод Леви и Вилларе, доказав, что в некотором смысле их перевод является лучшим из возможных, и доказали, что улучшенный перевод сохраняет унификаторы. То есть, если два номинальных термина можно объединить путем некоторой замены, то соответствующая проблема объединения шаблонов более высокого порядка при переводе решается путем переведенной замены. Для своего доказательства Доук и Габбай использовали разновидность номинальных терминов, называемую разрешительными номинальными терминами. Однако также существует перевод от разрешительных номинальных терминов и обратно, завершающий перевод между номинальными терминами и шаблонами более высокого порядка.

Ссылки

• Кристоф Кальвес и Марибель Фернандес (2008). «Алгоритм полиномиального номинального объединения» . Теоретическая информатика . 403 (2–3): 285–306. дои : 10.1016/j.tcs.2008.05.012 .
• Кристоф Кальвес (2013). «Объединяющее именное объединение» . Учеб. 4-я Международная конференция по методам и приложениям рерайтинга . стр. 143–157. дои : 10.4230/LIPIcs.RTA.2013.143 .
• Джеймс Чейни (2004). Номинальное логическое программирование (доктор философии). Корнелльский университет.
• Джеймс Чейни (2005). «Относительно унификации шаблонов высшего порядка и номинальной унификации». Материалы 19-го Международного семинара по унификации (UNIF) . стр. 104–119.
• Жиль Доук, Мердок Дж. Габбай и Доминик П. Маллиган (2010). «Разрешительные номинальные термины и их унификация». Логический журнал IGPL . 18 (6): 769–822. CiteSeerX   10.1.1.185.3105 . дои : 10.1093/jigpal/jzq006 .
• Хорги Леви и Матеу Вилларет (2008). «Номинальное объединение с точки зрения высшего порядка». Материалы 19-го Международного семинара по методам и приложениям переписывания (RTA) . стр. 246–260.
• Кристиан Урбан, Эндрю М. Питтс и Мердок Дж. Габбай (2004). «Номинальное объединение» . Теоретическая информатика . 323 (1–3): 473–497. дои : 10.1016/j.tcs.2004.06.016 .