Higher-order Abstract Syntax
   HOME

TheInfoList



OR:

In
computer science Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
, higher-order abstract syntax (abbreviated HOAS) is a technique for the representation of
abstract syntax tree An abstract syntax tree (AST) is a data structure used in computer science to represent the structure of a program or code snippet. It is a tree representation of the abstract syntactic structure of text (often source code) written in a formal ...
s for languages with variable
binders Ring binders (loose leaf binders, looseleaf binders, or sometimes called files in Britain) are large folders that contain file folders or hole punched papers (called loose leaves). These binders come in various sizes and can accommodate an arra ...
.


Relation to first-order abstract syntax

An abstract syntax is ''abstract'' because it is represented by
mathematical object A mathematical object is an abstract concept arising in mathematics. Typically, a mathematical object can be a value that can be assigned to a Glossary of mathematical symbols, symbol, and therefore can be involved in formulas. Commonly encounter ...
s that have certain structure by their very nature. For instance, in '' first-order abstract syntax'' (''FOAS'') trees, as commonly used in
compiler In computing, a compiler is a computer program that Translator (computing), translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primaril ...
s, 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.


Implementation

One mathematical object that could be used to implement HOAS is a
graph Graph may refer to: Mathematics *Graph (discrete mathematics), a structure made of vertices and edges **Graph theory, the study of such graphs and their properties *Graph (topology), a topological space resembling a graph in the sense of discret ...
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.


Use in logic programming

The first programming language which directly supported λ-bindings in syntax was the higher-order
logic programming Logic programming is a programming, database and knowledge representation paradigm based on formal logic. A logic program is a set of sentences in logical form, representing knowledge about some problem domain. Computation is performed by applyin ...
language
λProlog λProlog, also written lambda Prolog, is a logic programming language featuring polymorphic typing, modular programming, and higher-order programming. These extensions to Prolog are derived from the higher-order hereditary Harrop formulas used ...
. The paper that introduced the term HOAS used λProlog code to illustrate it. Unfortunately, when one transfers the term HOAS from the logic programming to the
functional programming In computer science, functional programming is a programming paradigm where programs are constructed by Function application, applying and Function composition (computer science), composing Function (computer science), functions. It is a declarat ...
setting, that term implies the identification of bindings in syntax with functions over expressions. In this latter setting, HOAS has a different and problematic sense. The term λ-tree syntax has been introduced to refer specifically to the style of representation available in the logic programming setting. While different in detail, the treatment of bindings in λProlog is similar to their treatment in logical frameworks, elaborated in the next section.


Use in logical frameworks

In the domain of
logical framework In logic, a logical framework provides a means to define (or present) a logic as a signature in a higher-order type theory in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework ty ...
s, the term higher-order abstract syntax is usually used to refer to a specific representation that uses the binders of the
meta-language In logic and linguistics, a metalanguage is a language used to describe another language, often called the ''object language''. Expressions in a metalanguage are often distinguished from those in the object language by the use of italics, quot ...
to encode the binding structure of the object language. For instance, the logical framework LF has a λ-construct, which has arrow (→) type. As an example, consider we wanted to formalize a very primitive language with untyped expressions, a built-in set of variables, and a let construct (let = in ), which allows to bind variables var with definition exp in expressions exp'. In
Twelf Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at Carnegie Mellon University. It is used for logic programming and for the formalization of programming language theory. Introduction At ...
syntax, we could do as follows: Here, exp is the type of all expressions and var the type of all built-in variables (implemented perhaps as
natural number In mathematics, the natural numbers are the numbers 0, 1, 2, 3, and so on, possibly excluding 0. Some start counting with 0, defining the natural numbers as the non-negative integers , while others start with 1, defining them as the positive in ...
s, which is not shown). The constant v acts as a casting function and witnesses the fact that variables are expressions. Finally, the constant let represents let constructs of the form let = in : it accepts a variable, an expression (being bound by the variable), and another expression (that the variable is bound within). The
canonical The adjective canonical is applied in many contexts to mean 'according to the canon' the standard, rule or primary source that is accepted as authoritative for the body of knowledge or literature in that context. In mathematics, ''canonical exampl ...
HOAS representation of the same object language would be: In this representation, object level variables do not appear explicitly. The constant let takes an expression (that is being bound) and a meta-level function exp → exp (the body of the let). This function is the ''higher-order'' part: an expression with a free variable is represented as an expression with ''holes'' that are filled in by the meta-level function when applied. As a concrete example, we would construct the object level expression (assuming the natural constructors for numbers and addition) using the HOAS signature above as where e is Twelf's syntax for the function \lambda y.e. This specific representation has advantages beyond the ones above: for one, by reusing the meta-level notion of binding, the encoding enjoys properties such as type-preserving ''substitution'' without the need to define/prove them. In this way using HOAS can drastically reduce the amount of
boilerplate code In computer programming, boilerplate code, or simply boilerplate, are sections of code that are repeated in multiple places with little to no variation. When using languages that are considered ''verbose'', the programmer must write a lot of boile ...
having to do with binding in an encoding. Higher-order abstract syntax is generally only applicable when object language variables can be understood as variables in the mathematical sense (that is, as stand-ins for arbitrary members of some domain). This is often, but not always, the case: for instance, there are no advantages to be gained from a HOAS encoding of dynamic scope as it appears in some dialects of
Lisp Lisp (historically LISP, an abbreviation of "list processing") is a family of programming languages with a long history and a distinctive, fully parenthesized Polish notation#Explanation, prefix notation. Originally specified in the late 1950s, ...
because dynamically scoped variables do not act like mathematical variables.


See also

*
Generalized algebraic data type In functional programming, a generalized algebraic data type (GADT, also first-class phantom type, guarded recursive datatype, or equality-qualified type) is a generalization of a Parametric polymorphism, parametric algebraic data type (ADT). Ove ...
* Parametric higher-order abstract syntax (PHOAS)


References


Further reading

* * * * {{DEFAULTSORT:Higher-Order Abstract Syntax Type theory Logic programming Dependently typed programming Programming language theory