Mikołaj Bojańczyk

Atoms


July 14, 2015
  1. Mikołaj Bojańczyk, Laurent Braud, Bartek Klin, Slawomir Lasota
    Towards nominal computation. POPL, 2012   PDF

  2. Mikołaj Bojańczyk, Szymon Torunczyk
    Imperative Programming in Sets with Atoms. FSTTCS, 2012   PDF

  3. Mikołaj Bojańczyk, Thomas Place
    Toward Model Theory with Data Values. ICALP (2), 2012   PDF

  4. Mikołaj Bojańczyk
    Modelling Infinite Structures with Atoms. WoLLIC, 2013   PDF

  5. Mikoł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

Your email address will not be published.