Mikołaj Bojańczyk

July 14, 2015

Mikołaj Bojańczyk

*Nominal Monoids.*Theory Comput. Syst., 2013 PDFMikołaj Bojańczyk, Bartek Klin, Slawomir Lasota 0001

*Automata theory in nominal sets.*Logical Methods in Computer Science, 2014 PDFMikołaj Bojańczyk, Slawomir Lasota 0001

*A Machine-Independent Characterization of Timed Languages.*ICALP (2), 2012 PDFMikołaj Bojańczyk, Laurent Braud, Bartek Klin, Slawomir Lasota 0001

*Towards nominal computation.*POPL, 2012 PDFMikołaj Bojańczyk, Szymon Torunczyk

*Imperative Programming in Sets with Atoms.*FSTTCS, 2012 PDFMikołaj Bojańczyk, Thomas Place

*Toward Model Theory with Data Values.*ICALP (2), 2012 PDFMikołaj Bojańczyk, Luc Segoufin, Szymon Torunczyk

*Verification of database-driven systems via amalgamation.*PODS, 2013 PDFMikołaj Bojańczyk

*Modelling Infinite Structures with Atoms.*WoLLIC, 2013 PDFMikołaj Bojańczyk, Bartek Klin, Slawomir Lasota 0001, Szymon Torunczyk

*Turing Machines with Atoms.*LICS, 2013 PDF

Atoms are a theory project that we are developing in Warsaw, which even has its blog and a book. The project was originally motivated by trying to understand automata on data words and data trees. The idea is to consider sets with ur-elements that are called atoms, and to consider a different notion of finiteness: a set is called *orbit-finite* if it has finitely many elements up to permutations of the atoms.

We began by studying orbit-finite automata and monoids. The papers [1,2,3,7] are on the question: “what is a regular language in sets with atoms?”. Paper [1] is about orbit-finite monoids, and it proves a Schützenberger theorem for them, demonstrating that the structural theory of monoids extends rather smoothly to orbit-finite monoids. Paper [1] is a journal version of

Mikołaj Bojańczyk*Data Monoids.* STACS, 2011 PDF

In the STACS paper above, the terminology is a bit antiquated, because at the time I was not aware of the existence of nominal sets or atoms. Paper [2] studies orbit-finite automata, which are more powerful than finite monoids. In a certain sense, orbit-finite automata are the same thing as register automata of Francez and Kaminski, but the formalism of orbit-finiteness is a bit more flexible, e.g. allowing a Myhill-Nerode theorem and effective minimization. Paper [2] is a journal version of

Mikołaj Bojańczyk, Bartek Klin, Slawomir Lasota 0001*Automata with Group Actions.* LICS, 2011 PDF

which is already aware of nominal sets. I think that maybe an easier to follow description of the topic of [2] is the book mentioned above. Paper [3] continues the study of the Myhill-Nerode theorem, but it does so for a kind of atoms that correspond to timed automata, where the assumptions of paper [2] are not satisfied. Finally, paper [7] gives a database angle on the automata from [2], although it tries to avoid using the word atom in order not to annoy database theorists, including Luc Segoufin.

After studying automata and monoids, we have subsequently moved on to a study of general computation, including a functional programming language in paper [4], an imperative programming language in paper [5], and a study of Turing machines [9]. Some highlights: there is a robust notion of computation for orbit-finite sets, with algorithms that can be (and are implemented, both functional and imperative) implemented on actual computers, although paper [9] shows that Turing machines are not the correct model (e.g. they do not determinize, although proving this requires use of the Cai-Fürer-Immermann construction).

Papers [6,8] study logic in sets with atoms. Paper [6] shows that orbit-finite Boolean operations can be eliminated. Paper [8] asks if there is a fundamental conflict between the finite support condition that underlies sets with atoms, and the need to study infinite objects.

**Attention: **there is a bug in the proof of paper [6]. Namely, Theorem 6.2 is false, a counterexample being obtained using the same CFI-inspired construction as in Theorem III.1 here. However, Tomek Gogacz has proposed in oral communication a modification of Theorem 6.2, which allows one to recover the main Theorem 3.5.

## Leave a Reply