Immerman's letter

What follows is the text of a letter from Neil Immerman to Vinay Deolalikar. It is being posted by Robert Solovay with the express permission of Professor Immerman.

Dear Vinay Deolalikar,

Thank you very much for sharing your paper with me. I find your approach and your ideas fascinating, but I am afraid that there is currently a serious hole in your paper as I now describe. For page numbers, I refer to the 102 page, 12 pt. version of your paper.

Your main idea for the lower bound is to show that FO(LFP) is not powerful enough to express SAT, by using Hanf-Gaifman locality to limit the connectivity of the graphs you consider at successive stages of the fixed point computation. As you point out, if a total ordering is given as part of the input structure, then the Gaifman graph has diameter one, so locality is meaningless. Thus you restrict to a successor relation and as you point out, it is still true that FO(LFP) is equal to P in the presence of a successor relation. However, you make two assertions that are not true.

You use the relation "[math]\displaystyle{ R_E }[/math]" as your successor relation. On page 67 you write, "The reason for the relation [math]\displaystyle{ R_E }[/math] that creates the chain is that on such structures, polynomial time queries are captured by FO(LFP) [EF06, S11.2]. This is a technicality. Recall that an order on the structure enables the LFP computation (or the Turing machine the runs this computation) to represent tuples in a lexicographical ordering. In our problem k-SAT, it plays no further role. Specifically, the assignments to the variables that are computed by the LFP have nothing to do with their order. They depend only on the relation [math]\displaystyle{ R_C }[/math] which encodes the clauses and the relation [math]\displaystyle{ R_P }[/math] that holds the initial partial assignment that we are going to ask the LFP to extend. In other words, each stage of the LFP is order invariant. It is known that the class of order invariant queries is also Gaifman local [GS00]."

Unfortunately, it is not true that each stage of the fixed point must be order invariant. In particular, consider the definition of ordering from successor, easily defined by a least fixed point and thus the reason that successor suffices to capture P. The ordering is defined by taking the transitive closure of the successor relation. At each stage, the successor distance is doubled, so in log n stages we have the whole ordering. Note that all these stages contain the order dependent information that is part of the original successor relation. It is true that the final aim of your computation is the SAT property which is order independent. But that definitely does not imply that each stage of the induction is order independent.

The other problem is that you restrict your attention to monadic fixed points. You write,

"Remark 7.4. The relation being constructed is monadic, and so it does not introduce new edges into the Gaifman graph at each stage of the LFP computation. When we compute a k-ary LFP, we can encode it into a monadic LFP over a polynomially (n^k) larger product space, as is done in the canonical structure, for instance, but with the linear order replaced by a weaker successor type relation. Therefore, we can always chose to deal with monadic LFP. This is really a restatement of the transitivity principle for inductive definitions that says that if one can write an inductive definition in terms of other inductively defined relations over a structure, then one can write it directly in terms of the original relations that existed in the structure [Mos74, p. 16]."

It is not the case that you can freely assume that your fixed points are monadic. If you actually work on the canonical structure, then you require the multiple arity relations that can take us from a tuple to its individual elements and back again. These would again make the diameter of the whole graph bounded. However, in your proof you do not include these relations. Thus, your restriction to only have successor and to restrict to monadic fixed points is fundamental. In this domain -- only monadic fixed points and successor -- FO(LFP) does not express all of P!

Currently, as I see it, the strongest tool we have in descriptive complexity -- rather than the locality theorems -- is the Håstad Switching Lemma. Beame and Håstad used this to shown that Sipser's hierarchy theorem extends all the way to [math]\displaystyle{ FO[\log n/\log \log n] }[/math]. As you know, FO(LFP) is the same thing as [math]\displaystyle{ FO[n^{O(1)}] }[/math] -- properties expressible by the polynomial iteration of a fixed block of restricted quantifiers. We know that [math]\displaystyle{ NC^1 }[/math] is contained in [math]\displaystyle{ FO[\log n/\log \log n] }[/math] and this is tight. Furthermore, L and NL are contained in [math]\displaystyle{ AC^1 = FO[\log n] }[/math], and it remains open whether [math]\displaystyle{ NC^1 }[/math] is equal to NP. A state of the art paper that I very much recommend is Ben Rossman's result that expressing the existence of a k clique requires k/4 variables in FO, and even in [math]\displaystyle{ FO[c\log n/\log \log n] }[/math] for appropriate c. (In Rossman's result, as in all results that use the switching lemma, the lower bound is true in the presence not just of order, but of any numeric relations including addition and multiplication.)

My hope is that work such as yours can get us beyond the [math]\displaystyle{ \log n/\log \log n }[/math] boundary.

I look forward to meeting you and talking with you in person about your work sometime in the future.

Good luck and best wishes,

-- Neil