% IMPORTANT: The following is UTF-8 encoded. This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.
@PHDTHESIS{Schalthfer:780280,
author = {Schalthöfer, Svenja},
othercontributors = {Grädel, Erich and Dawar, Anuj},
title = {{C}hoiceless computation and logic},
school = {RWTH Aachen University},
type = {Dissertation},
address = {Aachen},
reportid = {RWTH-2020-00549},
pages = {1 Online-Ressource (182 Seiten) : Illustrationen},
year = {2019},
note = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
University 2020; 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.},
cin = {117220 / 110000},
ddc = {510},
cid = {$I:(DE-82)117220_20140620$ / $I:(DE-82)110000_20140620$},
typ = {PUB:(DE-HGF)11},
doi = {10.18154/RWTH-2020-00549},
url = {https://publications.rwth-aachen.de/record/780280},
}