Archive for the 'Nominal unification' Category

Equivariant unification

By James Cheney, from RTA 2005, available from James Cheney’s website:

Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves as the basis of logic programming and term rewriting techniques that provide similar advantages to, but remain simpler than, higher-order logic programming or term rewriting systems. Previous work on nominal rewriting and logic programming has relied on nominal unification, that is, unification up to equality in nominal logic. However, because of nominal logic’s equivariance property, these applications require a stronger form of unification, which we call equivariant unification. Unfortunately, equivariant unification and matching are NP-hard decision problems. This paper presents an algorithm for equivariant unification that produces a complete set of finitely many solutions, as well as NP decision procedure and a version that enumerates solutions one at a time. In addition, we present a polynomial time algorithm for swapping-free equivariant matching, that is, for matching problems in which the swapping operation does not appear.

Permissive nominal terms and their unification

By Gilles Dowek, Murdoch J. Gabbay and Dominic P. Mulligan, from CILC 2009, available from Murdoch J. Gabbay’s website:

We introduce permissive nominal terms. Nominal terms extend first-order terms with binding. They lack properties of first- and higher-order terms: Terms must be reasoned on in a context of ‘freshness assumptions’; it is not always possible to ‘choose a fresh variable symbol’ for a nominal term; and it is not always possible to ‘alpha-convert a bound variable symbol’. Permissive nominal terms recover these ‘always fresh’ and ‘always alpha-rename’ properties. Freshness contexts are elided and the notion of unifier is based on substitution alone rather than on nominal terms’ notion of substitution plus freshness conditions. We prove that all expressivity of nominal unification is retained.

A web based demo of the unification algorithm is available from Dominic Mulligan’s website.

Relating higher-order pattern unification and nominal unification

By James Cheney, from UNIF 2005, available from James Cheney’s website:

Higher-order pattern unification and nominal unification are two approaches to unifying modulo some form of α-equivalence (consistent renaming of bound names). The higher-order and nominal approaches seem superficially dissimilar. However, we show that a natural concretion (or name-application) operation for nominal terms can be used to simulate the behavior of higher-order patterns. We describe a form of nominal terms called nominal patterns that includes concretion and for which unification is equivalent to a special case of higher-order pattern unification, and then show that full higher-order pattern unification can be reduced to nominal unification via nominal patterns.

This is one in a series of three papers detailing the precise connection between higher-order pattern unification and nominal unification (they’re essentially “the same thing”).  Levy and Villaret expanded on Cheney’s work, removing the need for the translation to nominal patterns, with the concretion operator.  They demonstrated that higher-order pattern unifiability is preserved under their translation.  However, Dowek and Gabbay took Levy and Villaret’s results further, and came up with a translation where higher-order unifiers are preserved (they also sharpened Levy and Villaret’s result in another direction, by demonstrating that the Dowek/Gabbay translation is optimum, in a certain manner).

EDIT: the Dowek/Gabbay conference paper isn’t yet available, though the material from that paper will be in a journal paper “Permissive nominal terms and their unification” by Dowek, Gabbay and Mulligan, hopefully to appear soon.  If you have access to the ACM academic archive, then the Levy and Villaret paper is available here.