Author name cluster

Svenja Schalthöfer

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

2 author rows

MFCS Conference 2019 Conference Paper

Choiceless Logarithmic Space

Erich Grädel
Svenja Schalthöfer

One of the most important open problems in finite model theory is the question whether there is a logic characterising efficient computation. While this question usually concerns Ptime, it can also be applied to other complexity classes, and in particular to Logspace which can be seen as a formalisation of efficient computation for big data. One of the strongest candidates for a logic capturing Ptime is Choiceless Polynomial Time (CPT). It is based on the idea of choiceless algorithms, a general model of symmetric computation over abstract structures (rather than their encodings by finite strings). However, there is currently neither a comparably strong candidate for a logic for Logspace, nor a logic transferring the idea of choiceless computation to Logspace. We propose here a notion of Choiceless Logarithmic Space which overcomes some of the obstacles posed by Logspace as a less robust complexity class. The resulting logic is contained in both Logspace and CPT, and is strictly more expressive than all logics for Logspace that have been known so far. Further, we address the question whether this logic can define all Logspace-queries, and prove that this is not the case.

Details

CSL Conference 2016 Conference Paper

Definability of Cai-Fürer-Immerman Problems in Choiceless Polynomial Time

Wied Pakusa
Svenja Schalthöfer
Erkal Selman

Choiceless Polynomial Time (CPT) is one of the most promising candidates in the search for a logic capturing Ptime. The question whether there is a logic that expresses exactly the polynomial-time computable properties of finite structures, which has been open for more than 30 years, is one of the most important and challenging problems in finite model theory. The strength of Choiceless Polynomial Time is its ability to perform isomorphism-invariant computations over structures, using hereditarily finite sets as data structures. But, as it preserves symmetries, it is choiceless in the sense that it cannot select an arbitrary element of a set - an operation which is crucial for many classical algorithms. CPT can define many interesting Ptime queries, including (the original version of) the Cai-Fürer-Immerman (CFI) query. The CFI query is particularly interesting because it separates fixed-point logic with counting from Ptime, and has since remained the main benchmark for the expressibility of logics within Ptime. The CFI construction associates with each connected graph a set of CFI-graphs that can be partitioned into exactly two isomorphism classes called odd and even CFI-graphs. The problem is to decide, given a CFI-graph, whether it is odd or even. In the original version, the underlying graphs are linearly ordered, and for this case, Dawar, Richerby and Rossman proved that the CFI query is CPT-definable. However, the CFI query over general graphs remains one of the few known examples for which CPT-definability is open. Our first contribution generalises the result by Dawar, Richerby and Rossman to the variant of the CFI query where the underlying graphs have colour classes of logarithmic size, instead of colour class size one. Secondly, we consider the CFI query over graph classes where the maximal degree is linear in the size of the graphs. For these classes, we establish CPT-definability using only sets of small, constant rank, which is known to be impossible for the general case. In our CFI-recognising procedures we strongly make use of the ability of CPT to create sets, rather than tuples only, and we further prove that, if CPT worked over tuples instead, no such procedure would be definable. We introduce a notion of "sequence-like objects" based on the structure of the graphs' symmetry groups, and we show that no CPT-program which only uses sequence-like objects can decide the CFI query over complete graphs, which have linear maximal degree. From a broader perspective, this generalises a result by Blass, Gurevich, and van den Bussche about the power of isomorphism-invariant machine models (for polynomial time) to a setting with counting.

Details

Highlights Conference 2014 Conference Abstract

Interpretation Logic: an Alternative Characterisation of Choiceless Polynomial Time

Svenja Schalthöfer

We introduce a characterisation of Choiceless Polynomial Time based on first-order interpretations. Choiceless Polynomial Time with counting (introduced by Blass, Gurevich and Shelah) succeeds to define several queries that separate other logics from PTIME (e. g. the Cai-Fürer-Immerman query) and is thus an interesting candidate for a logic capturing PTIME. Originally, Choiceless Polynomial Time has been formalised as a machine model operating on structures by means of set-theoretic operations, especially creation of hereditarily finite sets. Despite the benefits of viewing the logic as a machine model, this makes it less accessible to model theoretic techniques. Computations in Choiceless Polymomial Time primarily define new relations over hereditarily finite sets. This closely resembles the process of updating relations with first-order interpretations, which suggests a characterisation with iterated first-order interpretations. Representing Choiceless Polynomial Time on the basis of first-order logic not only allows for a more concise definition, it also permits analysis using tools of finite model theory. Moreover, our characterisation makes it easy to define natural fragments of our logic and hence of Choiceless Polynomial Time. A characterisation of these fragments may, in turn, give useful insights into the expressibility of Choiceless Polynomial Time itself. We formalise the idea of iterated first-order interpretations with appropriate polynomial time and space constraints to create Interpretation Logic, a logic that is equivalent to Choiceless Polynomial Time. The main principle of Interpretation Logic is to iterate the application of a first-order interpretation to the input structure, where the halting condition and evaluation are given in first-order logic as well. In order to obtain a representation of the extension of Choiceless Polynomial Time by the counting operation, we show that it suffices to equip our logic with an equicardinality operation, namely, the Härtig quantifier. More precisely, we show that Choiceless Polynomial Time with counting can already be simulated by the extension of Choiceless Polynomial Time by an equicardinality operator. This is possible because Choiceless Polynomial Time programs have access to operations on hereditarily finite sets and thus on finite ordinals. Our main result is the equivalence of this extension of first-order logic by the equicardinality operation and the extension of Interpretation Logic by the Härtig quantifier, where the simulation requires representation of higher-order objects in the interpreted structures as well as a correspondence between different measures of space complexity.

PDF Details