### TRANSDUCERS (SESSION CHAIR: ANCA MUSCHOLL)

#### Emmanuel Filiot: Automata, Logic and Algebra for Word Transductions

This talk will survey old and recent results about word transductions, i.e. functions mapping (finite) words to words. Connections between automata models (transducers), logic and algebra will be presented. Starting with rational functions, defined by (one-way) finite transducers, and the canonical model of bimachines introduced by Reutenauer and Schützenberger, the talk will also target the more expressive class of functions defined by two-way transducers and their equivalent MSO-based formalism.

#### Helmut Seidl: Equivalence of Deterministic Tree-to-String Transducers Is Decidable

Top-down tree-to-string transducers recursively process their structured input data while producing output in an unstructured way, namely as a string. Let yDT denote the class of all deterministic top-down tree-to-string transducers. In the presentation, we show that equivalence of two such transducers is decidable – a problem which has been open for more than 30 years.

As non-equivalence can be witnessed by an input on which the two transducers differ, decidability of equivalence follows if only an effective proof system can be provided for certifying equivalence whenever it holds. We indicate how such a proof system can be constructed using powerful techniques from commutative algebra.

While in general not much is known about the complexity of the decision problem, we also present special cases where polynomial upper bounds can be obtained.

Joint work with Sebastian Maneth (Edinburgh) and Gregor Kemper (München).

### SETS WITH ATOMS (SESSION CHAIR: SŁAWOMIR LASOTA)

#### Szymon Toruńczyk: Towards complexity theory with atoms

I will discuss various classical computational problems, generalized to the setting where the instances are potentially infinite sets with atoms. In particular, we will focus on constraint satisfaction problems, such as 3-colorability, unreachability, Horn-SAT, solvability of systems of linear equations, where the instance is an infinite structure (graph, formula) built out of atoms, with a finite description. It turns out that tight classical complexity results lift to the infinite setting. Moreover, many classical algorithms can be lifted to this setting in a natural way.

#### Eryk Kopczyński and Michał Szynwelski: Programming with atoms (tool demonstration)

A demo presentation of two simple programming languages designed to manipulate infinite, but first-order definable structures, such as the set of all intervals with rational endpoints. One of the languages is implemented as a C++ library, LOIS, by Eryk Kopczyński and Szymon Toruńczyk, while the other as a Haskell module, NLambda, by Bartek Klin and Michał Szynwelski. Internally, infinite sets are represented by logical formulas that define them, whereas an external SMT solver is invoked to check their basic properties.

#### Murdoch James Gabbay: Consistency of Quine’s NF using nominal techniques

Naive set theory has one rule; naive sets comprehension: If φ is a predicate, then {a | φ(a)} is a set. This is inconsistent by Bertrand Russell’s famous observation of 1901 that {a | a ∉ a} ∈ {a | a ∉ a} if and only if {a | a ∉ a} ∉ {a | a ∉ a}. Solutions proposed included Zermelo-Fraenkel set theory, simple type theory, and Quine’s New Foundations (NF).

NF works by restricting comprehension to stratifiable formulae; those in which variables can be assigned ‘levels’, which are natural numbers, such that if a ∈ b occurs and a has level n, then b must have level n+1. Russell’s example is ruled out because a ∉ a cannot be stratified.

Consistency of NF has been an open problem since it was proposed by Quine in 1937. I will present a claimed proof of consistency for Quine’s NF (paper available on my webpage and on arXiv from www.gabbay.org.uk/papers.html#conqnf), exhibiting it as a corollary of a new view of the foundations of logic and computation based on nominal techniques which I have been developing now for several years.