## Definable sets with atoms

${\mathcal Atoms} \ = \ ({\mathbb{N}},=)$

$a, b, c, \ldots$ - denote atoms

${\mathbf Aut}({\mathcal Atoms})$ - all permutations

Examples:

• ${\mathcal Atoms}$
• ${\mathcal Atoms}^{(2)}$ - set of non-repeating pairs of atoms
• $a$ - a single atom

## Set expressions

Examples:

• $\{ x \mid x \in {\mathcal Atoms}\}$
• $\{ (y_1,y_2) \mid (y_1,y_2) \in {\mathcal Atoms}^2, \ y_1 \neq y_2 \}$
• $x$

A set expression can be:

• a variable,
• a formal tuple of set expressions,
• a formal union of set expressions,
• a set-builder expression of the form $$\{ e(\bar{x}\bar{y}) \mid \bar{y}\in{\mathcal Atoms}^n, \ \phi(\bar{x}\bar{y})\}.$$

$\{ \{y_1\} \cup \{y_2\} \cup \{y_3\} \mid (y_1,y_2) \in {\mathcal Atoms}^2, \ y_1 \neq y_2 \wedge y_1 \neq y_3 \wedge y_2 \neq y_3 \}$

Valuation: $\ y_3 \mapsto a$

$\{ S \subseteq {\mathcal Atoms} \mid |S| = 3 , a \in S \}$

## Set expressions

Examples:

• $\{ x \mid x \in {\mathcal Atoms}\}$
• $\{ (y_1,y_2) \mid (y_1,y_2) \in {\mathcal Atoms}^2, \ y_1 \neq y_2 \}$
• $x$

A set expression can be:

• a variable,
• a formal tuple of set expressions,
• a formal union of set expressions,
• a set-builder expression of the form $$\{ e(\bar{x}\bar{y}) \mid \bar{y}\in{\mathcal Atoms}^n, \ \phi(\bar{x}\bar{y})\}.$$

## Orbit-finiteness

${\mathbf Aut}({\mathcal Atoms})$ acts on a set with atoms by atom renaming.

Fact. Every definable set with atoms has finitely many orbits under the action of ${\mathbf Aut}({\mathcal Atoms})$.

Examples:

• ${\mathcal Atoms}$ - one orbit
• ${\mathcal Atoms}^{2}$ - two orbits $\ \ \ (a,b) \mapsto (c,d) \ \ (a,a) \mapsto (d,d)$
• ${\mathcal P}({\mathcal Atoms})$ - infinitely many orbits (not definable)
• ${\mathcal P}_{fin}({\mathcal Atoms})$ - infinitely many orbits (not definable)

## Context

• Fraenkel-Mostowski set theory (1922)
• Nominal sets [Gabbay and Pitts]

 Alphabet: ${\mathcal Atoms}$ States: $\{\top, \bot \} \cup {\mathcal Atoms}$ Transitions: $\{ (\bot, a, a), (a,b,a), (a,a,\top) \mid (a,b) \in {\mathcal Atoms}^2 \}$

## Definable automata

[Bojańczyk, Klin, Lasota]

Determinization fails

Minimisation works (syntactic automaton)

Emptiness is decidable (PSPACE-complete)

"some letter appears twice"

Powerset construction does not work.

## Other models

Definable pushdown systems - reachability is decidable [Murawski, Ramsay, Tzevelekos].

Definable Petri nets - reachability is open.

Definability over different atoms.

## TM with atoms

Alphabet: ${\mathcal Atoms}^{(2)}$

States: $\{I,A,R\} \cup {\mathcal Atoms}^{(2)}$

Turing machine with atoms is a Turing machine whose alphabet, state space, and transition relation are definable sets with atoms.

## Standard alphabets

An alphabet $\mathcal{A}$ is standard iff every language $\mathcal{L}$ over $\mathcal{A}$ recognisable by a nondeterministic TMA is recognisable by some deterministic TMA.

Theorem [Bojańczyk, Klin, Lasota, Toruńczyk]. There exists a non-standard alphabet.

Backtracking does not work.

No definable function

from $\{ \{a,b \} \mid (a,b) \in {\mathcal Atoms}^2 \}$ to ${\mathcal Atoms}$.

Theorem [Klin, Lasota, O., Toruńczyk]. It is decidable if an alphabet $\mathcal{A}$ is standard.

$\{(a,c,e),(a,d,f),(b,c,f),(b,d,e)\}$

## Standard alphabets

An alphabet $\mathcal{A}$ is standard iff every language $\mathcal{L}$ over $\mathcal{A}$ recognisable by a nondeterministic TMA is recognisable by some deterministic TMA.

Theorem [Bojańczyk, Klin, Lasota, Toruńczyk]. There exists a non-standard alphabet.

Backtracking does not work.

No definable function

from $\{ \{a,b \} \mid (a,b) \in {\mathcal Atoms}^2 \}$ to ${\mathcal Atoms}$.

Theorem [Klin, Lasota, O., Toruńczyk]. It is decidable if an alphabet $\mathcal{A}$ is standard.

## Quest for logic for PTime

 Logic Expresses Fails to express FO "there is a loop" "there is a path from $p$ to $q$" Datalog "there is a path from $p$ to $q$" $2$-colorability LFP $2$-colorability evenness LFP+counting evenness ?

Question: Is there a logic that expresses exactly PTime properties of graphs?

## Alphabets of graphs

${\mathcal A} = \{ (\{a,b,c,d\},\{(a,c),(b,d)\}) \mid (a,b,c,d) \in {\mathcal Atoms}^4, \ \phi(a,b,c,d) \}$

Each alphabet of graphs ${\mathcal A}$ gives rise to a computational problem ${\mathcal{I}_{\mathcal A}}$ - isomorphism of "patched" graphs.

## The power of LFP+C

Theorem [Furst, Hopcroft, Luks]. Each problem ${\mathcal{I}_{\mathcal A}}$ is solvable in PTime (bounded color classes).

Theorem [Klin, Lasota, O., Toruńczyk]. The problem ${\mathcal{I}_{\mathcal A}}$ is expressible in LFP+C iff $\mathcal A$ is standard.

Corollary [Cai, Fürer, Immerman]. LFP+C does not capture PTime.

Key observation: Over "patched" graphs LFP+C = polynomial time (deterministic) TMAs.

## Choiceless polynomial time

Question: Does CPT express all PTime properties of graphs?

"Easier" question: Does it express the isomorphism problem on graphs with bounded colour class size, i.e., ${\mathcal{I}_{\mathcal A}}$ for any $\mathcal A$?

(Over "patched" graphs LFP+C = polynomial time deterministic TMAs.)

Idea: Allow some kind of nondeterminism in TMA to capture CPT over "patched" graphs.

 Vertices: ${\mathcal Atoms}^{(2)}$ Edges:$\{ \{(a,b),(b,c)\} \mid (a,b,c) \in {\mathcal Atoms}^3, \phi(a,b,c) \}$

## Constraint satisfaction problem

Problem: CSP$(\mathbb{B})$

Input: structure $\mathbb{A}$ (over the same signature)

Decide: Is there a homomorphism from $\mathbb{A}$ to $\mathbb{B}$?

## Linear equations mod $2$

$\mathbb{B} = \bigl( \{0,1\}, R_1, R_0 \bigr)$

$R_0 = \{ (x,y,z) \in \{0,1 \}^3 \ | \ x+y+z=0 \mbox{ mod } 2\}$

$R_1 = \{ (x,y) \in \{0,1 \}^2 \ | \ x+y=1 \mbox{ mod } 2\}$

\begin{align*} x+y+z=0 \\ x+y=1 \end{align*}

$\mathbb{A} = \bigl( \{x,y,z\}, R_0(x,y,z), R_1(x,y) \bigr)$

## $3$-SAT

$\mathbb{B} = \bigl( \{0,1\}, R_{000}, R_{100}, R_{110}, R_{111} \bigr)$

$R_{000} = \{0,1 \}^3 \setminus \{(0,0,0) \}$

$R_{100} = \{0,1 \}^3 \setminus \{(1,0,0) \}$

$R_{110} = \{0,1 \}^3 \setminus \{(1,1,0) \}$

$R_{111} = \{0,1 \}^3 \setminus \{(1,1,1) \}$

\begin{align*} \neg x \wedge y \wedge z \end{align*}

$\mathbb{A} = \bigl( \{x,y,z\}, R_{100}(x,y,z) \bigr)$

## Definable CSP

Problem: CSP$_{inf}(\mathbb{B})$

Input: definable structure $\mathbb{A}$ (over the same signature)

Decide: Is there a homomorphism from $\mathbb{A}$ to $\mathbb{B}$?

Theorem [Klin, Lasota, O., Toruńczyk]. There exists a definable structure $\mathbb{B}$ for which the problem Hom$(\mathbb{B})$ is undecidable.

## Definable linear equations mod $2$

\begin{align*} x_{ab} + x_{ba} &= 1, \mbox{ wherea$and$b$are distinc} \\ x_{ab}+x_{bc}+x_{ca} &=0, \mbox{where$a$,$b$and$care distinct} \end{align*}

## Definable CSP

Problem: CSP$_{inf}(\mathbb{B})$

Input: definable structure $\mathbb{A}$ (over the same signature)

Decide: Is there a homomorphism from $\mathbb{A}$ to $\mathbb{B}$?

Theorem [Klin, Lasota, O., Toruńczyk]. There exists a definable structure $\mathbb{B}$ for which the problem CSP$_{inf}(\mathbb{B})$ is undecidable.

## Complexity

Theorem [Klin, Kopczyński, O., Toruńczyk]. For a finite structure $\mathbb{B}$, if CSP$(\mathbb{B})$ is C-complete, then CSP$_{inf}(\mathbb{B})$ is Exp(C)-complete.

Corollary. $3$-colorability of definable graphs is NEXP-complete.

Open problem: Is it decidable, given two definable relational structures, whether they are isomorphic?