Nominal techniques
In computer science, nominal techniques are a range of related tools, ostensibly for working with abstract syntax involving variable binding.
Nominal terms
Nominal terms are a generalisation of first-order terms with name binding, an in-built notion of meta-variable ("unknown") with a non-capture avoiding substitution action, a notion of derivable freshness (a necessary generalisation of the free-variables of a term in the presence of unknowns), and an elegant definition of alpha-equivalence, centred around variable permutations. Their semantics is provided by nominal sets.
Despite the presence of name binders, unification of nominal terms is efficiently decidable.
In contrast with de Bruijn indices, nominal encodings are "nameful", yet unlike higher order approaches, nominal encodings are first order, and have a sets, rather than a function based semantics.
Practical uses
Nominal terms have been used in the programming language alpha-Prolog, and related techniques are used in the nominal datatype package, for the Isabelle proof assistant. The Haskell Nominal Toolkit provides an implementation of nominal terms, with associated rewriting and unification algorithms, for the Haskell programming language.
See also
References
- Christian Urban, Andrew M. Pitts and Murdoch J. Gabbay (2004). "Nominal Unification" (PDF). Theoretical Computer Science. 323: 473--497.