L-Recursion and a new Logic for Logarithmic Space

TL;DR

This paper introduces LREC, a new logical framework that formalizes limited recursion in logarithmic space, capturing LOGSPACE-complete problems and extending the expressiveness of existing logics.

Contribution

The paper presents LREC, a logic that formalizes recursion in LOGSPACE, and demonstrates its expressive power and limitations compared to other logics like FPC and STC.

Findings

LREC captures LOGSPACE on directed trees.

LREC= captures LOGSPACE on interval graphs.

LREC is more expressive than deterministic transitive closure logic with counting.

Abstract

We extend first-order logic with counting by a new operator that allows it to formalise a limited form of recursion which can be evaluated in logarithmic space. The resulting logic LREC has a data complexity in LOGSPACE, and it defines LOGSPACE-complete problems like deterministic reachability and Boolean formula evaluation. We prove that LREC is strictly more expressive than deterministic transitive closure logic with counting and incomparable in expressive power with symmetric transitive closure logic STC and transitive closure logic (with or without counting). LREC is strictly contained in fixed-point logic with counting FPC. We also study an extension LREC= of LREC that has nicer closure properties and is more expressive than both LREC and STC, but is still contained in FPC and has a data complexity in LOGSPACE. Our main results are that LREC captures LOGSPACE on the class of directed trees and that LREC= captures LOGSPACE on the class of interval graphs.