Continuing the Quest for a Logic Capturing Polynomial Time – Potential, Limitations, and Interplay of Current Approaches
Moritz Lichter
Die Suche nach einer Logik für Polynomialzeit (PTIME) ist eine zentrale Frage der endlichen Modelltheorie und der deskriptiven Komplexitätstheorie: Gibt es eine vernünftige Logik, die genau die in Polynomialzeit entscheidbaren Eigenschaften endlicher relationaler Strukturen, z.B. endlicher Graphen, definiert? Diese Arbeit setzt die Suche fort und betrachtet alle derzeitigen Ansätze und Kandidaten für solche Logiken. Wir untersuchen und vergleichen deren Ausdrucksstärke, zeigen Limitierungen und studieren deren Kombination und Beziehungen zueinander. Wir tragen folgende neue Ergebnisse bei:
Wir zeigen zuerst, dass die Quantorentiefe, die in Logik erster Stufe mit 3 Variablen und Zählen benötigt wird, um zwei n-elementige Strukturen zu unterscheiden, in O(n log n) ist. Dies ist äquivalent dazu, dass der 2-dimensionale Weisfeiler-Leman Algorithmus nach O(n log n) Iterationen stabilisiert. Diese obere Schranke entspricht der bekannten Ω(n) unteren Schranke bis auf einen logarithmischen Faktor.
Wir betrachten zweitens die Logik Choiceless Polynomial Time (CPT). Diese Logik drückt alle wahlfreien Polynomialzeit-Berechnungen auf relationalen Strukturen aus. CPT ist ein vielversprechender Kandidat für eine Logik für PTIME. Wir untersuchen die logische Charakterisierung von PTIME auf Klassen von Strukturen. Dies zeigt man meistens durch das Definieren einer Kanonisierung. Wir zeigen, dass CPT für Strukturen mit beschränkter Farbklassengröße, für welche jede Farbklasse eine Diedergruppe als Automorphismengruppe induziert, eine Kanonisierung definiert. Diese basiert auf einer neuen Normalform und einer Klassifizierung spezieller subdirekter Produkte von Diedergruppen.
Wir kombinieren drittens zwei verschiedene Ansätze: Wir erweitern CPT um bezeugte symmetrische Wahl (CPT+WSC). Dieser eingeschränkte Wahlmechanismus garantiert, dass das Ergebnis einer CPT-Berechnung immer unabhängig von den getroffenen Wahlen ist. Auch wenn Kanonisierung der übliche Weg ist, um PTIME zu charakterisieren, ist es unbekannt, ob Kanonisierung definierbar sein muss. Wir zeigen, dass in CPT+WSC ein definierbarer Isomorphietest eine definierbare Kanonisierung impliziert. Wenn Isomorphie für eine Klasse von Strukturen in Polynomialzeit entscheidbar ist, dann ist in CPT+WSC das Charakterisieren von PTIME äquivalent zum Definieren von Isomorphie.
Viertens untersuchen wir bezeugte symmetrische Wahl genauer. Ein Beweis, dass bezeugte symmetrische Wahl CPT ausdrucksstärker macht, würde CPT von PTIME trennen, was selbst ein offenes Problem ist. Wir betrachten inflationäre Fixpunktlogik mit Zählen (IFPC), für welche bezeugte symmetrische Wahl die Ausdrucksstärke strikt erhöht. Wir trennen IFPC+WSC von PTIME und zeigen, dass die Erweiterung mit einem Operator basierend auf logischen Interpretationen (IFPC+WSC+I) strikt ausdrucksstärker ist. Also ist bezeugte symmetrische Wahl zu schwach, um PTIME in IFPC zu charakterisieren.
Zuletzt betrachten wir Erweiterungen von IFPC mit Operatoren aus der linearen Algebra. Wir trennen Ranglogik, den zweiten vielversprechenden Kandidaten, von PTIME. Ranglogik erweitert IFPC mit einem Operator, der Ränge über endlichen Körpern definiert. Wir zeigen, dass Ranglogik Isomorphie für eine Klasse von Strukturen nicht definiert, für welche Isomorphie sogar CPT-definierbar ist. Also umfasst Ranglogik nicht einmal CPT. Wir zeigen weiterhin, dass die allgemeinere linear-algebraische Logik dieses Isomorphieproblem ebenso nicht definiert. Diese Logik umfasst jede Erweiterung von IFPC mit linear-algebraisches Operatoren über endlichen Körpern. Folglich ist lineare Algebra über endlichen Körpern zu schwach um PTIME charakterisieren.