A Logspace Constructive Proof of L=SL
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.
Cite
@article{arxiv.2511.12011,
title = {A Logspace Constructive Proof of L=SL},
author = {Sam Buss and Anant Dhayal and Valentine Kabanets and Antonina Kolokolova and Sasank Mouli},
journal= {arXiv preprint arXiv:2511.12011},
year = {2025}
}
Comments
39 pages, one figure