Nominal Monoids

(Link).

Author: Mikołaj Bojańczyk (University of Warsaw)

Reference: Theory of Computing Systems, Springer Open Choice, 4 April 2013

Comments: This, the twelfth paper I've read for this blog, represents something of a full circle, as it is by one of the same authors that wrote the first paper I looked at. In that post I discussed how Bojańczyk and collaborators had generalised the nominal sets model to capture certain computational phenomena, particularly to do with automata.

Automata are mathematical machines, somewhat like flowcharts, that accept certain inputs as 'questions' and return 'yes' or 'no' as their answer (more sophisticated notions of automata can return more complex output, and can also fail to terminate). The set of inputs that an automaton returns 'yes' to (in the jargon, recognises) is known as the automaton's language. This paper takes a more abstract view of formal language theory by, instead of using automata, using abstract algebraic structures called monoids to recognise languages, but the intention is the same - to study certain classes of computation at a clarifying level of mathematical abstraction.

There actually already exists a paper titled 'nominal monoids' (pdf), written in 2010 by Alexander Kurz (one of the authors of last week's paper) and collaborators, and perhaps surprisingly not cited in this paper. To be fair, the two notions of nominal monoid are a bit different in their emphasis - Kurz et al are interested in monoids equipped with binding structure, while Bojańczyk is interested in changing the 'alphabet' underlying languages to include an infinite number of letters, possibly equipped with some non-trivial structure. This point of view is known as languages with data words and is claimed to have applications e.g. with XML.

The key result of this paper is to adapt a result called the Schützenberger-McNaughton-Papert theorem from the setting of ordinary languages to languages with data words. This theorem makes a surprising and beautiful link between languages, the monoids that recognise them, and the logic that specifies them (specifically first-order logic, one of the basic logics you learn in a first or second year course). Bojańczyk extends notions of language, monoid, and even first-order logic to his generalised nominal setting, and his version of the theorem is proved with a new assumption that the monoid is 'ordered' in a certain sense. Interestingly, in the 'ungeneralised' nominal sets model that I'm most familiar with, this ordering requirement becomes unnecessary, so the statement of the theorem becomes very close indeed to the standard version.

Full Abstraction for Nominal Scott Domains

(Link).

Authors: Steffen Lösch and Andrew M. Pitts (University of Cambridge).

Conference / Reference: 40th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL '13), 23-25 January 2013, Rome, Italy (ACM Press).

Comments: Just two weeks ago I was remarking on the very large proportion of papers recommended by Google Scholar Updates that came from Cambridge; well, here is another one - the fourth of the last six. To be precise, I should say it was the fourth of the last eight, as I have decided to fudge the purity of the experiment for the first time by skipping two papers from the same authors as this this one, on the grounds that I was unlikely to gain much benefit from them.

This paper, whose second author was my PhD supervisor, is much more down my alley, as you might expect; it is another that deals with nominal sets, which I first discussed on this blog here. In that post I mentioned in passing that nominal sets had their origins in 1930s axiomatic set theory, before a rather surprising revival in 1999 by Murdoch Gabbay and Andrew Pitts, who employed them to model syntax with names and binders in computing. However their origins in deep set theory shouldn't be completely forgotten; their original use was for an attempt to construct a model of set theory where the axiom of choice failed.

Mathematics as conceived by Euclid is the process of enumerating axioms and inference rules that are obviously true, and then deriving truths from them (some of which may be far from obvious). Even in Euclid's own work this idealised picture did not really hold, as the fifth postulate of his geometry, regarding non-parallel lines, was rather more complicated that might be desired, and was long regarded as a flaw of his presentation. Much later it turned out that denying this postulate could lead to interesting and valuable mathematics for geometry in curved space. The attempt to axiomatise set theory in the early twentieth century came to a quite similar place, with the axiom of choice (which regards the ability to make systematic choices from unstructured sets, even infinite ones) as the useful but non-obvious 'rogue' axiom. Again, it turned out that both the axiom and its negation were compatible with the other, more obvious, set axioms, and so 'nonstandard set theory' in which the axiom failed - of which nominal sets are an example - could be developed and applied, as with non-Euclidean geometry.

The subjects of this paper, domain theory and denotational semantics, are techniques to interpret computer programs as objects in a mathematical setting that directly supports rich and complex computation phenomena such as recursion. This apparently esoteric material about set theoretic axioms matters because some of the proofs of the basic facts about domains use the axiom of choice. This paper defines a programming language PNA (and an extension, PNA+) with commands for manipulating and binding names, and develops domain theory within nominal sets to provide a characterisation of programs in this language. But domain theory within nominal sets needs, in part, to be reconstructed to avoid reliance on the now invalid axiom, which is one of interesting technical challenges addressed by this work (following earlier work by Glynn Winskel and David Turner (pdf), also at Cambridge).

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.