Computation in sets with atoms


Joanna Ochremiak

Universitat Politècnica de Catalunya


QuantLA, Krippen, 19th September 2016











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:


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:


A set expression can be:

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




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


I ab bc ce A I ab bc R ab bc ce B B ... ab bc ea ce ad B B ... language of "paths"

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









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


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


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