FMT 6: capturing PTime and canonisation

$% \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 this post, we consider the question of the existence of a logic corresponding to PTime more formally, and we relate it to the graph isomorphism problem. This post is loosely based on a chapter of Martin Grohe’s book.

$\newcommand{\Pp}{\mathcal P}$Let $\Ll$ be a logic, i.e., a mapping which associates to each signature $\Sigma$ the set $\Ll[\Sigma]$ of well-formed $\Ll$-sentences over $\Sigma$.

We require $\Ll$ to have decidable syntax, meaning that for every finite signature $\Sigma$, the set $\Ll[\Sigma]$ is decidable, i.e. one can decide whether a given sentence is a well-formed sentence over $\Sigma$.

We say that $\Ll$ captures PTime over a class of structures $\Cc$ if for every signature $\Sigma$ and for every property of $\Pp$ of $\Sigma$-structures, the following conditions are equivalent:

  1. There is a formula $\phi\in\Ll[\Sigma]$ such that $\str A\models \phi$ if and only if $\str A\in \Pp$, for every $\str A\in \Cc$
  2. There is a polynomial-time Turing machine $M$ such that $\textit{encoding}(\str A)\in L(M)$ if and only if $\str A\in \Pp$, for every $\str A \in\Cc$,

and moreover, there is an algorithm which given a formula $\phi$ constructs an equivalent polynomial-time Turing machine $M$ which, over $\Cc$, accepts the same structures as $\phi$ (we say that $\Ll$ has effective semantics).

If $\Cc$ is the class of all structures, then we simply say that $\Ll$ captures PTime.

Remark 1. Observe that one could try to take as $\Ll[\Sigma]$ the class of polynomial-time Turing machines which are order-invariant, i.e. whose result does not depend on the chosen encoding of a given $\Sigma$-structure. Then $\Ll$ would form a logic which satisfies all the conditions, except that its syntax is not decidable.

Remark 2. On the other hand, one could define a logic such that $\Ll[\Sigma]$ is simply the set of natural numbers and where the number $n$ is treated as a sentence recognising the $n$-th order-invariant Turing machine over vocabulary $\Sigma$. Then $\Ll$ forms a logic which has decidable syntax, but does not satisfy the condition that one can effectively construct a Turing machine from a given sentence.

The main question is whether there is a logic which captures PTime. This question is motivated by a similar question of Chandra and Harel, who asked whether there is a query language for databases which expresses precisely all PTime queries, buch does not depend on the internal ordering of the database. Gurevich conjectures that there is no logic which captures PTime. This would clearly imply that P≠NP, since there is a logic which captures NP, namely ESO (see this post).

The CFI theorem (see previous post) shows that IFP+C does not capture PTime, since it fails the condition 2. However, IFP+C captures PTime over many classes of structures:

  1. Over linearly-ordered structures (Immerman-Vardi theorem),
  2. Over the class of all cliques,
  3. Over the class of all trees,
  4. Over the class of all planar graphs [Grohe],
  5. Over the class of all graphs excluding a fixed minor $K_n$ [Grohe, described in his book].

A natural idea would be to show that IFP+C can define a linear ordering over its input, and then apply the Immerman-Vardi theorem to the ordered graph. However, this line is already impossible for cliques.

Excercise. Prove that there is no formula of IFP+C with two free variables, such that $\phi$ defines a linear order on every clique.

Instead of defining a linear order on the input structure, the idea is to produce an ordered copy of the input structure. This is called IFP+C definable canonisation, a notion that will be defined later, which is related to the graph isomorphism problem.

Graph Isomorphism and Canonisation

The Graph Isomorphism Problem (GI) is the decision problem of determining whether two given graphs are isomorphic. Clearly, this problem is in NP, but it is not known to be NP-complete, nor to be in PTime. However, it is known that GI is in PTime when restricted to many classes of graphs, including:

  1. Trees – in linear time [Aho, Hopcroft and Ullman]
  2. Graphs with treewidth bounded by some number $n$ [Courcelle]
  3. Graphs with a quasi-linear order with equivalence classes of size at most $n$ (called colored graphs with bounded color classes) – in NC (polylogarithmic time on a parallel computer)
  4. Planar graphs – in LogSpace [Hopcroft, Tarjan]
  5. Graphs of bounded degree [Luks, involves nontrivial group theory]
  6. Graphs excluding a fixed minor $K_n$ [Ponomarenko]
  7. Graphs excluding a fixed topological minor $K_n$ [Grohe, Marx] – generalizing 1,2,4,5,6.

For each of those classes, there is a PTime canonisation algorithm, i.e. an algorithm which, given a graph $G$, outputs a graph $\textit{can}(G)$ isomorphic to $G$, with the property that $\textit{can}(G)=\textit{can}(H)$ if and only if $G$ and $H$ are isomorhpic.

Example. Here is a canonisation algorithm which works for cliques: given a clique $G$, output the clique with vertices $1,\ldots,n$, where $n$ is the size of $G$.

Exercise. Find a canonisation algorithm for trees.

Clearly, the existence of a canonisation algorithm over a class $\Cc$ implies that GI is in PTime over the class $\Cc$. It is an open problem whether the converse implication also holds.

Remark 3. The existence of a canonisation algorithm over a class $\Cc$ also implies that there is a logic $\Ll$ which captures PTime over $\Cc$. The sentences of $\Ll[\Sigma]$ are formulas of IFP+C over $\Sigma\cup\set{<}$. The semantics of such a sentence is $\phi$ is defined as follows: a given structure $\str A$ satisfies $\phi$ if   $\textit{can}(\str A)$ satisfies $\phi$. This logic satisfies all the requirements of the definition of capturing PTime. One can say that the semantics is not very natural, since it refers to an external algorithm. Note that the results mentioned earlier say that the arguably more natural logic IFP+C (without an additional linear order) captures PTime over some classes.

Definable canonisations

We say that a transduction $\Theta(\bar x)$ canonises a structure $\str A$ if for every (and for at least one) $\bar x$ in the domain of $\Theta$, the structure $\Theta(\str A,\bar x)$, is an ordered copy of $\str A$. We say that the formula $\Theta(\bar x)$ canonises a class $\Cc$ if it canonises every structure in that class $\Cc$.

Example. The class of cycles admits an IFP+C-definable canonisation.

Proposition. Suppose that $\Cc$ admits an IFP+C-definable canonisation. Then IFP+C captures PTime over $\Cc$.

Proof. Use Immerman-Vardi over the ordered copy.$\square$

Color Refinement and the Weisfeiler-Lehman algorithm

The original algorithms from the items 2-7 in the list above use quite complicated and divert. It turns out that there is a single family of simple algorithms which covers all the cases 2-6, however, proving that one of those algorithm works is a very nontrivial feat.

The color refinement algorithm starts with a graph $G$, and proceeds in rounds, by partitioning its node set (a partition can be thought of as a coloring, where each part gets the same color). Initially, all nodes get the same color, and in each round, two nodes of the same color get different colors if have a different number of neighbours of some color $c$. After a finite number of steps, the partition stabilizes; the result is called the stable coloring.

Color refinement can be applied to a pair of graphs $G,H$, by applying it to their disjoint union. If in the resulting stable coloring, some color appears more times in one graph than in the other, than we say that color refinement disinguishes the two graphs. We say that a graph is identified by color refinement if it is distinguished from any graph which is not isomorphic to it.

Example. Color refinement distinguishes the tree -<== from —<=.

Example. Color refinement distinguishes two graphs of different sizes.

Example. Color refinement identifies all trees from each other.

Theorem (Babai, Erdős, Selkow). Color refinement identifies almost all graphs: a randomly chosen graph with $n$ vertices is identified with probability converging to $1$ as $n$ tends to infinity.

Example. Color refinement does not distinguish a cycle from the disjoint union of two cycles.

Example. Color refinement does not distinguish between two 3-regular graphs of the same cardinality.


Theorem (Immerman and Lander).  Let $G,H$ be graphs. Then color refinement does not distinguish $G$ and $H$ if and only if $G$ and $H$ are $\Cc^2_{\omega,\infty}$-equivalent.

Proof sketch. For the left-to-right implication, we use the bijective $2$-pebble game as characterising $\Cc^2_{\omega,\infty}$-equivalence (see this post).

For the right-to-left implication, for each $n$ and for each color class $C$ of the $n$-th step of the color refinement algorithm, we define a formula $\phi_n^C(c)$ which defines the color class $C\cap V(G)$. $\square$.


The $k$-dimensional Weisfeiler-Lehman algorithm is a generalization of the color refinement algorithm. For a given graph $G$, let $G^k$ denote the structure whose nodes are $k$-tuples of vertices of $G$, and with $k$ binary relation symbols – for each $i\in\set{1,\ldots,k}$, a binary $i$-neighboring relation which connects two $k$-tuples if and only if they differ only on the $i$-th coordinate. The $k$-dimensional Weisfeiler-Lehman algorithm ($k$-WL for short) on a graph $G$ proceeds as color refinement on the structure $G^k$, with the modification that initially two tuples get the same color iff they are isomorphic, and in each step we distinguish two nodes if they have a different number of $i$-neighbors for some $i$. We can apply the $k$-dimensional WL algorithm to a pair of graphs, as before.

Theorem (Cai, Fürer, Immerman). Let $k\in\NN$ and let $G,H$ be graphs. Then $k$-WL does not distinguish $G$ and $H$ if and only if $G$ and $H$ are $\Cc^k_{\omega,\infty}$-equivalent.

The proof is essentially the same as of the previous result.

Corollary. Let $\Cc$ be a class of graphs which admits IFP+C-definable canonisation. Then there is a number $k$ such that $k$-WL identifies all graphs in $\Cc$.

Corollary. $k$-WL does not distinguish the graphs obtained from the structures defined in the CFI construction (in this post).

Universal logic capturing PTime

Consider the following logic $\Ll$. The sentences of $\Ll[\Sigma]$ consist of three components:

  • A polynomial $p$,
  • A Turing machine $M$ accepting encodings of $\Sigma$-structures
  • A proof $\gamma$ of ZFC that the machine $M$ is order-invariant.

This logic has decidable syntax, since checking whether a given proof is a valid ZFC proof can be done effectively (even in PTime). The semantics of a tuple $(p,M,\gamma)$ is defined so that a structure $\str A$ is accepted if and only if $M$ accepts $\str A$ in at most $p(n)$ steps (where $n=|\str A|)$. We call this logic the universal logic for PTime.

Clearly, the semantics is effective, i.e., given a sentence $(p,M,\gamma)$ one can effectively construct a polynomial-time Turing machine equivalent to it. Does this logic capture PTime? At first sight it seems so. The only catch is the following question.

Question. Is it the case that for every PTime property of finite structures $\Pp$ there exists a Turing machine $M$ such that $M$ is provably order-invariant?

In other words, are there properties of finite structures decidable in polynomial time, but which are not provably so? One can ponder about the original motivation for the question about a logic for PTime: who cares about properties of databases which are defined by a PTime algorithm which is order-invariant, but not provably so?

If Question has a positive answer, then the logic proposed above is a logic which captures PTime. The converse is also true, under a reasonable proviso:

Proposition. Suppose that there is a logic which provably captures PTime, i.e., there is a proof (in ZFC) that this logic does indeed capture PTime. Then Question has a positive answer. In particular, if there is a logic which provably captures PTime, then also the universal logic provably captures PTime.

Proof: exercise.$\square$

Reassuming, the existence for a logic capturing PTime essentially boils down to the question above, about provably order-invariant Turing machines. How could one prove that the question has a positive answer?

Conjecture. The following conditions are equivalent for a class of structures $\Cc$:

  1. $\Cc$ admits a PTime canonisation algorithm,
  2. There is a logic capturing PTime over $\Cc$.


  1. Prove the theorem of Immerman and Lander.
  2. Show that $k$-WL is indeed a polynomial time algorithm.

Leave a Reply

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

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>