Nominal terms (computer science)

Nominal terms are a metalanguage for embedding object languages with binding constructs into. Intuitively, they may be seen as an extension of first-order terms with support for name binding. Consequently, the native notion of equality between two nominal terms is alpha-equivalence (equivalence up to a permutative renaming of bound names).

Nominal unification is efficiently decidable. This fact led to the development of alphaProlog, a Prolog-like logic programming language with facilities for binding names in terms, where Prolog's standard first-order unification algorithm is replaced with nominal unification.

Nominal term embeddings may be seen as alternatives to de Bruijn encodings and higher-order abstract syntax, where the latter uses the simply-typed lambda-calculus as a metalanguage.