A Logspace Constructive Proof of L=SL
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917081335726080 |
|---|---|
| author | Buss, Sam Dhayal, Anant Kabanets, Valentine Kolokolova, Antonina Mouli, Sasank |
| author_facet | Buss, Sam Dhayal, Anant Kabanets, Valentine Kolokolova, Antonina Mouli, Sasank |
| contents | 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ý [Bus+20] that allow VL to reason about graph expansion in combinatorial terms. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_12011 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Logspace Constructive Proof of L=SL Buss, Sam Dhayal, Anant Kabanets, Valentine Kolokolova, Antonina Mouli, Sasank Logic in Computer Science Logic 03D15, 03F30, 03F35, 68Q15, 68Q10 F.4.1; F.1.1 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ý [Bus+20] that allow VL to reason about graph expansion in combinatorial terms. |
| title | A Logspace Constructive Proof of L=SL |
| topic | Logic in Computer Science Logic 03D15, 03F30, 03F35, 68Q15, 68Q10 F.4.1; F.1.1 |
| url | https://arxiv.org/abs/2511.12011 |