${\mathcal Atoms} \ = \ ({\mathbb{N}},=)$
$a, b, c, \ldots$ - denote atoms
${\mathbf Aut}({\mathcal Atoms})$ - all permutations
Examples:
$\{ \{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 \}$
Examples:
A set expression can be:
${\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})$.
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 \}$ |
[Bojańczyk, Klin, Lasota]
"some letter appears twice"
Powerset construction does not work.
Definable pushdown systems - reachability is decidable [Murawski, Ramsay, Tzevelekos].
Definable Petri nets - reachability is open.
Alphabet: ${\mathcal Atoms}^{(2)}$
States: $\{I,A,R\} \cup {\mathcal Atoms}^{(2)}$
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.
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.
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 | ? |
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.
Question: Does CPT express all PTime properties of graphs?
Vertices: ${\mathcal Atoms}^{(2)}$ |
Edges:$\{ \{(a,b),(b,c)\} \mid (a,b,c) \in {\mathcal Atoms}^3, \phi(a,b,c) \}$ |
Problem: CSP$(\mathbb{B})$
Input: structure $\mathbb{A}$ (over the same signature)
Decide: Is there a homomorphism from $\mathbb{A}$ to $\mathbb{B}$?
$\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\}$
$\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) \}$
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.
$\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*}$
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.
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.