Choiceless computation and logic

• Auswahlfreie Berechnungsmodelle und Logik

Schalthöfer, Svenja; Grädel, Erich (Thesis advisor); Dawar, Anuj (Thesis advisor)

Aachen (2019, 2020)
Doktorarbeit

Dissertation, RWTH Aachen University, 2019

Kurzfassung

Auswahlfreie Berechnungsmodelle (choiceless computation) entwickelten sich aus der bedeutendsten offenen Frage der deskriptiven Komplexitätstheorie: Gibt es eine Logik für Polynomialzeit? Logiken unterscheiden sich von klassischen Berechnungsmodellen hauptsächlich durch Isomorphieinvarianz. Daraus ergibt sich das Konzept auswahlfreier Maschinen, also isomorphieinvarianter Algorithmen, die, ohne Umweg über eine bestimmte Kodierung, direkt auf mathematischen Strukturen arbeiten. Insbesondere bedeutet Auswahlfreiheit, dass diese Algorithmen aus einer Menge nicht unterscheidbarer Elemente kein beliebiges auswählen können. Auswahlfreie Maschinen wurden erstmals durch Blass, Gurevich und Shelah in Form von Choiceless Polynomial Time (CPT) eingeführt. Dieses Modell basiert auf hereditär endlichen Mengen polynomieller Größe als Datenstrukturen. Wir untersuchen die Struktur und Ausdrucksstärke von Choiceless Polynomial Time, und entwickeln zudem ein neues auswahlfreies Berechnungsmodell für die Komplexitätsklasse Logspace. Seine unkonventionelle Definition erschwert die Analyse von CPT mittels bewährter Methoden. Daher untersuchen wir in Kapitel 3 zunächst die technischen Aspekte der Definition. Eine alternative Darstellung für CPT ist polynomielle Interpretationslogik (PIL), welche auf iterierten FO-Interpretationen beruht. In Kapitel 4 betrachten wir Konsequenzen dieser Darstellung, genauer gesagt einige natürliche Fragmente und Erweiterungen. Insbesondere kann PIL sowohl als Erweiterung höherer Ordnung von Fixpunktlogiken, als auch als deterministische Einschränkung von existentieller Logik zweiter Stufe betrachtet werden. Zudem definieren wir eine Einschränkung von PIL auf die Erzeugung einfacher Mengen von Tupeln, und beweisen dass dieses Fragment in PIL strikt enthalten ist. In Kapitel 5 analysieren wir die Ausdrucksstärke von CPT, indem wir bekannte Methoden anwenden und diese verallgemeinern. Dabei betrachten wir das Cai-Fürer-Immerman-Problem, ein Graphproblem, das Fixpunktlogik von Polynomialzeit trennt und deshalb zur Einordnung von Logiken innerhalb von PTIME verwendet wird. Das Cai-Fürer-Immerman- oder CFI-Problem ist, wie Dawar, Richerby und Rossman zeigten, zwar CPT-definierbar, sofern die Konstruktion von linear geordneten Graphen ausgeht, nicht aber unter Verwendung von Mengen mit beschränktem Rang. Wir verallgemeinern das Definierbarkeitsergebnis auf Präordnungen mit Farbklassen logarithmischer Größe, sowie auf Klassen, für die die CFI-Konstruktion besonders große Graphen ergibt. Im zweiten Fall sind bereits Mengen von beschränktem Rang ausreichend. Eine neuartige Charakterisierung von tupel-artigen Objekten ergibt, dass dies mit dem tupelbasierten \PIL-Fragment nicht möglich ist. Schließlich widmen wir uns in Kapitel 6 unserem auswahlfreien Berechnungsmodell für Logspace. Unsere Logik, abgekürzt CLogspace, fußt auf der Beobachtung, dass die Größe von Objekten in Logspace stark von ihrer Kodierung abhängt. Wir definieren daher eine Semantik basierend auf Mengen mit variablen Größenzuweisungen. Wir weisen nach, dass unser Formalismus in Logspace auswertbar ist, und als Fragment von CPT als auswahlfrei angesehen werden kann. Weiterhin ist die Ausdrucksstärke von CLogspace echt größer als die zuvor bekannter Logiken für Logspace.

Einrichtungen

• Lehr- und Forschungsgebiet Mathematische Grundlagen der Informatik (Logik und Komplexität) [117220]
• Fachgruppe Mathematik [110000]