Абстрактный синтаксис высшего порядка - Higher-order abstract syntax

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

Отношение к абстрактному синтаксису первого порядка

Абстрактное синтаксическое дерево - это Абстрактные потому что это математический объект который имеет определенную структуру по самой своей природе. Например, в абстрактный синтаксис первого порядка (FOAS) деревья, как обычно компиляторы, древовидная структура подразумевает отношение подвыражений, что означает, что скобки не требуются для устранения неоднозначности программ (как они есть в конкретный синтаксис ). HOAS раскрывает дополнительную структуру: взаимосвязь между переменными и их сайтами привязки. В представлениях FOAS переменная обычно представлена ​​идентификатором, причем связь между сайтом связывания и использованием указывается с помощью одно и тоже идентификатор. В HOAS нет имени для переменной; каждое использование переменной относится непосредственно к сайту привязки.

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

Выполнение

Один математический объект, который можно использовать для реализации HOAS, - это график где переменные связаны с их сайтами привязки через края. Другой популярный способ реализации HOAS (например, в компиляторах) - это индексы де Брёйна.

Использование в логических рамках

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

Например, логическая структура LF имеет λ-конструкцию, имеющую тип стрелки (→). Кодирование первого порядка конструкции объектного языка позволять будет (используя Двенадцать синтаксис):

exp: type.var: type.v: var -> exp.let: exp -> var -> exp -> exp.

Здесь, exp семейство выражений объектного языка. Семья вар - представление переменных (возможно, реализованное в виде натуральных чисел, которое не показано); постоянная v свидетельствует о том, что переменные - это выражения. Постоянная позволять - это выражение, которое принимает три аргумента: выражение (которое связывается), переменная (с которой оно связано) и другое выражение (внутри которого привязана переменная).

В канонический Представление HOAS того же объектного языка будет:

exp: type.let: exp -> (exp -> exp) -> exp.

В этом представлении переменные уровня объекта не отображаются явно. Постоянная позволять принимает выражение (которое связывается) и функцию мета-уровня exp → exp (тело пусть). Эта функция является более высокого порядка часть: выражение со свободной переменной представляется как выражение с дыры которые заполняются функцией мета-уровня при применении. В качестве конкретного примера мы построим выражение уровня объекта

пусть x = 1 + 2 в x + 3

(предполагая естественные конструкторы для чисел и сложения) с использованием подписи HOAS выше как

let (плюс 1 2) ([y] плюс y 3)

куда [y] e синтаксис Twelf для функции ${\displaystyle \lambda y.e}$.

Это конкретное представление имеет преимущества по сравнению с приведенными выше: во-первых, за счет повторного использования понятия привязки на мета-уровне кодировка обладает такими свойствами, как сохранение типа замена без необходимости их определять / доказывать. Таким образом, использование HOAS может значительно сократить количество шаблонный код имея дело с привязкой в ​​кодировке.

Абстрактный синтаксис более высокого порядка обычно применим только тогда, когда переменные объектного языка могут пониматься как переменные в математическом смысле (то есть как заместители для произвольных членов некоторой области). Это часто, но не всегда: например, нет никаких преимуществ, которые можно получить от кодирования HOAS динамический диапазон как это появляется в некоторых диалектах Лисп потому что переменные с динамической областью видимости не действуют как математические переменные.

Смотрите также

• Обобщенный алгебраический тип данных
• Параметрический абстрактный синтаксис высшего порядка (ФОАС)

Рекомендации

• Дейл Миллер; Гопалан Надатур (1987). Подход логического программирования к работе с формулами и программами (PDF). Симпозиум IEEE по логическому программированию. С. 379–388.
• Фрэнк Пфеннинг, Конал Эллиотт (1988). Абстрактный синтаксис высшего порядка (PDF). Труды ACM СИГПЛАН PLDI '88. С. 199–208. Дои:10.1145/53990.54010. ISBN  0-89791-269-1.
• Дж. Деспейру; А. Фелти; А. Хиршовиц (1995). Абстрактный синтаксис высшего порядка в Coq. Конспект лекций по информатике. 902. С. 124–138. Дои:10.1007 / BFb0014049. ISBN  978-3-540-59048-4. Архивировано из оригинал 30 августа 2006 г.
• Мартин Хофманн (1999). Семантический анализ абстрактного синтаксиса высшего порядка. 14-й ежегодный Симпозиум IEEE по логике в компьютерных науках. п. 204. ISBN  0-7695-0158-3.
• Дейл Миллер (2000). Абстрактный синтаксис для переменных связывания: обзор (PDF). Computational Logic - {CL} 2000. С. 239–253. Архивировано из оригинал (PDF) на 2006-12-02.
• Эли Барзилай; Стюарт Аллен (2002). Отражение абстрактного синтаксиса высшего порядка в Nuprl (PDF). Доказательство теорем в логиках высокого порядка 2002. С. 23–32. ISBN  3-540-44039-9. Архивировано из оригинал (PDF) на 2006-10-11.
• Эли Барзилай (2006). Оценщик самостоятельного хостинга с использованием HOAS (PDF). ICFP Практикум по схемному и функциональному программированию 2006 г.