Choiceless computation and logic

Schalthöfer, Svenja; Grädel, Erich; Dawar, Anuj

doi:HT020343325

Choiceless computation and logic = Auswahlfreie Berechnungsmodelle und Logik

Schalthöfer, Svenja^RWTH*

2019 & 2020

Verantwortlichkeitsangabevorgelegt von Svenja Schalthöfer, M.Sc.

ImpressumAachen 2019

Umfang1 Online-Ressource (182 Seiten) : Illustrationen

Dissertation, RWTH Aachen University, 2019

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2020

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Grädel, Erich (Thesis advisor)^RWTH* ; Dawar, Anuj (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2019-01-24

Online
DOI: 10.18154/RWTH-2020-00549
URL: https://publications.rwth-aachen.de/record/780280/files/780280.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Cai-Fürer-Immerman graphs (frei) ; Finite Model Theory (frei) ; choiceless computation (frei) ; choiceless logspace (frei) ; choiceless polynomial time (frei) ; descriptive complexity (frei) ; fixed point logic (frei) ; logic (frei) ; logspace (frei)

Thematische Einordnung (Klassifikation)
DDC: 510

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.

Choiceless computation emerged as an approach to the fundamental open question in descriptive complexity theory: Is there a logic capturing polynomial time? The main characteristic distinguishing logic from classical computation is isomorphism-invariance. Consequently, choiceless computation was developed as a notion of isomorphism-invariant computation that operates directly on mathematical structures, independently of their encoding. In particular, these computation models are choiceless in the sense that they cannot make arbitrary choices from a set of indistinguishable elements. Choiceless computation was originally introduced by Blass, Gurevich and Shelah in the form of Choiceless Polynomial Time (CPT), a model of computation using hereditarily finite sets of polynomial size as data structures. We study the structure and expressive power of Choiceless Polynomial Time, and expand the landscape of choiceless computation by a notion of Choiceless Logarithmic Space. The unconventional definition of CPT makes it less accessible to established methods. Therefore, we examine the technical aspects of the definition in Chapter 3.An alternative characterisation of CPT is polynomial-time interpretation logic (PIL), a computation model based on iterated first-order interpretations. In Chapter 4, we study the consequences of that characterisation in terms of naturally arising fragments and extensions. In particular, we characterise PIL as an extension of fixed-point logic by higher-order objects, as well as a deterministic fragment of existential second-order logic. Furthermore, we define a fragment of PIL that limits the ability to construct sets to simple sets of tuples, and prove that this fragment is strictly less expressive than full PIL. Towards a deeper understanding of the expressive power of CPT, we apply and extend known methods for its analysis in Chapter 5. The foundation of our investigation is the Cai-Fürer-Immerman query, a graph property that separates fixed-point logic from polynomial time and thus serves as a benchmark for the expressibility of logics within PTIME. As shown by Dawar, Richerby and Rossman, the Cai-Fürer-Immerman (CFI) query is definable in CPT if it is defined starting from linearly ordered graphs, but not while using only sets of bounded rank. We generalise their definability result to preordered graphs with colour classes of logarithmic size, as well as graph classes where the CFI construction yields particularly large graphs. The latter case is definable with sets of bounded rank. Using a novel formalisation of tuple-like objects, we prove that this is, however, not possible using the tuple-based fragment of PIL. Finally, Chapter 6 is dedicated to our model of choiceless computation for logarithmic space. Our logic, called CLogspace, is based on the observation that the size of objects in logarithmic space is sensitive to their encoding. The semantics thus depends on an annotation of sets with varying sizes. We verify that our formalism can be evaluated in logarithmic space, and can be regarded as a model of choiceless computation, as it is included in Choiceless Polynomial Time. Moreover, it is strictly more expressive than previously known logics for logarithmic space.

OpenAccess:
PDF
(additional files)