Modelling Infinite Structures with Atoms

(Link).

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

Conference: Workshop on Logic, Language, Information and Computation (WoLLIC 2013), 20-23 August, 2013, Darmstadt, Germany.

Journal reference: Lecture Notes in Computer Science, to appear.

Comments: The topic of this week's paper, from an author we've met twice before (here and here) is compactness. Compactness is the property that states that an infinite set of logical sentences is satisfiable (not contradictory) if and only if all the finite subsets of that infinite set are satisfiable. Some logics have the property, but others may not. The importance of this result may not be immediately obvious; it was first discovered by Kurt Gödel for first-order logic as a mere corollary to another theorem (completeness). However compactness went on to be a cornerstone principle of the mathematical field of model theory, which in a broad sense looks at how logical claims can be 'satisfied' by mathematical constructions.

Bojańczyk is interested in shifting first-order logic from its usual set-theoretic foundations to the world of nominal sets, the mathematical model for names in syntax that I've discussed in many places on this blog, e.g. here (in fact, as discussed in that link, Bojańczyk has a somewhat more general notion in mind than is usually meant by 'nominal sets', but such subtleties are orthogonal enough to the gist of this paper that we will pass by them). Making first-order logic nominal means that predicates can involve names, and disjunctions and conjunctions can be infinite, although only 'orbit-finite'.

Compactness is fundamentally a theorem about infinite and finite collections; in nominal sets such issues become a bit subtle. First, each element of a nominal set has what is called the finite support property, which means that it 'depends' on only finitely many names. This is a very helpful assumption in practice, and is motivated by the idea that real syntax can only ever involve finitely many names (even when the syntax might get infinitely large, as I discussed here). Moving up a level, we see that no non-trivial nominal set is finite. However there is a notion something like finiteness that does make sense for nominal sets - that of orbit-finiteness, which essentially says that the nominal set is finitely 'generated', rather like an infinite number of reflections in a hall of mirrors could be generated by a finite number of people standing in its middle.

With familiar notions of finiteness and infinity upended by the nominal sets model, getting a halfway sensible notion of compactness becomes quite difficult. It clearly makes no sense to state the theorem in terms of finite sets of sentences, because there are no interesting finite nominal sets. More surprisingly, the compactness postulate got by replacing the word 'finite' with 'orbit-finite' turns out to be false. In fact to validate that version of the theorem we initially need to jump outside of the nominal sets model entirely by axing the finite support property. This is by no means an illegitimate move but it does create worries, because sets with names but no finite support property are less relevant to computer science applications. However Bojańczyk finishes the paper by putting the rabbit back into the hat by defining what are called 'stratified models', more complicated constructions which have the finite support property but also satisfy compactness by 'approximating' the non-finitely supported models.

Update: Due to workload my next post will be a fortnight after this one.

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.

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.