Certified Split Windows for Parallel Lexing: Recovering Boundaries Where No Byte Certifies
2026-08-10 • Formal Languages and Automata Theory
Formal Languages and Automata TheoryDistributed, Parallel, and Cluster ComputingProgramming Languages
AI summaryⓘ
The authors studied how a parallel lexer (a tool that breaks down text into tokens) can split input safely without changing the order of tokens. They improved previous methods by allowing the split to happen over a short sequence of bytes rather than just one, making the process more flexible and reliable. They created a mathematical model to prove when and where such splits can happen and tested it on many token sets, showing it works well without errors. Their approach analyzes the lexer's behavior using only its internal tables, not the input text itself.
lexertokenizationparallel processingsplit pointmaximal munchtoken setsautomatonrewindsemantic certificatefinite state machine
Authors
Nicklas Nidhögg
Abstract
A certified split point lets a parallel lexer cut unlexed input at a single byte with the serial token stream provably preserved, but several conventional token sets in the predecessor's controlled study certify no byte once string, comment, or whitespace-run forms are included (arXiv:2608.03473). We generalize from a byte to a bounded window: a byte string after which the position where the current token began is known, regardless of surrounding context. We certify the directly usable form of that recovery: the token covering the window's final byte begins at the reported origin. The certificate is conditional on occurrence and may be vacuous; every applicability figure counts only windows carrying an asserted completely tokenizable occurrence witness. We give a conservative model of a maximal-munch scanner's possible histories across a window, prove it sound, and decide reachability in that model exactly by exhausting a finite quotient of its reachable configurations, so every answer of the unbudgeted procedure is either a certified window with its origin or a proof that the model admits none. Within the stated flat, non-nullable, completely-tokenizable scope, model-positive answers are semantic certificates; negatives are relative to the conservative model, which deliberately refuses some windows a greedy scanner would allow. In a sample of 400 random token sets, 91 of the 95 non-nullable sets certifying no byte gain a witnessed window, with zero inconclusive searches, and every exact-empty row of the predecessor's study gains a witnessed window of two to four bytes. Rewind-stress rows exercised 1,079,392 executions that scanned through the window and contained at least one rewind, with zero disagreements against the shipped scanner. The analysis runs once after automaton construction, using only the compiled tables and no input.