Абстрактный синтаксис высшего порядка
 | Эта статья включает список общих ссылок , но в ней отсутствуют достаточные соответствующие встроенные цитаты . ( Август 2010 г. ) |
В информатике ) — абстрактный синтаксис высшего порядка (сокращенно 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 -> ( exp -> exp ) -> exp . В этом представлении переменные уровня объекта не отображаются явно. Константа let принимает выражение (которое привязывается) и функцию метауровня exp → exp (тело лета). Эта функция является частью высшего порядка : выражение со свободной переменной имеет видпредставлено как выражение с пробелами , которые при применении заполняются функцией метауровня. В качестве конкретного примера мы могли бы построить выражение уровня объекта
пусть x = 1 + 2 в x + 3 (при условии наличия естественных конструкторов для чисел и сложения), используя приведенную выше подпись HOAS как
пусть ( плюс 1 2 ) ([ y ] плюс y 3 ) где [y] e это синтаксис Twelf для функции .
Это конкретное представление имеет преимущества помимо вышеперечисленных: во-первых, благодаря повторному использованию понятия привязки на метауровне кодирование обладает такими свойствами, как подстановка с сохранением типа, без необходимости их определять/доказывать. Таким образом, использование 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 г.