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

В информатике абстрактный синтаксис высшего порядка (сокращенно 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 : тип . var : тип . v : var -> exp . let : var -> exp -> exp -> exp .

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

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

 exp : тип . пусть : exp -> ( exp -> exp ) -> exp .

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

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

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

 пусть ( плюс 1 2 ) ([ y ] плюс y 3 )

где [y] e— синтаксис Twelf для функции . λ у . е {\displaystyle \лямбда йе}

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

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

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

Ссылки

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

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

  • J. Despeyroux; A. Felty; A. Hirschowitz (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.
  • Эли Барзилай; Стюарт Аллен (2002). Отражение абстрактного синтаксиса высшего порядка в Nuprl (PDF) . Доказательство теорем в логике высшего порядка 2002. стр.  23–32 . ISBN 3-540-44039-9. Архивировано из оригинала (PDF) 2006-10-11.
  • Эли Барзилай (2006). Самостоятельный оценщик с использованием HOAS (PDF) . Семинар ICFP по схемам и функциональному программированию 2006.
Взято с "https://en.wikipedia.org/w/index.php?title=Высший_порядок_абстрактного_синтаксиса&oldid=1193617257"