HEXAGONbeta

Sublinear-space recognition for Boolean grammars

Primarily AI-generated textHuman understanding: all partscs.FL — Formal Languages and Automata Theory

Contributed by Will Howe, Grant Huffman, Jensen Kohlmeyer ↗, Liam Kruer

Version 1 / Nov 11, 2026 / CC BY 4.0

Abstract

For every fixed Boolean grammar in the standard language family considered by Okhotin, we give a deterministic membership algorithm using OG(n2/3(log⁡(n+2))2/3)O_G(n^{2/3}(\log(n+2))^{2/3}) working space on an input of length nn. In particular, the whole family is contained in DSPACE⁡(n3/4)\operatorname{DSPACE}(n^{3/4}), answering Okhotin's Problem 4 affirmatively. The construction partitions substring endpoints into blocks of size bb. It represents the parsing recurrence by a constant-fan-in circuit with OG(b2)O_G(b^2)-bit values and dependency height O(n/b+1)O(n/b+1). Splits in the endpoint blocks are resolved locally, and an ordering of the remaining splits controls the height even when a split is highly unbalanced. Applying the Cook–Mertz tree-evaluation algorithm to the implicitly unfolded circuit gives the space bound.

Provenance statement

The mathematical draft and exposition were produced primarily with OpenAI Codex under the direction of the listed contributors. Lean was used for supporting algorithmic and algebraic lemmas; the complete sublinear-space theorem is not yet formally verified. No independent referee acceptance is claimed.

Tools used

OpenAI
Codex
Lean
Lean

References

  1. A. Okhotin, Boolean grammars , Information and Computation 194 (2004), no. 1, 19--48. doi:10.1016/j.ic.2004.03.006 (https://doi.org/10.1016/j.ic.2004.03.006).DOI
  2. A. Okhotin, Nine open problems on conjunctive and Boolean grammars , Bulletin of the EATCS 91 (2007), 96--119. Publisher PDF (https://eatcs.org/images/bulletin/beatcs91.pdf).link
  3. A. Okhotin and C. Reitwießner, Parsing unary Boolean grammars using online convolution , Dagstuhl Seminar Proceedings 10501 (2011), 1--11. doi:10.4230/DagSemProc.10501.3 (https://doi.org/10.4230/DagSemProc.10501.3).DOI
  4. M. Barash and A. Okhotin, Linear-space recognition for grammars with contexts , Theoretical Computer Science 719 (2018), 73--85. doi:10.1016/j.tcs.2017.11.006 (https://doi.org/10.1016/j.tcs.2017.11.006).DOI
  5. J. Cook and I. Mertz, Tree evaluation is in space O(log⁡n⋅log⁡log⁡n)O(\log n\cdot\log\log n) , Proceedings of the 56th Annual ACM Symposium on Theory of Computing (STOC 2024), 1268--1278. doi:10.1145/3618260.3649664 (https://doi.org/10.1145/3618260.3649664).DOI
  6. R. R. Williams, Simulating time with square-root space , Proceedings of the 57th Annual ACM Symposium on Theory of Computing (STOC 2025), 13--23. doi:10.1145/3717823.3718225 (https://doi.org/10.1145/3717823.3718225). Expanded author version, 25 February 2025, arXiv:2502.17779v1 (https://arxiv.org/abs/2502.17779v1) (including Appendix A).arXivDOI
  7. É. Grandjean, T. Grente, and V. Terrier, Context-free, conjunctive and Boolean grammars and SCYK automata , in M.-P. Béal and P. Caron (eds.), Developments in Language Theory (DLT 2026), Lecture Notes in Computer Science 16578 , Springer, 2026, 139--152. doi:10.1007/978-3-032-28404-4_11 (https://doi.org/10.1007/978-3-032-28404-4_11).DOI

Version history

  1. v1 · 6 pagesSubmitted by Jensen KohlmeyerInitial depositCurrentNov 10, 2026