FMT 4: Logics for PSpace and the Abiteboul-Vianu theorem

$% \usepackage{amsmath} % \usepackage{amsfonts} % \usepackage{amssymb} % create the definition symbol \def\bydef{\stackrel{\text{def}}{=}} \newcommand{\qed}{\mbox{ } \Box} \newcommand{\set}[1]{\{#1\}} \newcommand{\eps}{\varepsilon} \newcommand{\NN}{\mathbb N} \newcommand{\Nat}{\mathbb N} \newcommand{\RR}{\mathbb R} \newcommand{\Aa}{\mathcal A} \newcommand{\Bb}{\mathcal B} \newcommand{\Cc}{\mathcal C} \newcommand{\Dd}{\mathcal D} \newcommand{\Ll}{\mathcal L} \newcommand{\str}[1]{\mathbb {#1}} \renewcommand{\implies}{\rightarrow} \newcommand{\lor}{\vee} \newcommand{\land}{\wedge} \renewcommand{\phi}{\varphi} \renewcommand{\subset}{\subseteq} \newcommand{\models}{\vDash} \DeclareMathOperator{\dom}{Dom} \DeclareMathOperator{\ifp}{ifp} \DeclareMathOperator{\lfp}{lfp} \DeclareMathOperator{\gfp}{gfp} \DeclareMathOperator{\tcl}{tcl} \DeclareMathOperator{\ln}{ln} $

In the meantime, we studied Ehrenfeucht-Fraisse games, finite variable logic, k-pebble games and 0-1 laws. The relevant material is in Libkin’s book, in chapters 3, 11.1, 11.2 and 12.

Now we come back to the study of logics capturing known complexity classes.


  • IFP=LFP=PTime over linearly ordered finite structures.
  • ESO=NP over all finite structures (ESO can guess a linear order)
  • TCL=NLogSpace over linearly ordered structures.

What about e.g. LogSpace? We define the logics DTCL and STCL.

Transitive Closure Logics

Theorem. Over linearly ordered structures, DTCL=LogSpace and STCL=SymLogSpace.

SymLogSpace (also called SL) is the class of languages which are log-space reducible to the problem of undirected graph reachability. Equivalently, those are languages accepted by symmetric Turing machines.

In 2004 Omar Reingold showed that undirected graph reachability is in LogSpace. This immediately implies the following.

Theorem. LogSpace=SymLogSpace.

Corollary. Over linearly ordered structures, STCL=DTCL.

The following remains a wide open problem in complexity theory.

Conjecture. LogSpace≠NLogSpace. Equivalently, undirected reachability is not decidable in LogSpace.

This equivalent to saying that DTCL≠TCL over linearly ordered finite structures.

The following results show that restricting to linearly ordered structures really makes the problem much more difficult.

Theorem. (Grädel, McColm) DTCL⊈TCL over all finite structures.

Proof. Excercise.

Fact. LFP,IFP⊊ESO over all structures.

$\newcommand{\ll}{\mathcal L^\omega_{\infty,\omega}}$Indeed, ESO can test whether a pure set has even size. Over pure sets, IFP and LFP are hopeless, since $LFP,IFP⊆\ll$ cannot test parity.

Partial Fixpoint Logic

Consider a relational operator (see this post) $F: P(\str A^k\times Q)\to P(\str A^k\times Q)$. The partial fixpoint of $F$ is defined as $F^n(\emptyset)$ if $n$ is such that $F^n(\emptyset)=F^{n+1}(\emptyset)$, and as $\emptyset$ if no such number $n$ exists. Partial Fixpoint Logic (PFP) is the extension of First Order logic by the partial fixpoint operator, which given a formula $\phi$, constructs the partial fixpoint of the relational operator $F_\phi$ (formally, the logic is defined analogously to LFP, but there is no monotonicity restriction, and partial fixpoints are used instead of least fixpoints).

Theorem. PFP captures PSpace over linearly ordered structures.

Corollary 1. The following conditions are equivalent:

  1. PFP=ESO over linearly ordered finite structures,
  2. NP=PSpace.

Observe that whereas ESO⊆PFP over linearly ordered structures (since NP⊆PSpace), ESO⊈PFP over all finite structures, since again evenness of a pure set cannot be expressed in PFP. Indeed, also PFP⊆$\ll.$ Therefore, it is trivial to separate ESO from PFP over all finite structures, although this separation is not the one that would correspond to the conjecture NP⊊PSpace. This also shows that PFP heavily relies on the linear ordering, unlike ESO, which can guess a linear ordering.

Lemma. IFP,LFP,PFP⊆$\ll$

Corollary 2. The following conditions are equivalent:

  1. LFP=PFP over linearly ordered finite structures,
  2. PTime=PSpace.

One could think that it should be easy to separate PFP from LFP over all finite structures, similarly as it was easy to show IFP⊊ESO, DTCL⊊TCL. This is not the case.

Theorem (Abiteboul-Vianu).  LFP=PFP over all finite structures if and only if PSpace=PTime.

One direction is easy:

If LFP=PFP then this also holds over linearly ordered structures, and hence PTime=PSpace over words, so also PTime=PSpace as normal complexity classes.

The other direction is more difficult. Assuming that PTime=PSpace, we get that LFP=PFP over linearly ordered structures. We want to prove that PFP⊆LFP over all structures.

Fix a relational signature $\Sigma$ and any number $k$ larger than the maximal arity of the symbols in $\Sigma$.

Consider any formula $\phi$ of PFP over $\Sigma$, which uses $k$ variables. We need to show that $\phi$ is equivalent to some formula of LFP over all structures.

Step 1.

Show that LFP can compare types with respect to the much stronger logic $\ll.$ What does that mean? Note that there are infinitely many types, unlike the types of formulas of bounded quantifier rank. $\newcommand{\llk}{\mathcal L^k_{\infty,\omega}}$

If $\bar a,\bar b$ are two $l$-tuples of elements of some structure $\str A$ and if $k\ge l$, let us write $\bar a\sim_k\bar b$ if they satisfy exactly the same formulas of the infinitary logic $\llk$ with $k$ variables.

Fact. The following conditions are equivalent for two $l$-tuples $\bar a,\bar b$ of a structure $\str A$

  1. $\bar a\sim_k \bar b$,
  2. $\bar a$ and $\bar b$ satisfy exactly the same formulas of $FO^k$,
  3. Duplicator wins the $k$-pebble game on $(\str A,\str A)$ with initial configuration $(\bar a,\bar b)$.

Proposition 1. For every $k,l$ (with $l\le k$) the relation $\sim_k$ over $l$-tuples is definable in LFP.

Step 2.

Show that in fact an LFP formula can linearly order the $\sim_k$-equivalence classes of $l$-tuples:

Proposition 2. For every $k,l$ (with $l\le k$) there is a linear quasi-order $\preceq_k$ over $l$-tuples which is definable in LFP, and whose equivalence classes are the equivalence classes of $\sim_k$.

Step 3.

For a given structure $\str A$, using the quasi-linear order $\preceq_k$ define a structure $\str A^*$, which has the following properties:

  1. Its signature $\Sigma^\ast$ depends only on the signature $\Sigma$
  2. Its elements are the equivalence classes of $k$-tuples of elements of $\str A$ with respect to $\sim_k$, so they correspond to configurations in the $k$-pebble game, modulo equivalence.
  3. It is linearly ordered by $\preceq_k$.
  4. It has unary relations encoding the atomic types of the $k$-types
  5. It has binary relations $S_1,\ldots,S_j$, where $S_j$ connects $[\bar a]$ with $[\bar b]$ if the tuples $\bar a$ and $\bar b$ only differ on the $j$-th coordinate.

This allows to recover the properties of the original structure $\str A$, so that the following holds.

Proposition 3. Any sentence $\phi$ of PFP/LFP using $k$ variables can be converted into a sentence $\phi^*$ of PFP/LFP, so that for all $\str A$,

$$\str A\models \phi\quad\iff\quad \str A^*\models \phi^*.$$

Conversely, any sentence $\psi^*$ of PFP/LFP can be converted into a formula $\hat\psi$ of PFP/LFP so that for all $\str A$,

$$\str A^*\models \psi^*\quad\iff\quad \str A\models \hat\psi.$$

As a side note we remark that is not difficult to show the following.

Proposition. $\str A$ and $\str B$ are equivalent with respect to $\llk$ if and only if $\str A^*$ and $\str B^*$ are isomorphic.

Because of this, $\str A^*$ can be seen as a canonical structure with respect to $\llk$-definability.


Let us show how to conclude the proof of the Abiteboul-Vianu theorem.

Suppose that PTime=PSpace and consider a formula $\phi$ of PFP, using $k$ variables. Let be the formula $\phi^*$ of PFP from the last proposition. Since PTime=PSpace, over linearly ordered structures, the formula $\phi^*$ is equivalent to a formula $\psi^*$ of LFP. The formula $\psi^*$ lifts to a formula $\hat\psi$ of LFP. The resulting formula $\hat\psi$ is equivalent to $\phi$ one over any structure $\str A$. This ends the proof of the theorem.

Leave a Reply

Your email address will not be published. Required fields are marked *