Высший порядок абстрактного синтаксиса: представление связывания переменных
Higher-order abstract syntax
Высокоуровневый абстрактный синтаксис (HOAS) в информатике: представление деревьев синтаксиса с переменными. Структура связывания переменных и их областей видимости.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
В информатике абстрактный синтаксис высшего порядка (сокращенно HOAS) — это техника представления абстрактных синтаксических деревьев для языков с переменными-связывателями.
In computer science, higher order abstract syntax (abbreviated HOAS) is a technique for the representation of abstract syntax trees for languages with variable binders.
Отношение к абстрактному синтаксису первого порядка
Абстрактный синтаксис является абстрактным, поскольку он представлен математическими объектами, обладающими определенной структурой по самой своей природе. Например, в деревьях абстрактного синтаксиса первого порядка (FOAS), которые обычно используются в компиляторах, структура дерева подразумевает отношение подвыражения, что означает, что скобки не требуются для устранения неоднозначности в программах (в отличие от конкретного синтаксиса). HOAS раскрывает дополнительную структуру: связь между переменными и местами их привязки. В представлениях FOAS переменная обычно представляется идентификатором, а связь между местом привязки и использованием указывается с помощью того же идентификатора. В HOAS переменная не имеет имени; каждое использование переменной напрямую ссылается на место привязки. Существует ряд причин, по которым этот подход полезен. Во-первых, он делает структуру привязки программы явной: как нет необходимости объяснять приоритет операторов в представлении FOAS, так и нет необходимости иметь под рукой правила привязки и области видимости для интерпретации представления HOAS. Во-вторых, программы, которые являются альфа-эквивалентными (отличаются только именами связанных переменных), имеют идентичные представления в HOAS, что может повысить эффективность проверки на эквивалентность.
An abstract syntax is abstract because it is represented by mathematical objects that have certain structure by their very nature. For instance, in first order abstract syntax (FOAS) trees, as commonly used in compilers, the tree structure implies the subexpression relation, meaning that no parentheses are required to disambiguate programs (as they are, in the concrete syntax). HOAS exposes additional structure: the relationship between variables and their binding sites. In FOAS representations, a variable is typically represented with an identifier, with the relation between binding site and use being indicated by using the same identifier. With HOAS, there is no name for the variable; each use of the variable refers directly to the binding site. There are a number of reasons why this technique is useful. First, it makes the binding structure of a program explicit: just as there is no need to explain operator precedence in a FOAS representation, there is no need to have the rules of binding and scope at hand to interpret a HOAS representation. Second, programs that are
alpha equivalent (differing only in the names of bound variables) have identical representations in HOAS, which can make equivalence checking more efficient.
Реализация
Один математический объект, который можно использовать для реализации HOAS, — это граф, в котором переменные связаны со своими областями привязки посредством рёбер. Другой распространённый способ реализации HOAS (например, в компиляторах) — использование индексов де Брюйна.
One mathematical object that could be used to implement HOAS is a graph where variables are associated with their binding sites via edges. Another popular way to implement HOAS (in, for example, compilers) is with de Bruijn indices.