Higher-Order Abstract Syntax

Definition

Higher-order abstract syntax is a representation of lexical scoping with binders in which binding in the object language is represented by binding in a meta-language.

Instead of storing a variable name inside a constructor, a binder is represented by a meta-level function. This lets renaming and capture-avoiding substitution be handled by the meta-language rather than by explicit syntax manipulation.

Example

In a first-order representation one might use a constructor such as $\text{Lam}:\text{String}\to \text{Term}\to \text{Term}$. In a HOAS representation one instead uses a constructor of the shape $\text{Lam}:(\text{Term}\to \text{Term})\to \text{Term}$.

The meta-language’s own lambda abstraction then represents binding for the object language.

Related Concepts

Lexical Scope
Structural Substitution
Alpha Equivalence
De Bruijn Indices
Nameful Scoping
Nominal Sets