Номинальные условия (информатика) - Википедия - Nominal terms (computer science)

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

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

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

Мотивация

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

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

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

Синтаксис

Примеры вложений

Алгоритм унификации

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

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

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

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

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