Абстрактный синтаксис высшего порядка

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

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

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

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

Выполнение

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

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

Первый язык программирования, который напрямую поддерживал высшего порядка λ-привязки в синтаксисе были логическим программированием . язык λProlog . ^[1] Статья, в которой был введен термин HOAS. ^[2] использовал Код λProlog, иллюстрирующий это. К сожалению, когда кто-то переносит термин HOAS от логического программирования к функциональному программированию установка, этот термин подразумевает идентификацию привязок в синтаксисе с функциями над выражениями. В этом последнем случае HOAS имеет другой и проблемный смысл. Термин синтаксис λ-дерева был введен в конкретно обратитесь к стилю представления, доступному в настройка логического программирования. ^[3]^[4] Несмотря на различия в деталях, обработка привязок в λProlog аналогична. их трактовке в логических рамках, подробно описанной в следующем разделе.

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

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

Например, логическая структура LF имеет λ-конструкцию, имеющую стрелку (→) тип. В качестве примера предположим, что мы хотели формализовать очень примитивный язык с нетипизированными выражениями, встроенным набором переменных и конструкцией let ( let <var> = <exp> in <exp'>), что позволяет связывать переменные var с определением exp в выражениях exp'. В синтаксисе Twelf мы могли бы сделать следующее:

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

Здесь, exp это тип всех выражений и var тип всех встроенных переменных (возможно, реализованных как натуральные числа , которые не показаны). Константа v действует как функция приведения и подтверждает тот факт, что переменные являются выражениями. Наконец, константа let представляет конструкции let формы let <var> = <exp> in <exp>: он принимает переменную, выражение (связанное с переменной) и другое выражение (с которым связана переменная).

Каноническое : представление того же объектного языка в HOAS будет следующим

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

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

 let x = 1 + 2
 in x + 3

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

 let (plus 1 2) ([y] plus y 3)

где [y] e это синтаксис Twelf для функции $\lambda y.e$ .

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

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

См. также

Ссылки

^ Дейл Миллер ; Гопалан Надатур (1987). Подход к управлению формулами и программами с помощью логического программирования (PDF) . Симпозиум IEEE по логическому программированию. стр. 379–388.
^ Фрэнк Пфеннинг , Конал Эллиотт (1988). Абстрактный синтаксис высшего порядка (PDF) . Материалы ACM SIGPLAN PLDI '88. стр. 199–208. дои : 10.1145/53990.54010 . ISBN 0-89791-269-1 .
^ Дейл Миллер (2000). Абстрактный синтаксис связывателей переменных: обзор (PDF) . Вычислительная логика - {CL} 2000. стр. 239–253. Архивировано из оригинала (PDF) 2 декабря 2006 г.
^ Миллер, Дейл (октябрь 2019 г.). «Возвращение к механизированной метатеории» (PDF) . Журнал автоматизированного рассуждения . 63 (3): 625–665. дои : 10.1007/s10817-018-9483-3 . S2CID 254605065 .

Дальнейшее чтение

Ж. Десперу; А. Фелти; А. Хиршовиц (1995). «Абстрактный синтаксис высшего порядка в Coq». Типизированные лямбда-исчисления и приложения . Конспекты лекций по информатике. Том. 902. стр. 124–138. дои : 10.1007/BFb0014049 . ISBN 978-3-540-59048-4 . Архивировано из оригинала 30 августа 2006 г.
Мартин Хофманн (1999). Семантический анализ абстрактного синтаксиса высшего порядка . 14-й ежегодный симпозиум IEEE по логике в информатике . п. 204. ИСБН 0-7695-0158-3 .
Эли Барзилай; Стюарт Аллен (2002). Отражение абстрактного синтаксиса высшего порядка в Nuprl (PDF) . Доказательство теорем в логике высшего порядка 2002. С. 23–32. ISBN 3-540-44039-9 . Архивировано из оригинала (PDF) 11 октября 2006 г.
Эли Барзилай (2006). Оценщик самостоятельного размещения с использованием HOAS (PDF) . Семинар ICFP по схемам и функциональному программированию, 2006 г.

[1] Дейл Миллер ; Гопалан Надатур (1987). Подход к управлению формулами и программами с помощью логического программирования (PDF) . Симпозиум IEEE по логическому программированию. стр. 379–388.

[2] Фрэнк Пфеннинг , Конал Эллиотт (1988). Абстрактный синтаксис высшего порядка (PDF) . Материалы ACM SIGPLAN PLDI '88. стр. 199–208. дои : 10.1145/53990.54010 . ISBN 0-89791-269-1 .

[3] Дейл Миллер (2000). Абстрактный синтаксис связывателей переменных: обзор (PDF) . Вычислительная логика - {CL} 2000. стр. 239–253. Архивировано из оригинала (PDF) 2 декабря 2006 г.

[4] Миллер, Дейл (октябрь 2019 г.). «Возвращение к механизированной метатеории» (PDF) . Журнал автоматизированного рассуждения . 63 (3): 625–665. дои : 10.1007/s10817-018-9483-3 . S2CID 254605065 .

[1]

[2]

[3]

[4]