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

<p><strong>Longer answer.</strong> 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. </p>

<p>The problem is that in early formal proofs about languages with binders, a <em>disproportional</em> 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>

<p>$$
  P \quad ::= \quad x = E \ |\  while\ P\ do\ P \ |\   ...
$$</p>

<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>

<p>$$
  P \ ::=\ ... \ |\ \lambda x.P
$$</p>

<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. </p>

<p>Several techniques have been proposed for a better mathematisation of  the informal handling of binding.</p>

<ul>
<li><p><a href="https://en.wikipedia.org/wiki/Higher-order_abstract_syntax">Higher-order abstract syntax</a>,</p></li>
<li><p><a href="https://en.wikipedia.org/wiki/De_Bruijn_index">De Bruijn representation of binding</a>, </p></li>
<li><p>Getting rid of variables altogether by using combinators.</p></li>
<li><p>Nominal technique which replaces substitution by swapping. Swapping is essentially<sup>*</sup> a first-order operation and can be internalised in the ambient logic.</p></li>
</ul>

<p>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 <a href="http://www.inf.kcl.ac.uk/staff/urbanc/">Nominal Isabelle</a>, where most of the reasoning about binders can be hidden from the user. See <a href="http://www.inf.kcl.ac.uk/staff/urbanc/Publications/nom-cade-05.ps">Nominal Techniques in Isabelle/HOL</a> for a discussion. </p>

<hr>

<p><sup>*</sup> 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 <a href="http://www.sciencedirect.com/science/article/pii/S089054010300138X">Nominal logic, a first order theory of names and binding</a>, 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".</p>

CC BY-SA 3.0
2015-11-11T13:05:04.017Z
2015-11-11T15:01:22.693Z
2015-11-11T15:01:22.693Z
Martin Berger
<p>What is the significance of nominal techniques, as far as their application to the formal theory of bound variables is concerned?</p>

<p>I have been reading M. J. Gabbay's expository work on the topic that appeared in <em>Bulletin of Symbolic Logic</em>.  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.</p>

<p>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.</p>

<p>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.</p>

<p>Here's an attempt to answer my question: automorphisms on the set-theoretic universe induced by permutations of atoms are crucial in <em>proving</em> 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 <em>users</em> of the recursion/induction principles.  </p>

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

<p>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?</p>

CC BY-SA 3.0
2015-11-14T11:59:34.763Z
About Edit 2: if you propose a new foundational formalism such as nominal logic, you should show that it is sound. The translation into the Fraenkel-Mostowski permutation model of set theory achieves this. As to getting a proper treatment of $\alpha$-equivalence, as I said in my long answer below, this was formalised before in several ways, but the nominal approach is nicer than previous formalisations, where nicer means that formal reasoning involving $\alpha$-equivalence is closer to informal reasoning than with other approaches.
Martin Berger
CC BY-SA 3.0
2015-11-14T12:09:50.497Z
So no, you don't "need" nominal approaches, you can stick with de Bruijn, or locally-nameless or combinators or HOAS. But there is a price to pay, which is more awkward reasoning. You also lose the beautiful unexpected connections with other mathematical structure, e.g. the equivalence of Nom (the category of nominal sets and equivariant functions) with e.g. the Schanuel topos .
Martin Berger
<lo.logic><automated-theorem-proving>
What is the significance of nominal techniques?
Gonbê Nanasino
# What is the significance of nominal techniques?

(Asked by: username_0 on 2015-11-11)

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?

**Tags:** lo.logic, automated-theorem-proving
> **Comments:**
> **username_1**: About Edit 2: if you propose a new foundational formalism such as nominal logic, you should show that it is sound. The translation into the Fraenkel-Mostowski permutation model of set theory achieves this. As to getting a proper treatment of $\alpha$-equivalence, as I said in my long answer below, this was formalised before in several ways, but the nominal approach is nicer than previous formalisations, where nicer means that formal reasoning involving $\alpha$-equivalence is closer to informal reasoning than with other approaches.  
> **username_1**: So no, you don't "need" nominal approaches, you can stick with de Bruijn, or locally-nameless or combinators or HOAS. But there is a price to pay, which is more awkward reasoning. You also lose the beautiful unexpected connections with other mathematical structure, e.g. the equivalence of Nom (the category of nominal sets and equivariant functions) with e.g. the Schanuel topos .  

---

## 1 answers

### Answer by username_1 on 2015-11-11. Score: 8

**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](https://en.wikipedia.org/wiki/Higher-order_abstract_syntax),
* [De Bruijn representation of binding](https://en.wikipedia.org/wiki/De_Bruijn_index),
* 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](http://www.inf.kcl.ac.uk/staff/urbanc/), where most of the reasoning about binders can be hidden from the user. See [Nominal Techniques in Isabelle/HOL](http://www.inf.kcl.ac.uk/staff/urbanc/Publications/nom-cade-05.ps) 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](http://www.sciencedirect.com/science/article/pii/S089054010300138X), 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".


---

