Choiceless computation and logic

• Auswahlfreie Berechnungsmodelle und Logik

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

Aachen (2019, 2020)
Dissertation / PhD Thesis

Dissertation, RWTH Aachen University, 2019

Abstract

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.

Institutions

• Mathematical Fundamentals of Computer Science (Logic and Complexity) Teaching and Research Area [117220]
• Department of Mathematics [110000]