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.