### 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: SLAWOMIR LASOTA)

#### Szymon Torunczyk: 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 Kopczynski and Michal 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 Kopczynski and Szymon Torunczyk, while
the other as a Haskell module, NLambda, by Bartek Klin and Michal 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.