Definable sets with atoms

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

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

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

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$

$\{ \{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})$.

Context

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

Definable automata

[Bojańczyk, Klin, Lasota]

"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.

TM with atoms

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

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

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 [Klin, Lasota, O., Toruńczyk]. It is decidable if an alphabet $\mathcal{A}$ is standard.

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

Alphabets of 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?

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}$?

$3$-colorability

$3$-colorability

$3$-colorability

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\}$

$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) \}$

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 $3$-colorability

Definable linear equations mod $2$

$\begin{align*} x_{ab} + x_{ba} &= 1, \mbox{ where $a$ and $b$ are distinc} \\ x_{ab}+x_{bc}+x_{ca} &=0, \mbox{where $a$, $b$ and $c$ are 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.