Rank Logic is Dead, Long Live Rank Logic!

Motivated by the search for a logic for polynomial time, we study rank logic (FPR) which extends fixed-point logic with counting (FPC) by operators that determine the rank of matrices over finite fields. While FPR can express most of the known queries that separate FPC from PTIME, nearly nothing was known about the limitations of its expressive power. 
In our first main result we show that the extensions of FPC by rank operators over different prime fields are incomparable. This solves an open question posed by Dawar and Holm and also implies that rank logic, in its original definition with a distinct rank operator for every field, fails to capture polynomial time. In particular we show that the variant of rank logic FPR* with an operator that uniformly expresses the matrix rank over finite fields is more expressive than FPR. 
One important step in our proof is to consider solvability logic FPS which is the analogous extension of FPC by quantifiers which express the solvability problem for linear equation systems over finite fields. Solvability logic can easily be embedded into rank logic, but it is open whether it is a strict fragment. In our second main result we give a partial answer to this question: in the absence of counting, rank operators are strictly more expressive than solvability quantifiers.

Related papers:

title: Logics with Rank Operators
abstract: 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 rk_p for determining the rank of a matrix over the finite field GF_p defined 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+rk_p can define deterministic and symmetric transitive closure. This allows us to show that, on ordered structures, FO+rk_p captures the complexity class MOD_pL, for all prime values of p.

title: The structure of graphs and new logics for the characterization of Polynomial Time
abstract: Descriptive complexity theory is the area of theoretical computer science that is concerned with the abstract characterization of computations by means of mathematical logics. It shares the approach of complexity theory to classify problems on the basis of the resources that are needed to solve them. Instead of computational resources, however, descriptive complexity theory considers the expressiveness necessary for a logic to define classes of problems. Its primary goal is to provide alternative characterizations of computational complexity that give us a way to reason about the strengths and limitations of computational procedures without reference to the underlying machine model. This thesis is making contributions to three strands of descriptive complexity theory. First, we consider an incongruence between machine computations, which receive ordered strings as their input, and logics, whose abstract view on input structures omits the ordering. We show that a combinatorial, singly exponential-time graph canonization algorithm of Corneil and Goldberg (1984) can be extended to edge-colored directed graphs. The algorithm’s input invariance allows us to implement it in the logic Choiceless Polynomial Time with Counting (CPT+C) if we restrict our attention to logarithmic-sized fragments of such graphs. This means that on structures whose relations are of arity at most 2, the polynomial-time (PTIME) properties of logarithmic-sized fragments are precisely characterized by CPT+C. The second contribution investigates the descriptive complexity of PTIME computations on restricted classes of graphs. We present a novel canonical form for the class of interval graphs which is definable in fixed-point logic with counting (FP+C), resulting in FP+C capturing PTIME on this graph class. The methods developed for this result may serve as the foundation for a systematic study of the interrelation of logics and complexity classes on the basis of modular decompositions of graphs. Then we introduce the notion of non-capturing reductions that lead us to a wide variety of graph classes on which computational problems are equally hard to characterize as on the class of all graphs. We finally mold our methods into a canonical labeling algorithm for interval graphs which is computable in logarithmic space (LOGSPACE) and we draw the conclusion that interval graph isomorphism is complete for LOGSPACE. In this way, our methods developed for the logical domain make a contribution to classical complexity theory. In the final part of this thesis, we take aim at the open question whether there exists a logic which generally captures polynomial-time computations. We introduce a variety of rank logics with the ability to compute the ranks of matrices over (finite) prime fields. We argue that this introduction of linear algebra makes for a robust notion of a logic and that it increases the expressiveness of FP+C and many other logics considered in the context of capturing PTIME. By adapting a construction of Hella (1996), we establish that rank logics strictly gain in expressiveness when we increase the number of variables that index the matrices we consider. Rank computations are the first natural operation for which this property is shown in the presence of recursion. Our particular choice of rank computations is justified by showing that most classic problems in linear algebra can either be defined by rank logics or are already definable in FP+C. Then we establish a direct connection to standard complexity theory by showing that in the presence of orders, a variety of complexity classes between LOGSPACE and PTIME can be characterized by suitably defined rank logics. Our exposition provides evidence that rank logics are a natural object to study and establishes the most expressive of our rank logics as a viable candidate for capturing PTIME, suggesting that rank logics need to be better understood if progress is to be made towards a logic for polynomial time.

title: The Quest for a Logic Capturing PTIME
abstract: The question of whether there is a logic that captures polynomial time is the central open problem in descriptive complexity theory. In my talk, I will review the question and the early, mostly negative results that were obtained until the mid 1990s, and then move on to positive results about capturing polynomial time on specific classes of graphs. This will include recent results on definability in fixed-point logic and graph structure theory. Finally, I will dicuss stronger logics and propose directions for further research.The purpose of this accompanying note is to give the basic definitions in detail, state the main results, mention some open problems, and give a list of references.

title: The nature and power of fixed-point logic with counting
abstract: In 1982, Neil Immerman proposed an extension of fixed-point logic by means of counting quantifiers (which we denote FPC) as a logic that might express all polynomial-time properties of unordered graphs. It was eventually proved (by Cai, Fürer and Immerman) that there are polynomial-time graph properties that are not expressible in FPC. Nonetheless, FPC is a powerful and natural fragment of the complexity class PTime. In this article, I justify this claim by reviewing three recent positive results that demonstrate the expressive power and robustness of this logic.

title: An optimal lower bound on the number of variables for graph identification
abstract: It is shown that Omega (n) variables are needed for first-order logic with counting to identify graphs on n vertices. This settles a long-standing open problem. The lower bound remains true over a set of graphs of color class size 4. This contrasts sharply with the fact that three variables suffice to identify all graphs of color class size 3, and two variables suffice to identify almost all graphs. The lower bound is optimal up to multiplication by a constant because n variables obviously suffice to identify graphs on n vertices.<<ETX>>

title: Affine systems of equations and counting infinitary logic
abstract: We study the definability of constraint satisfaction problems (CSPs) in various fixed-point and infinitary logics. We show that testing the solvability of systems of equations over a finite Abelian group, a tractable CSP that was previously known not to be definable in Datalog, is not definable in the infinitary logic with finitely many variables and counting. This implies that it is not definable in least fixed-point logic or its extension with counting. We relate definability of CSPs to their classification obtained from tame congruence theory of the varieties generated by the algebra of polymorphisms of the template structure. In particular, we show that if this variety admits either the unary or affine type, the corresponding CSP is not definable in the infinitary logic with counting.

title: Choiceless Polynomial Time on Structures with Small Abelian Colour Classes
abstract: Choiceless Polynomial Time (CPT) is one of the candidates in the quest for a logic for polynomial time. It is a strict extension of fixed-point logic with counting (FPC) but to date it is unknown whether it expresses all polynomial-time properties of finite structures. We study the CPT-definability of the isomorphism problem for relational structures of bounded colour class size q (for short, q-bounded structures). Our main result gives a positive answer, and even CPT-definable canonisation procedures, for classes of q-bounded structures with small Abelian groups on the colour classes. Such classes of q-bounded structures with Abelian colours naturally arise in many contexts. For instance, 2-bounded structures have Abelian colours which shows that CPT captures Ptime on 2-bounded structures. In particular, this shows that the isomorphism problem of multipedes is definable in CPT, an open question posed by Blass, Gurevich, and Shelah.

title: Definability of linear equation systems over groups and rings
abstract: Motivated by the quest for a logic for PTIME and recent insights that the descriptive complexity of problems from linear algebra is a crucial aspect of this problem, we study the solvability of linear equation systems over finite groups and rings from the viewpoint of logical (inter-)definability. All problems that we consider are decidable in polynomial time, but not expressible in fixed-point logic with counting. They also provide natural candidates for a separation of polynomial time from rank logics, which extend fixed-point logics by operators for determining the rank of definable matrices and which are sufficient for solvability problems over fields. 
 
Based on the structure theory of finite rings, we establish logical reductions among various solvability problems. Our results indicate that all solvability problems for linear equation systems that separate fixed-point logic with counting from PTIME can be reduced to solvability over commutative rings. Further, we prove closure properties for classes of queries that reduce to solvability over rings. As an application, these closure properties provide normal forms for logics extended with solvability operators.

title: On the hardness of graph isomorphism
abstract: We show that the graph isomorphism problem is hard under logarithmic space many-one reductions for the complexity classes NL, PL (probabilistic logarithmic space), for every logarithmic space modular class Mod/sub k/L and for the class DET of problems NC/sup 1/ reducible to the determinant. These are the strongest existing hardness results for the graph isomorphism problem, and imply a randomized logarithmic space reduction from the perfect matching problem to graph isomorphism.

title: Finite model theory
abstract: Finite model theory has its origins in classical model theory but owes its systematic development to research from complexity theory. The text presents the main results of descriptive complexity theory, the connection between axiomatizability of classes of finite structures and their complexity with respect to time and space bounds. The logics that are important in this context include fixed point logics, transitive closure logics and also certain infinitary languages; their model theory is studied in detail. Other topics include DATALOG languages, quantifiers and oracles, 0-1 laws, and optimization and approximation problems. The book is written in such a way that the representative parts on the model theory and descriptive complexity theory may be read independently.

title: Bounded Variable Logics and Counting: A Study in Finite Models
abstract: O. Introduction.- 1. Definitions and Preliminaries.- 2. The Games and Their Analysis.- 3. The Invariants.- 4. Fixed-Point Logic with Counting.- 5. Related Lindstrom

title: Structure and Importance of Logspace-MOD-Classes
abstract: We refine the techniques of Beigel, Gill, Hertrampf [BGH90] who investigated polynomial time counting classes, in order to make them applicable to the case of logarithmic space. We define the complexity classes MODkL and demonstrate their significance by proving that all standard problems of linear algebra over the finite rings Z/kZ are complete for these classes. We then define new complexity classes LogFew and LogFewNL and identify them as adequate logspace versions of Few and LogFew and FewP. We show that LogFew and LogFewNL is contained in MODZkL and that LogFew is contained in MODkL for all k. Also an upper bound for L #L in terms of computation of integer determinants is given from which we conclude that all logspace counting classes are contained in NC2.