Lindell's Critique
Reproduced from this comment
I have worked in finite model theory for quite some time, including some recent related work on monadic fixed points. My comments refer to the August 06, 2010 version (98 numbered pages). The paper is very well written and interesting to read, and I have spent many hours poring over it. It is of particular interest to me because it uses techniques from finite model theory that are similar to my unpublished manuscript [Lin05]. According to what I’ve seen, including the local and global types being kept track of in the ENSP model, ‘factoring through’ a monadic fixed-point is being done correctly.
The concern I have is with the author’s claim that this analysis can be extended to k-ary inductions. Specifically, in the introduction at the bottom of page 8 “Finally, we either do the extra bookkeeping to work with relations of higher arity, or work in a larger structure where the relation of higher arity is monadic…” as well as section 4.3 at the top of page 49 “but the argument we provided was for simple fixed points having one free variable…” amplified upon in point 3 on that same page. A key point in the proof is on page 70 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.” However, the rest of that paragraph goes on to explain that “…we can encode it into a monadic LFP over a polynomially larger product space…”
This construction appears in a recent paper of mine ["A normal form for first-order logic over doubly-linked data structures" IJFCS Vol. 19 No. 1 (Feb. 2008) pp. 205-217] and I think it is useful to refer to the details there in order to understand my specific objections (available on my website). In particular, Definition 3 there explains how to map any k-ary structure into what I called a singulary structure (never mind the terminology, it is just unary predicates and functions). But clearly, when mapping k-tuples into single points, one must preserve the origin of their components by some means, such as the projection functions delineated there. The next section shows that the translation preserves the degree of each node within a polynomial, a fact which is also stated in the paper under consideration.
Even though the successor relation does not significantly change the degree of each node, incorporating it into an LFP in which “the output will be some section of a relation of higher arity…” (as stated on page 71) does. In Appendix A, transitive and simultaneous fixed points are dealt with in a mostly standard way, where each of the individual fixed points are computed in different columns of an induction of wider width. But here’s the problem. The induction relation itself must be monadically encoded, and it may not have bounded degree. In fact, because of successor, it could define an ordering in two of its columns, which would render the Gaifman graph useless. This can be seen most clearly in the aforementioned paper of mine, Figure 1. That diagram illustrates a subsequent sentence stating “But in general, there will be an unbounded number of elements that reference the ground elements, leading to unbounded-degree.”
In short, even though using successor avoids disturbing the diameter of the original structure, I don’t see how circumventing the ordering avoids the problem that a k-ary fixed point could have a diameter one Gaifman graph.
Nevertheless, there are many clever ideas in this purported proof and I would not yet dismiss all hope that it cannot be repaired by some clever means that exploits the specific nature of LFP(<) on SAT such as "… each stage of the LFP is order-invariant." on page 67 (even though this claim appears to hold only for a monadic fixed-point). However, it is my belief that such an analysis will require a new idea in finite model theory. Note that simultaneous inductions (A.2) are not the real problem since the proof can be adapted to deal with multiple monadic fixed points. It is rather the transitivity theorem (A.1). However, since the standard proof of the transitivity theorem uses simultaneous inductions, one would have to find a route which circumvents this, particularly in the case of order. One way to do this might be to re-compute the order every time it is required (similar to a transitive-closure computation) without storing the results. But since this is parameterized, I don’t see a way that it can be done in a purely unary fashion.
