A Logspace Constructive Proof of L=SL

TL;DR

This paper formalizes Reingold's theorem within bounded arithmetic VL, proving that SL equals L using combinatorial graph expansion reasoning, and resolves an open question about the equivalence of these complexity classes.

Contribution

It provides a formal proof of SL=L in the theory VL, avoiding eigenvalue reasoning by employing combinatorial expansion arguments, and confirms VL=VSL.

Findings

VL proves SL=L using combinatorial methods.

Resolves the open question of VL=VSL.

Formalizes a constructive proof within bounded arithmetic.

Abstract

We formalize the proof of Reingold's Theorem that SL=L [Rei05] in the theory of bounded arithmetic VL, which corresponds to ``logspace reasoning''. As a consequence, we get that VL=VSL, where VSL is the theory of bounded arithmetic for ``symmetric-logspace reasoning''. This resolves in the affirmative an old open question from Kolokolova [Kol05] (see also Cook-Nguyen [NC10]). Our proof relies on the Rozenman-Vadhan alternative proof of Reingold's Theorem ([RV05]). To formalize this proof in VL, we need to avoid reasoning about eigenvalues and eigenvectors (common in both original proofs of SL=L). We achieve this by using some results from Buss-Kabanets-Kolokolova-Kouck\'y [Bus+20] that allow VL to reason about graph expansion in combinatorial terms.