Simulating Logspace-Recursion with Logarithmic Quantifier Depth

Proceedings - Symposium on Logic in Computer Science, pp. 1–13

Abstract

The fixed-point logic LREC=was developed by Grohe et al. (CSL 2011) in the quest for a logic to capture all problems decidable in logarithmic space. It extends FO+C, first-order logic with counting, by an operator that formalises a limited form of recursion. We show that for every LREC=-definable property on relational structures, there is a constant k such that the k-variable fragment of first-order logic with counting quantifiers expresses the property via formulae of logarithmic quantifier depth. This yields that any pair of graphs separable by the property can be distinguished with the k-dimensional Weisfeiler–Leman algorithm in a logarithmic number of iterations. In particular, it implies that a constant dimension of the algorithm identifies every interval graph and every chordal claw-free graph in logarithmically many iterations, since every such graph admits LREC=-definable canonisation.

Authors 4

1. Steffen van Bergerem

   Humboldt-Universität zu Berlin

   Affiliation as printed

   Humboldt-Universität zu Berlin,Berlin,Germany

2. Martin Grohe Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University,Aachen,Germany

3. Sandra Kiefer

   University of Oxford

   Affiliation as printed

   University of Oxford,Oxford,United Kingdom

   University of Oxford (Wellington Square, Oxford OX1 2JD - United Kingdom)

4. Luca Oeljeklaus Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University,Aachen,Germany