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