Locality from Circuit Lower Bounds

International audienceWe study the locality of an extension of first-order logic that captures graph queries computable in AC0 , i.e., by families of polynomial-size constant-depth circuits. The extension considers first-order formulas over relational structures which may use arbitrary numerical predicates in such a way that their truth value is independent of the particular interpretation of the numerical predicates. We refer to such formulas as Arb-invariant first-order. We consider the two standard notions of locality, Gaifman and Hanf locality. Our main result gives a Gaifman locality theorem: An Arb-invariant first-order formula cannot distinguish between two tuples that have the same neighborhood up to distance (log n) c , where n represents the number of elements in the structure and c is a constant depending on the formula. When restricting attention to string structures, we achieve the same quantitative strength for Hanf locality. In both cases we show that our bounds are tight. We also present an application of our results to the study of regular languages. Our proof exploits the close connection between first-order formulas and the complexity class AC0 , and hinges on the tight lower bounds for parity on constant-depth circuits