Nominal logic, a first-order theory of names and binding

Andrew Pitts, from the Journal of Information and Computation, available from Andrew Pitts’s website:

This paper formalises within first-order logic some common practices in computer science to do with representing and reasoning about syntactical structures involving lexically scoped binding constructs. It introduces Nominal Logic, a version of first-order many-sorted logic with equality containing primitives for renaming via name-swapping, for freshness of names, and for name-binding. Its axioms express properties of these constructs satisfied by the FM-sets model of syntax involving binding, which was recently introduced by the author and M.J. Gabbay and makes use of the Fraenkel-Mostowski permutation model of set theory. Nominal Logic serves as a vehicle for making two general points. First, name-swapping has much nicer logical properties than more general, non-bijective forms of renaming while at the same time providing a sufficient foundation for a theory of structural induction/recursion for syntax modulo α-equivalence. Secondly, it is useful for the practice of operational semantics to make explicit the equivariance property of assertions about syntax – namely that their validity is invariant under name-swapping.


1 Response to “Nominal logic, a first-order theory of names and binding”

  1. 1 Samuel Gélineau October 9, 2009 at 5:17 pm

    Strange, I thought nominal logic used “∇”, not “ᴎ”? Regardless, here’s how to define a function counting variable occurrences using the work described in the paper.

    -- sorts
    Var  : atom-sort
    Term : data-sort
    Nat  : data-sort
    -- lambda calculus terms
    var : Var        -> Term
    app : Term, Term -> Term
    lam : [Var]Term  -> Term
    -- function counting variable occurrences
    countV : Var, Term -> Nat
    -- countV’s behaviour is defined by the following axioms.
    (∀ x : Var)             countV(x, var(y)) = 1
    (∀ x : Var) (ᴎ y : Var) countV(x, var(y)) = 0
    (∀ s, t : Term) countV(x, app(s, t)) = countV(x, s)
                                         + countV(x, t)
    (∀ x, y : Var) (ᴎ z : Var)
    (∀ s    : Term) countV(x, lam(y.s) ) = countV(x, swap(y, z, s))
    -- we swapped y with a fresh Var to avoid capture.

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: