Simulating Logspace-Recursion with Logarithmic Quantifier Depth

RWTH Publications (RWTH Aachen)

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

4. Luca Oeljeklaus Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany