Higher-order Abstract Syntax - Use in Logical Frameworks

Use in Logical Frameworks

In the domain of logical frameworks, the term higher-order abstract syntax is usually used to refer to a specific representation that uses the binders of the meta-language to encode the binding structure of the object language.

For instance, the logical framework LF has a λ-construct, which has arrow (→) type. A first-order encoding of an object language construct let would be (using Twelf syntax):

exp : type. var : type. v : var -> exp. let : exp -> var -> exp -> exp.

Here, exp is the family of object language expressions. The family var is the representation of variables (implemented perhaps as natural numbers, which is not shown); the constant v witnesses the fact that variables are expressions. The constant let is an expression that takes three arguments: an expression (that is being bound), a variable (that it is bound to) and another expression (that the variable is bound within).

The canonical HOAS representation of the same object language would be:

exp : type. let : exp -> (exp -> exp) -> exp.

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

let x = 1 + 2 in x + 3

(assuming the natural constructors for numbers and addition) using the HOAS signature above as

let (plus 1 2) ( plus y 3)

where e is Twelf's syntax for the function .

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 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 because dynamically scoped variables do not act like mathematical variables.