Nominal Sets and Nominal Computation Theory

Nominal Sets: Names and Symmetry in Computer Science
Andrew M. Pitts
Cambridge, 2013 (see also recent lecture notes)

Dagstuhl Seminar on Nominal Computation Theory
(organized by Mikolaj Bojanczyk, Bartek Klin, Alexander Kurz, and Andrew M. Pitts)

$\newcommand{\AA}{\mathbb{A}}$Part of my summer reading was Pitts' recent book on nominal sets.  Let $\AA$ be a set of names. A nominal set is a set $X$ equipped with a permutation action, that is, a function $\cdot_X :  Perm(\AA) \times X \to X$ where $Perm(\AA)$ is the set of all (finite) permutations on $X$.  Being a permutation action means that $id\cdot_X x = x$ and $(\pi \circ \pi') \cdot_X x = \pi \cdot_X \pi' \cdot_X x$ for all $\pi,\pi' \in Perm(\AA)$.  In addition, a nominal set must satisfy a finite-support property, which (oversimplifying slightly) requires that for each element there is a least support set $supp(x) \subseteq \AA$ such that for all $a,b \notin supp(x)$ we have $(a~b)\cdot_X x = x$.  Intuitively, the support is the set of names "appearing in" $x$, though in general there is no requirement that $X$ be a set of abstract syntax trees in the usual sense.




One of the main attractions of nominal sets and related techniques is the fact that they provide a well-behaved mathematical framework for understanding name-binding.  Given any nominal set $X$, we can form the quotient $(\AA \times X)/_\equiv$ of pairs of names and elements of $X$, by the least equivalence relation satisfying

\[(a,x) \equiv (b,y) \iff (a~b)\cdot_X x = y \text{ and } a \notin supp(y)\]

This turns out to coincide with the standard notion of $\alpha$-equivalence (if, say, we take $X$ to be the type of raw $\lambda$-terms with names from $\AA$).

This fact has lots of interesting consequences, including the development of a theory of abstract syntax trees modulo $\alpha$-equivalence with induction and recursion principles, which are explored further in Pitts' book. 

However, one recent development which is only discussed in passing in the book is the application of ideas from nominal sets to automata and other classical notions of computation.  This was one of several themes of the Dagstuhl seminar on nominal computation theory mentioned above (the others being the uses of nominal techniques for abstract syntax and semantics).  This is being explored by Bojanczyk and colleagues as a way to study automata over infinite alphabets.

The basic insight (at least confined to "classical" nominal sets) is that in some situations, it isn't necessary that a given object be finite in the usual sense; it may be enough that it only has finitely many distinct behaviors, up to some notion of symmetry.  In classical nominal sets, this notion of symmetry is given by considering the equivalence relation induced by the group action:

\[x \sim y \iff \exists \pi \in Perm(\AA). \pi \cdot_X x = y\]

The equivalence classes of this relation are called orbits; intuitively, the orbit of $x$ is the set of all $y \in X$ that we can get to by applying a permutation.  Permutations preserve distinctions among names but not their values.  A nominal set $X$ with finitely many orbits is called orbit-finite.

Then, if you consider classical finite automata, it turns out that many facts generalize if we replace the notion of finite (e.g. finite number of states, transitions, etc.) with orbit-finite.  Chapter 5 of Pitts' book discusses orbit-finiteness in some detail, and other papers by Bojanczyk and colleagues discuss applications and generalizations of this idea beyond "plain" nominal sets, by considering other structures and their automorphisms.  It isn't obvious yet whether this leads to insights that can be re-imported back into the reasoning-about-syntax setting, but maybe that doesn't matter.  It's an interesting area and I will probably be (re)reading some of the related papers soon.