# Orbit-finite CSPs

Consider the following decision problem (for classical Turing machines). Let be a fixed, finite signature.

Input: Two orbit-finite relational structures , over .

Decide: is there a homomorphism from to ?

Question 1. Is the above problem decidable?

Observe that we are not asking for the existence of an equivariant homomorphism. If this were the case, the problem would be clearly decidable, since there are only finitely many equivariant homomorphisms between orbit-finite sets, and they can be effectively scanned. In this problem, the homomorphisms do not even have to be finitely supported! Below is an example where a homomorphism exists, but no finitely supported homomorphism exists.

Example. Consider the equality atoms. Let be the graph whose vertices are pairs of distinct atoms, and in which edges join a pair with its inverse. Let be the -clique. Then maps to , but no finitely supported homomorphism exists.

Following the idea of this post, in order to solve this problem, it might be useful to move to the totally ordered atoms .

Question 2. In the totally ordered atoms, if there is a homomorphism between orbit-finite structures , , is there one which is equivariant?

A positive answer to Question 2 would imply a positive answer to Question 1.

Edit. After reading Bartek’s comment below, I noticed that Question 2 has an even more negative answer. Consider the structures and (orders reversed). There is a homomorphism from to , namely the mapping , but there is none which is finitely supported.

# Classification of standard alphabets

The master thesis of Łukasz Wołochowski continues the study of standard alphabets and classifies  all alphabets of dimension up to 8, with regard to their standardness. Here is the thesis and here is its abstract:

This thesis concerns Turing machines with atoms. There exist alphabets with atoms over which Turing machines do not determinize and a method of alphabet classification is known. In this thesis we show and implement an improved version of this algorithm. The improvement is made by using advanced algorithms from the theory of Constraint Satisfaction Problems, as well as algebraic methods to reduce the size of a problem. As a result, we obtain a classification of all alphabets of dimension 8.

# Orbit-finite systems of linear equations

Consider the following decision problem, over the equality symmetry.

Input: an orbit-finite system of linear equations over Decide: does have a solution (not necessarily finitely-supported)?

Inspired by Eryk’s beautiful solution of this problem, we present another solution, using an amazing theorem from topological dynamics.

# Join of two elements

Let be two elements with atoms. The pair satisfies the following universal property: supports both and , and if is another element with this property, then supports .

We demonstrate the existence of an element denoted , with a dual property: is supported both by and by , and if is another element with this property, then is supported by .  The construction does not require any assumptions on the symmetry.

# Bipartite graphs without bipartite partition

In the equality symmetry, there is a single-orbit graph with the property that is bipartite in the classical sense (equivalently, has no odd-length cycle) but has no partition into two parts which are finitely supported and not inter-connected. In other words, the graph maps to the single-edge graph via a infinitely-supported homomorphism, but not via a finitely-supported one. And here’s the graph: its nodes are pairs of distinct atoms, and there is an edge from to , whenever are distinct atoms. That’s it.

# Cohomology groups of the torus

Čech cohomology  is a way of defining cohomology groups (a topological invariant with algebraic structure) on a topological space. We give a rough description of the construction, in a very special case of a torus, and relate it to the construction of the nonstandard alphabets.  Continue reading

# Uniform bound on the size of support of a witness

Let be an equivariant relation. We show that under a certain assumption on , for every , if there exists a witness such that holds, then there also exists one with small support. We show an application to extending homomorphisms.

# Normalization of pp-formulas

Classicaly,  primitive positive formulas form the smallest fragment of first-order logic which is closed under conjunction and existential quantification. Pp-formulas can be turned in to a normal form – this is due to Skolemization, i.e. the fact that can be turned into . In this case, Skolemization is a consequence of the axiom of finite choice.

We show that in the world with atoms,  not every orbit-finite pp-formula can be converted into an equivalent one in prenex form. This is another demonstration of the failure of the axiom of choice.

This raises the question: what is the appropriate notion of a pp-formula, which does have normal forms?

# Log-standard alphabets

A result of Grädel and McColm shows that over finite structures, the logic DTCL is strictly less expressive than the logic TCL. My question is: can this result be translated into some separation result concerning Turing machines with atoms?

# Characterization of Standard Alphabets

In this paper (accepted to LICS 14) we characterize those alphabets for which Turing machines with atoms determinize.