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

Эта статья включает в себя список литературы , связанной литературы или внешних ссылок , но ее источники остаются неясными, поскольку в ней отсутствуют встроенные цитаты . Пожалуйста, помогите улучшить эту статью, добавив более точные цитаты. ( Август 2010 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения )

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

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

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

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

Реализация [ править ]

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

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

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

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

exp: type.var: type.v: var -> exp.пусть: var -> exp -> exp -> exp.

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

Канонический Hoås представление одного и того же языка - объекта будет:

exp: type.пусть: ехр -> (ехр -> ехр) -> ехр.

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

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

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

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

где [y] e- синтаксис функции Twelf .${\ displaystyle \ lambda ye}$

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

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

См. Также [ править ]

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

Ссылки [ править ]

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