Mikołaj Bojańczyk

July 14, 2015

Mikołaj Bojańczyk, Laurent Braud, Bartek Klin, Slawomir Lasota

*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

*Modelling Infinite Structures with Atoms.*WoLLIC, 2013 PDFMikołaj Bojańczyk, Bartek Klin, Slawomir Lasota, 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. I am very slowly writing a book on this, although progress has recently stalled. 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, but we have subsequently moved on to a study of general computation, including a functional programming language in paper [1], an imperative programming language in paper [2], and a study of Turing machines [5]. Some highlights: there is a robust notion of computation for orbit-finite sets, with algorithms that can (and are) implemented on actual computers, although paper [5] 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 [3,4] study logic in sets with atoms. Paper [3] shows that orbit-finite Boolean operations can be eliminated. Paper [4] 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 [3]. 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