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.


Read more »