What is the significance of nominal techniques?

Question

What is the significance of nominal techniques, as far as their application to the formal theory of bound variables is concerned?

I have been reading M. J. Gabbay's expository work on the topic that appeared in Bulletin of Symbolic Logic. I understand that, the main contribution of nominal techniques to the nasty problem of $\alpha$-conversion is that they introduced new principles of induction and recursion, and a new quantifier. However, I am not sure if the use of orbits instead of $\alpha$-equivalence classes is strictly necessary for these purposes - because orbits and equivalence classes are essentially the same thing.

I understand the theory of nominal sets are very fruitful in that it can be applied in many different areas - including infinite automata theory and domain theory, due mainly to its general nature. I would like to know the relevance of the theory's generality - replacing $\alpha$-equivalence classes with orbits - in the very first problem that it is meant to solve, that is, $\alpha$-equivalence of syntactic objects.

EDIT: I knew how nominal techniques could be applied to reasoning up to $\alpha$-equivalence; my question was more about the theory's internal methodology, that is, the focus on the group action.

Here's an attempt to answer my question: automorphisms on the set-theoretic universe induced by permutations of atoms are crucial in proving the new recursion/induction principles, so is the reinterpretation of $\alpha$-equivalence as orbits. However, this reinterpretation might or might not be relevant to the users of the recursion/induction principles.

Let me know if there is something in my answer to be added or corrected.

EDIT 2: My question might have been better phrased as: do we really need to appeal to axiomatic set theory - something very powerful - to get a proper treatment of alpha-equivalence?

Answer 1

Short answer. Formal reasoning about binding and $\alpha$-conversion with nominal approaches is closer to intuitive reasoning than alternative approaches.

Longer answer. Binders arise everywhere in mathematics and computer science. Dealing with binders has historically been done in a handwaving way (e.g. assuming Barendregt's variable convention). This works well in informal mathematics, but breaks down in formal reasoning. In implementations of programming languages, this problem was initially handled with some form of renaming using a global operation, often called gensym, that creates globally fresh variables. Already in the implementation of programming languages that has some disadvantages, but the problem comes to the fore when reasoning about formal languages with binders, in particular about certified software.

The problem is that in early formal proofs about languages with binders, a disproportional amount of effort was dedicated to proving largely uninteresting lemmas about substitutions and $\alpha$-conversion. The core of the problem is that programming language syntax is usually defined inductively. For example

$$ P \quad ::= \quad x = E \ |\ while\ P\ do\ P \ |\ ... $$

Given this genesis of programming language syntax, it is natural to prove program properties by structural induction on program syntax. This works fine for simple languages like that above, but once we add binders

$$ P \ ::=\ ... \ |\ \lambda x.P $$

the situation changes. $P$ is not a subterm of $\lambda x.P$. We want to identfy programs up to consistent renaming of bound variables, for example we don't want to distinguish $\lambda x.ax$ from $\lambda y.ay$. In other words, programs are equivalence classes ... and structural induction goes out of the window.

Several techniques have been proposed for a better mathematisation of the informal handling of binding.

• Higher-order abstract syntax,

• De Bruijn representation of binding,

• Getting rid of variables altogether by using combinators.

• Nominal technique which replaces substitution by swapping. Swapping is essentially^* a first-order operation and can be internalised in the ambient logic.

Of all those proposals, the reasoning about binders with nominal techniques is closest to the intuitive "handwaving" done to handle binders in informal reasoning. That is the key advantage of nominal techniques. This might be best observed in Nominal Isabelle, where most of the reasoning about binders can be hidden from the user. See Nominal Techniques in Isabelle/HOL for a discussion.

---

^* There is a subtle issue in that if you want to define higher-order functions by recursion in nominal logic, the recursion operator requires some kind of freshness. See the conclusion of Pitt's Nominal logic, a first order theory of names and binding, which points out that "Nominal Logic does not give a complete axiomatisation of the notion of finite support that underlies the notion of freshness in FM-sets. Nevertheless, the first-order properties of a notion of freshness of names presented in this paper seem sufficient to develop a useful theory, independent of any particular object-level language involving binders".