Linear equation systems and the search for a logical characterisation of polynomial time
- Lineare Gleichungssysteme und die Suche nach einer Logik für Polynomialzeit
Pakusa, Wied; Grädel, Erich (Thesis advisor); Otto, Martin (Thesis advisor); Dawar, Anuj (Thesis advisor)
Aachen (2015, 2016)
Dissertation / PhD Thesis
Dissertation, RWTH Aachen, 2015
The search for a logic which captures polynomial time is one of the most important challenges in finite model theory. During the last years, significant new insights were obtained by the systematic study of the descriptive complexity of queries from (linear) algebra. These investigations were initiated in 2007 by a striking result of Atserias, Bulatov, and Dawar, who showed that fixed-point logic with counting (FPC) cannot define the solvability of linear equation systems over finite Abelian groups.Their result triggered the development of new candidates for capturing polynomial time, for instance of rank logic (FPR), which was introduced by Dawar, Grohe, Holm, and Laubner in 2009. Before that, only few other candidates had been proposed, of which certainly the most important one is Choiceless Polynomial Time (CPT), developed by Blass, Gurevich, and Shelah in 1999. This thesis continues the search for a logic capturing polynomial time in the light of the following leading questions.(I) How can the algorithmic principles for solving linear equation systems be captured by logical mechanisms (such as operators or quantifiers)? (II) Are there interesting classes of structures on which the solvability of linear equations systems can be used to capture polynomial time?Ad (I), we study in Chapter 3 the inter-definability of linear equation systems over finite Abelian groups, rings, and modules.Our aim is to transform linear equation systems over these algebraic domains into equivalent linear equation systems over simpler domains, such as fields, or cyclic groups, via a reduction which is definable in fixed-point logic.For linear equation systems over ordered Abelian groups, rings, and modules, and also for certain interesting classes of unordered commutative rings, we obtain a reduction to cyclic groups. Moreover, we establish a reduction to commutative rings for the general case.In Chapter 4, we study rank logic (FPR), which extends FPC by operators to compute the rank of definable matrices over finite fields. Our main result validates a conjecture of Dawar and Holm: rank operators over different prime fields have incomparable expressive power. An important consequence is that rank logic, in the original definition with a distinct rank operator for every prime, fails to capture polynomial time, and should be replaced by a more powerful version with a uniform rank operator. We further show that, in the absence of counting, solvability quantifiers are weaker than rank operators.Ad (II), we introduce in Chapter 5 a class of linear equation systems, so called cyclic linear equation systems, which are structurally simple, but general enough to describe the Cai-Fürer-Immerman query, and thus separate FPC from polynomial time.Our main result is that CPT can express the solvability of cyclic linear equation systems.In Chapter 6, we use this definability result to show that CPT captures polynomial time on structures with Abelian colours, a class containing many of the known queries which separate FPC from polynomial time.Our result further solves an open question of Blass, Gurevich, and Shelah: the isomorphism problem for multipedes is definable in CPT.