arXiv subjects

Nicklas Nidhögg

Publications and source records attributed to Nicklas Nidhögg.

4 recordsLinked to original sources

arXiv2026

Certified Splitting: Decidability and Anchor Supply for Maximal-Munch Tokenization

A certificate is a window of bytes with an origin inside it: wherever the window occurs in a completely tokenizable input, the token covering the window's final byte begins at that origin. Decided from the token set alone, a certified position marks where work may soundly begin. This paper decides certification and reads its anchors forward, into cuts, edits and audits. Certification is decided two ways: online with a completeness cutoff for literal vocabularies, and offline through an armed-run verifier for arbitrary regular token sets. Either route, under a declared window budget, yields the anchor inventory, with a witness on each refusal. The consequences are theorems. Cutting an input at certified anchors and scanning the chunks independently reproduces the sequential segmentation, with no speculation and no fixup pass. A byte substitution that keeps the input tokenizable moves boundaries only strictly between the certified anchors witnessed in the unchanged bytes on either side of it. For tokens of length at most L, an edit at p moves no boundary at or below p - L + 1. A delimiter permits a sound cut before it exactly when it sits only token-initial, and one after it exactly when only token-final, so the embedded-delimiter failure is refused. Two instruments follow: the anchor-free span of a finite certified inventory, decided bounded or not with its exact supremum, three for the UTF-8 shape; and a differential auditor deciding whether two token sets place different boundaries on an input both tokenize, with witnesses. Every theorem carries an executable check. Every measurement is a named program's output or arithmetic on such outputs, each program shipped with the paper or pinned by commit in the library it studies; that library's threaded scanner splits the archived campaign corpus at certified anchors, its boundary stream byte-identical throughout.

cs.FL↗

arXiv2026

Certified Split Points for Parallel Lexing: Exact and Modulo Discarded Tokens

Table-driven DFA lexing is sequential: each transition depends on the previous byte's state. Scanning one input in parallel needs each chunk's entry state, which existing methods recover by simulation, speculation, prescanning, or overlap. We give two conditions under which none is needed. For a longest-match scanner restarting from q0 at every token boundary, a byte b is a certified split symbol when no reachable state other than q0 has a b-transition whose target can reach acceptance, and q0 is not re-entrant if it has one. Every occurrence of such a byte in completely tokenizable input begins a token, so chunks starting there reproduce the serial sequence of kinds and lengths by ordered concatenation. The condition is necessary as well as sufficient, and fragile: one string, comment, or whitespace run can eliminate every useful certificate, and comments and whitespace are usually discarded. We therefore weaken the guarantee to equality after deleting a declared discarded set, and give a second condition, sound and more permissive, coinciding with the first when the discarded set is empty and strictly gaining on suitable pairs of token set and discarded set, but conservative rather than exact, decided from the same tables, answered by a second constant-time one-bit query. It recovers newline for a conventional C-like tokenization and tab, newline and carriage return for JSON, without altering their token definitions, and refuses it where block comments are unrestricted. Splitting at exact certificates in the munch library reaches 92.6-95.3% parallel efficiency at eight threads on a restricted CPU set, on a 512 MiB dense corpus beyond last-level cache, and a 3.46-3.94x end-to-end speedup at four threads, across two benchmark revisions on one machine. It turns delimiter-based parallel lexing from a language-specific assumption into a property a compiler checks.

cs.FL↗

arXiv2026

Certified Split Windows for Parallel Lexing: Recovering Boundaries Where No Byte Certifies

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, 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. A token set in which some token matches the empty string is decided through its positive-width equivalent, the same automaton entered through a start state that does not accept, which changes no scan. In a sample of 400 random token sets, 322 of the 337 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. The analysis runs once after automaton construction, using only the compiled tables and no input.

cs.FL↗

arXiv2026

Certified Panic Mode: Repair-Invariant Error Recovery for Maximal-Munch Lexing

Classical panic-mode recovery skips a failed scan forward by convention: it promises progress, and membership in a designated set where one is found, but no repair-universal boundary guarantee for the position it lands on. This paper chooses the resume position by theorem: a position is a sound recovery point when every prefix repair whose scan commits through the certificate's returned evidence places a token boundary there, complete repairs the special case, by a committed-prefix lemma over certificates posted for a different purpose (arXiv:2608.03473, arXiv:2608.09761). The quantifier is strictly the stronger one, and a dichotomy locates the difference exactly: the inclusion is strict precisely when no repair completes while some scan still commits through the evidence, a two-token witness realizing the case. The evidence-returning form pairs each answer with the interval it rests on, which is what makes the guarantee deployable: a caller who knows what the scanner cannot check decides whether the certified boundary transfers to the clean input it intended. The search is one forward walk in evidence order and provably terminates; the guarantee is per-automaton, relative to the active mode. The procedure ships in the munch lexing library, and a deterministic corruption study measures its recovery quality beside the classical skip-one and delimiter conventions. Every certified answer whose evidence survives the damage passes its executable landing check on every recovery move, 40,885 of 40,885; among first answers, the 5,595 resting on evidence the damage reached land 1,589 times, reported and never asserted. On 13,522 of the 16,808 trials the shipped repair routine labels beyond repair, the resumed suffix tokenizes whole and the two quantifiers provably coincide, so both are empty there if those negative labels are exact; 3,286 stay undetermined.

cs.PL↗