Many interesting calculi, logics and programming languages that are commonly seen in computer science feature name binding constructs. For instance, the universal quantifier from first-order logic, the lambda-binder from the lambda-calculus, and the pi-binder from the pi-calculus are all examples of name-binding constructs. Computer scientists often need to manipulate abstract syntax trees. For instance, compiler writers perform many manipulations of abstract syntax trees during the various optimisation and elaboration phases of compiler execution. In particular, when working with abstract syntax trees with name binding constructs, we often want to work on alpha-equivalence classes, implement capture-avoiding substitutions, and make it easy to generate fresh names. How best to do this, in a bug free and reliable manner, motivates a large amount of research. Prior attempts at solving this problem include 'nameless approaches' such as de Bruijn indices and levels, and higher-order approaches such as higher-order abstract syntax. Nominal terms are another, relatively new, approach that retain explicit names for bound variables like higher-order abstract syntax, whilst retaining the first-order flavour of de Bruijn encodings.
Syntax
Example embeddings
Unification algorithm
Relation with higher-order patterns
Higher-order unification is known to be undecidable. This motivates the search for subsets of lambda-terms that enjoy a computationally well-behaved unification procedure. Higher-order patterns, proposed by Miller, are one such set. Higher-order patterns are lambda-terms where the arguments of a free variable are all distinct bound variables. They possess an efficiently decidable unification procedure, and as a result, have been widely implemented, notably in the logic programming language lambdaProlog. A recent body of work has investigated the connections between nominal terms and higher-order patterns, and consequently between nominal unification and higher-order pattern unification. Cheney proposed an extension of nominal terms called nominal patterns. He then provided a translation between nominal patterns and higher-order patterns which preserved unifiers. Later, Levy and Villaret demonstrated a translation between nominal terms and higher-order patterns that preserves the notion of unifiability. That is, if two nominal terms are unifiable, then their translated pattern counterparts are also unifiable. Dowek and Gabbay later sharpened Levy and Villaret's translation, proving that in some sense their translation is the best that there can be, and proved that the improved translation preserves unifiers. That is, if two nominal terms are unifiable by some substitution, then the corresponding higher-order pattern unification problem under the translation is solved by the translated substitution. For their proof, Dowek and Gabbay used a variation of nominal terms called permissive nominal terms. However, a translation from permissive nominal terms and back again also exists, completing the translation between nominal terms and higher-order patterns.
