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.

0 Responses to “Permissive nominal terms and their unification”

  1. Leave a Comment

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: