Nominal Logic: A First Order Theory of Names and Binding

This talk describes an approach to formalising certain notions that are common in the practice of representing and reasoning about syntax involving variable binding. We concentrate on the use of explicitly named bound variables, rather than the use of nameless terms, explicit substitutions, or higher order abstract syntax. We introduce Nominal Logic, a version of first-order many-sorted logic that gives a mathematical status to the taxonomic distinction often made between free and bound names. Nominal Logic contains primitives for renaming via name-swapping and for freshness of names. Its axioms express key properties of these primitives derived from the FM-sets model of syntax introduced by Gabbay and Pitts (2001). The main point of the talk is to indicate that name-swapping has much nicer properties than renaming and to emphasise the usefulness, for the practice of operational semantics, of making explicit the equivariance property of assertions about syntax---namely that their validity is invariant under swapping bindable names.
Andrew Pitts
Last modified: Wed Oct 24 12:03:05 BST 2001