Imperative Programming in Sets with Atoms

(Link).

Authors: Mikołaj Bojańczyk and Szymon Toruńczyk (University of Warsaw).

Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012), December 15-17 2012, Hyderabad, India (invited talk).

Journal reference: Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, Deepak D'Souza, Telikepalli Kavitha and Jaikumar Radhakrishnan (Eds.), pp 4-15 (2012).

Comments: All but one of the papers I've published have been on nominal sets, so it is hardly surprising that Google Scholar Updates have started me off with something in this vein, although I had not read this particular paper.

Nominal sets are a mathematical model in which each set-element is 'supported by' finite sets of atoms. What are atoms? In the original theory, developed in the 30s by the set theorists Abraham Fraenkel and Andrzej Mostowski, they were simply elements of an infinite set with no particular structure. This paper, and other recent papers by Bojańczyk and various co-authors, takes a more expansive view of what an atom might be, but first we will consider this unstructured case.

Frankel-Mostowski set theory was imported from the abstruse world of foundational set theory into the apparently more grounded domain of computer science by Murdoch Gabbay and Andrew Pitts, in their 1999 paper A new approach to abstract syntax involving binders, where it was used to model the syntax of computer programs and formal calculi. The problem the Gabbay-Pitts paper addressed was the syntactic construct of names, such as variable names in a program, which were and are a continual source of error and irritation to those who trying to reason formally about computation. The atoms of the old set theory played the role of names in various applications, and provided a model in which we can reason about names with rather less headaches than before. The label 'nominal sets', and more broadly 'nominal techniques', were (later) coined for this approach - not the only approach on the market for dealing with names, but certainly one of the most prominent and successful.

This paper is a companion piece to Bojańczyk et al's 2012 Towards Nominal Computation, in which a functional programming language Nλ was presented to support computation in nominal sets. I should note that Nλ is by no means the first example of the application of nominal sets to the design of programming languages, and some of these languages have actually been implemented while Nλ has not; in the last paragraph we will discuss what makes Bojańczyk et al's research programme truly distinctive. But setting that aside, in Imperative Programming in Sets with Atoms we see a language based on the same principles as Nλ, but in the imperative style. The distinctive construct of this language is the command

for x in X do I

where x is a variable, X is a set possibly containing some atoms, and I is a code fragment. This command triggers a parallel execution in which x is bound to every (correctly typed) element of X and I is executed accordingly. If any such run of I fails to terminate, then this code fails to terminate. What if they all do terminate? Suppose y is some variable that has an expression assigned to it in the code fragment I. If y is of type atom then every run of I must agree on y's value, regardless of the value of x, or we get a run-time error. But if y is of type set, the final value of y will be the union of all the runs of I.

The most interesting aspect of Bojańczyk et al's research direction (initiated by the 2011 Automata with Group Actions) is that they have substantially generalised the definition of nominal sets to accommodate various structure, such as orderings, on their atoms. Their claim is that these generalised nominal sets are useful not merely for 'dealing with names', but also for reasoning about and computing with a variety of infinite computational phenomena (if this sounds paradoxical, it isn't; the set of integers is infinite but no one objects to programs that manipulate them). For example, the semantics I have sketched above for the command 'for x in X do I' seems to require that X be finite to work in the real world, as we obviously cannot compute infinitely many parallel branches. However, some sets that are infinite but have a finite 'recipe' (technically, finitely many orbits) can be sensibly computed within the framework defined in this paper. The big application of the generalisation at this stage is a model of computation called finite-memory automata, but it's a pretty new direction, so there may well be more value to be found in this relaxation of the normal definition of nominal sets.