Linear equation systems and the search for a logical characterisation of polynomial time

Pakusa, Wied; Grädel, Erich; Otto, Martin; Dawar, Anuj

doi:HT018891125

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

2015 & 2016

Verantwortlichkeitsangabevorgelegt von Diplom-Gymnasiallehrer Wied Pakusa aus Siegburg

ImpressumAachen 2015

Umfang1 Online-Ressource (vi, 173 Seiten) : Diagramme

Dissertation, RWTH Aachen, 2015

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2016

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Grädel, Erich (Thesis advisor) ; Otto, Martin (Thesis advisor) ; Dawar, Anuj (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2015-12-07

Online
URN: urn:nbn:de:hbz:82-rwth-2016-008390
URL: https://publications.rwth-aachen.de/record/567588/files/567588.pdf
URL: https://publications.rwth-aachen.de/record/567588/files/567588.pdf?subformat=pdfa

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Mathematik (frei) ; logic (frei) ; complexity (frei) ; polynomial time (frei) ; linear equation systems (frei)

Thematische Einordnung (Klassifikation)
DDC: 510

Kurzfassung
Die Suche nach einer Logik für Polynomialzeit ist eines der wichtigsten offenen Probleme im Gebiet der Endlichen Modelltheorie.In den letzten Jahren wurden neue Erkenntnisse erzielt durch die Analyse der deskriptiven Komplexität von Problemen aus der (Linearen) Algebra. Gestartet wurden diese Untersuchungen 2007 nach einem Resultat von Atserias, Bulatov und Dawar welches zeigt, dass Fixpunktlogik mit Zählen (FPC) die Lösbarkeit linearer Gleichungssysteme über endlichen Abelschen Gruppen nicht ausdrücken kann. Dieses Ergebnis führte nicht zuletzt zur Definition neuer Kandidaten von Logiken für Polynomialzeit, zum Beispiel von Ranglogik (FPR), welche 2009 von Dawar, Grohe, Holm und Laubner eingeführt wurde. Ein weiterer wichtiger Kandidat ist Choiceless Polynomial Time (CPT), eine Logik die bereits 1999 von Blass, Gurevich und Shelah vorgeschlagen wurde. Diese Arbeit setzt die Suche nach einer Logik für Polynomialzeit fort, geleitet durch die folgenden Fragen. (I) Wie repräsentiert man algorithmische Techniken zum Lösen linearer Gleichungssysteme durch logische Mechanismen (Quantoren, Operatoren)?(II) Auf welchen Strukturklassen kann das Lösbarkeitsproblem für lineare Gleichungssysteme genutzt werden, um Polynomialzeit einzufangen? Zu (I) betrachten wir in Kapitel 3 das Lösbarkeitsproblem für lineare Gleichungssysteme über endlichen Abelschen Gruppen, Ringen und Moduln. Unser Ziel ist die Reduktion auf einfache Bereiche, z.B. auf Körper oder zyklische Gruppen, wobei die Transformationen in Fixpunktlogik definierbar sein soll. Wir zeigen, dass eine Reduktion auf zyklische Gruppen möglich ist für Gleichungssysteme über geordneten Gruppen, Ringen und Moduln, und auch für Systeme über gewissen Klassen kommutativer Ringe. In Kapitel 4 betrachten wir Ranglogik, das heißt die Erweiterung von FPC um Operatoren, die den Rang von Matrizen über endlichen Körper definieren. Unser Hauptergebnis bestätigt eine Vermutung von Dawar und Holm: Rangoperatoren über verschiedenen Primkörpern haben unterschiedliche Ausdrucksstärke. Eine wichtige Folgerung ist, dass Ranglogik, in der ursprünglichen Definition mit einem separaten Rangoperator für jede Primzahl, nicht Polynomialzeit einfängt, und durch die stärkere Logik mit uniformem Rangoperator ersetzt werden sollte.Weiter zeigen wir, dass, ohne Hinzunahme von Zähloperatoren, Matrizenrang nicht durch entsprechende Lösbarkeitsquantoren ausgedrückt werden kann. Zu (II) führen wir in 5 zyklische lineare Gleichungssysteme ein. Solche System sind strukturell einfach, aber dennoch stark genung, um das Cai, Fürer, Immerman Problem zu kodieren, und damit um FPC von Polynomialzeit zu trennen. Unser Hauptergebnis ist, dass CPT die Lösbarkeit zyklischer Gleichungssysteme ausdrücken kann.In Kapitel 6 benutzen wir dieses Resultat um zu zeigen, dass CPT Polynomialzeit einfängt auf Strukturen mit Abelschen Farben. Dieses Ergebnis löst auch ein offenes Problem von Blass, Gurevich und Shelah: das Isomorphieproblem von multipedes ist definierbar in CPT.

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.

OpenAccess:
PDF PDF (PDFA)
(additional files)