Logics with Rank Operators
Anuj Dawar, Martin Grohe, Bjarki Holm, Bastian Laubner · 2009
We introduce extensions of first-order logic (FO) and fixed-point logic (FP) with operators that compute the rank of a definable matrix. These operators are generalizations of the counting operations in FP+C (i.e. fixed-point logic with counting) that allow us to count the dimension of a definable vector space, rather than just count the cardinality of a definable set. The logics we define have data complexity contained in polynomial time and all known examples of polynomial time queries that are not definable in FP+C are definable in FP+rk, the extension of FP with rank operators. For each prime number p and each positive integer n, we have rank operators rkpfor determining the rank of a matrix over the finite field GFpdefined by a formula over n-tuples. We compare the expressive power of the logics obtained by varying the values p and n can take. In particular, we show that increasing the arity of the operators yields an infinite hierarchy of expressive power. The rank operators are surprisingly expressive, even in the absence of fixed-point operators. We show that FO+rkpcan define deterministic and symmetric transitive closure. This allows us to show that, on ordered structures, FO+rkpcaptures the complexity class MODpL, for all prime values of p.