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.[clarification needed] Consequently, the native notion of equality between two nominal terms is alpha-equivalence (equivalence up to a permutative renaming of bound names). Nominal terms came out of a programme of research into nominal sets, and have a concrete semantics in those sets.
Where the regular unification found in Prolog is linear in the size of terms compared, the extension to faithfully capture equivalence of nominal terms, called nominal unification in the literature, is quadratic (Calvès 2013). Based on an earlier PTIME algorithm for nominal unification, alphaProlog is a Prolog-like logic programming language with facilities for binding names in terms, which was intended to be useful for programs acting on program syntax (Cheney 2004).
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.
Motivation
editMany 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 (and first-order computational properties) of de Bruijn encodings.
Syntax
editThis section is empty. You can help by adding to it. (July 2010) |
Example embeddings
editThis section is empty. You can help by adding to it. (July 2010) |
Unification algorithm
editThis section is empty. You can help by adding to it. (July 2010) |
Relation with higher-order patterns
editHigher-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.
References
edit- Christophe Calvès and Maribel Fernandez (2008). "A polynomial nominal unification algorithm". Theoretical Computer Science. 403 (2–3): 285–306. doi:10.1016/j.tcs.2008.05.012.
- Christophe Calvès (2013). "Unifying nominal unification". Proc. 4th International Conference on Rewriting Techniques and Applications. pp. 143–157. doi:10.4230/LIPIcs.RTA.2013.143.
- James Cheney (2004). Nominal Logic Programming (PhD). Cornell University.
- James Cheney (2005). "Relating higher-order pattern unification and nominal unification". Proceedings of the 19th International Workshop on Unification (UNIF). pp. 104–119.
- Gilles Dowek, Murdoch J. Gabbay and Dominic P. Mulligan (2010). "Permissive nominal terms and their unification". Logic Journal of the IGPL. 18 (6): 769–822. CiteSeerX 10.1.1.185.3105. doi:10.1093/jigpal/jzq006.
- Jorgi Levy and Mateu Villaret (2008). "Nominal unification from a higher-order perspective". Proceedings of the 19th International Workshop on Rewriting Techniques and Applications (RTA). pp. 246–260.
- Christian Urban, Andrew M. Pitts and Murdoch J. Gabbay (2004). "Nominal unification". Theoretical Computer Science. 323 (1–3): 473–497. doi:10.1016/j.tcs.2004.06.016.