Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques (vol 8, pg 769, 2010) [Book Review]

Logic Journal of the IGPL 20 (1):769-822 (2012)
  Copy   BIBTEX


Nominal terms extend first-order terms with binding. They lack some properties of first- and higher-order terms: Terms must be reasoned about in a context of ‘freshness assumptions’; it is not always possible to ‘choose a fresh variable symbol’ for a nominal term; it is not always possible to ‘α-convert a bound variable symbol’ or to ‘quotient by α-equivalence’; the notion of unifier is not based just on substitution. Permissive nominal terms closely resemble nominal terms but they recover these properties, and in particular the ‘always fresh’ and ‘always rename’ properties. In the permissive world, freshness contexts are elided, equality is fixed, and the notion of unifier is based on substitution alone rather than on nominal terms’ notion of unification based on substitution plus extra freshness conditions. We prove that expressivity is not lost moving to the permissive case and provide an injection of nominal terms unification problems and their solutions into permissive nominal terms problems and their solutions. We investigate the relation between permissive nominal unification and higher-order pattern unification. We show how to translate permissive nominal unification problems and solutions in a sound, complete, and optimal manner, in suitable senses which we make formal



    Upload a copy of this work     Papers currently archived: 91,252

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

‘That’-Clauses and Non-nominal Quantification.Tobias Rosefeldt - 2008 - Philosophical Studies 137 (3):301 - 333.
Completeness and Herbrand Theorems for Nominal Logic.James Cheney - 2006 - Journal of Symbolic Logic 71 (1):299 - 320.
Taming the Infinite. [REVIEW]Michael Potter - 1996 - British Journal for the Philosophy of Science 47 (4):609-619.
Nominal definition in the writings of Ibn taymiyya.Sobhi Rayan - 2009 - International Studies in the Philosophy of Science 23 (2):123 – 141.
Infinite chains and antichains in computable partial orderings.E. Herrmann - 2001 - Journal of Symbolic Logic 66 (2):923-934.


Added to PP

5 (#1,476,866)

6 months
1 (#1,478,435)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Completeness and Herbrand Theorems for Nominal Logic.James Cheney - 2006 - Journal of Symbolic Logic 71 (1):299 - 320.

Add more references