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

1 Introduction

• Over T = {ab, b}, cutting at b splits ab inside its committed token, while a is certified because it occurs only at token offset zero.The example shows why sound cuts require a theorem over all completely tokenizable inputs, not tests where b stands alone.Source: §1 · pp. 1–2
• The paper decides each proposed certificate and exact inventory through a declared budget, then answers recognition, cost, and anchor-supply questions for maximal-munch scanning.Its applications turn the certificate into consequences for safe work division and other uses.Source: §1 · p. 2
• Theorems do not require anchor density, but supply and edit measurements describe named material under named policies, budgets, and seeds.The subword vocabularies are BPE-derived token sets read under maximal munch, not ranked merge procedures.Source: §1 · p. 2
• Earlier work introduced single-byte certificates [27] and bounded-window certificates [28], while this paper adds arbitrary-regular-set decisions, inventories, span analysis, auditing, and measurements.The earlier window work did not decide arbitrary windows or provide an inventory or price.Source: §1 · p. 2

2 Setting

• A literal token set is a finite nonempty collection of nonempty byte strings; maximal munch commits the longest matching prefix, failing when none matches.For regular token sets, equal-length matches are resolved by list priority; a literal set is the singleton-language case.Source: §2 · p. 4
• From any boundary of a completely tokenizable input, scanning the suffix as a new input commits exactly the tokens committed from there onward.The scan has no state beyond its current position, so its choices depend only on the remaining suffix.Source: §2 · p. 4
• A token committed at an earlier boundary ends at or before any later boundary, because committed tokens partition the input.This confines matches relative to boundaries used in subsequent arguments.Source: §2 · p. 4
• A certificate requires that, at every occurrence of its window in every completely tokenizable input, the token covering the final byte begins at the specified origin.This guarantee is sufficient for a sound cut but stronger than merely having a boundary at the origin; the witnessing occurrence is part of an anchor.Source: §2 · p. 4

Online certification

• A violating window of length h exists for a literal token set with maximum token length L iff one exists on an input of length at most N = h+2L−2.The cutoff is attained: for T = {aab} and W = ba, the shortest violating input is aabaab, of length six.Source: §3 · pp. 5–6

Online limitation

• The online scan cannot always emit boundaries irrevocably: for T = {a+b, a}, no fixed lookahead settles whether the first token ends after a or b.Certification still decides in this case by verifying completed segmentations rather than computing them.Source: §3 · p. 6

Offline certification

• For arbitrary regular token sets, a finite armed-run automaton accepts exactly the boundary markings produced by greedy scans, making window certification decidable.The automaton tracks token runs from each marked position; an armed accept later than the segment end witnesses a longer match.Source: §3 · pp. 6–7

Anchor inventories

• A declared window budget H yields a computable inventory of certified pairs for regular token sets, without string enumeration or a cutoff.The construction tests each pair by a union-emptiness problem over the armed-run product.Source: §3 · p. 7

Unrestricted width

• Unrestricted-width certification is decidable via effectively regular languages, but existence is meaningful chiefly for windows occurring in tokenizable inputs because nonoccurring windows certify vacuously.The unrestricted language is closed under left extension; that closure need not preserve whether a window occurs.Source: §3 · pp. 7–8

Anchor-free span

• For a finite certified inventory, boundedness and the exact supremum of anchor-free stretches are decidable; an unanchored-exit cycle characterizes unboundedness.The UTF-8 shape has computed synchronization distance three, while the miniature C-like grammar has no bound because identifiers can be arbitrarily long.Source: §3 · pp. 8–10

Certified cuts

• Scanning chunks between certified anchors and concatenating their segmentations reproduces the sequential scan exactly.The anchors are established from the token set before the input exists, so the cut guarantee applies to every completely tokenizable input.Source: §4 · p. 11

Regular token sets

• The cut-at-boundaries result extends to regular token sets because both scans choose the same longest available token, resolving equal-length ties by the same priority.The proof relies on the scan’s fixed preference optimum, not merely on its dependence on the remaining suffix and partitioning into committed tokens.Source: §4 · p. 11

Edit damage

• After a tokenizable single-byte substitution, every changed boundary lies strictly between certified anchors witnessed in unchanged bytes on either side.If all token words have length at most L, no boundary at or below p − L + 1 can change for an edit at p.Source: §4 · pp. 11–12

Delimiter splitting

• Splitting before each delimiter occurrence is sound iff the delimiter appears only token-initial, and splitting after it is sound iff it appears only token-final.A delimiter embedded at a noninitial or nonfinal token position yields a single-token input on which the corresponding split fails to preserve segmentation.Source: §4 · p. 12

5 The differential auditor

• Theorem 7 decides boundary disagreement on jointly tokenizable inputs and domain difference, computing a witness input whenever either exists.The domain differential is an input tokenized by exactly one set.Source: §5 · p. 13
• For boundary disagreement, a product of armed-run verifiers tracks both true boundary sets and accepts when a flag records a position marked by only one side.Armed pruning rejects guesses outside each set’s greedy segmentation.Source: §5 · p. 13
• For domain difference, determinized byte projections track surviving marking configurations, allowing the search to test non-membership on either side.The subset construction is needed because a nondeterministic product cannot establish that one side rejects.Source: §5 · p. 13
• The auditor checks lexical boundary and tokenization-domain differences, but not token identity when boundaries coincide or priority ties.These predicates address lexer disagreements relevant to request smuggling, polyglot inputs, and log mangling.Source: §5 · p. 13
• The campaign’s conventional and split-friendly grammars differ on SN: the conventional row has boundary set {0}, while the split-friendly row has {0, 1}.The conventional grammar against itself is proved differential-free over every input, not merely a corpus.Source: §5 · p. 13
• Table 2 reports searched space, not running time; the two differential decisions are the only constructions here using a subset construction.Its entries are reachability questions over construction-specific state spaces.Source: §5 · pp. 13–14, Table 2 · p. 14

• Across evaluation blocks, trained-vocabulary supply ranged from 131 to 448 anchors per block (median 242), while external supply ranged from 537 to 756 (median 688).The ranges do not overlap, though each varies enough that a slice-wide aggregate hides block-level spread.Source: §6 · p. 16
• Through H = 4, supply rose to 242.1 anchors per kibibyte for the trained vocabulary and 651.2 for the external vocabulary, without flattening at the budget.Width four added more anchors for the external vocabulary than width three; supply beyond H = 4 was not estimated.Source: §6 · pp. 16–17
• The frozen inventory retained 209.4 of 242.1 anchors per kibibyte for the trained vocabulary and 608.6 of 651.2 for the external vocabulary.These held-out values are 86.5% and 93.5% of their respective ceilings on one adjacent-slice transfer, not guarantees.Source: §6 · p. 17
• The sixty sampled n-gram candidates yielded 57.8 anchors per kibibyte for the trained vocabulary versus its exhaustive 242.1, and 427.4 versus 651.2 for the external vocabulary.The trained vocabulary’s sampled total was nearly all supplied by certified bytes; the external vocabulary’s sampled pairs overlapped heavily with its certified-byte positions.Source: §6 · pp. 17–18
• Across 200 paired substitutions, the trained-minus-external hull difference had median 3 bytes and ninetieth percentile 13; it was positive in 144 trials, zero in 38, and negative in 18.The reported damage bounds depend on the declared H ≤ 4 inventory; its slack is an upper bound on global slack.Source: §6 · p. 18
• Edit slack is reported as both hull slack and unoccupied admissible positions; these inventory-relative measures can differ because one subtracts hull width and the other moved-boundary count.The comparison is made for both the evaluation-tailored ceiling inventory and the frozen hybrid inventory.Source: §6 · pp. 18–19, Table 6 · p. 19
• Synchronization distance is unbounded for both subword vocabularies, newline is not a sound split delimiter for either, and the 48-merge and 384-merge vocabularies disagreed on all 64 held-out slices.Each disagreement was exhibited by the two scans of that slice.Source: §6 · pp. 19–20
• All four campaign grammars had unbounded anchor-free spans, while certified-anchor cuts reproduced archived scans; supply ranged from 6.7 anchors per kibibyte for block comments to 324.4 for bare tokens.The conventional and split-friendly grammars used the same corpus: making newline its own token raised supply from 25.7 to 41.0 anchors per kibibyte. Of 156 certified pairs, 39 were vacuous and anchored no corpus positions; campaign edits moved boundaries only between flanking shared-context anchors, with median hull one byte and maximum two.Source: §6 · pp. 20–21

7 The artifact: the theorem as a scanner

• The probe derives anchors from the campaign grammar before input exists, scans chunks in parallel, joins them, and asserts equality with the sequential boundary stream.Its inventory is pinned by repository, commit, and source digest.Source: §7 · p. 21
• The chunked boundary stream is byte-identical in every tested configuration on both the half-mebibyte corpus and its sixteen-copy scaling case.The larger case repeats the same corpus, so it tests scale rather than input variety.Source: §7 · p. 22
• On the recorded machine, scanning the 8,388,608-byte input took 35.06 milliseconds sequentially and 5.70 milliseconds with 32 workers, a 6.16 speedup.Timings include thread creation and joining but exclude anchor discovery, cut selection, and output concatenation; they are best-of-five measurements on one machine.Source: §7 · p. 22
• The snap distances depend on the input, inventory, and worker grid, while the timings are machine-dependent and do not form part of the theorem’s guarantee.The equality of boundary streams is the stable fact the theorem promises.Source: §7 · p. 22

Code synchronization and resolving blocks

• Beyond the code-factorization special case, the paper reports finding no prior work deciding whether every occurrence of a window fixes the covering token’s origin for prioritized maximal-munch languages.In the code case, certification additionally requires the origin to be a factorization boundary at every occurrence and the window tail to be a codeword prefix.Source: §8 · pp. 22–23

Longest match as a finite-state relation

• The armed-run construction decides properties of maximal-munch segmentations rather than merely relying on a scanner’s existence or its runtime algorithm.It validates proposed boundary marks and supports certificate testing; the related transducer work establishes a regular output range, while the existence of an offline verifier is an inference from that work.Source: §8 · p. 23

Equivalence of transducers, and what it decides

• The differential decision separates domain equivalence from boundary equality and returns witnesses, using armed runs to compare the policies’ correctly marked scans.This differs from the symbolic-transducer equivalence framework, whose described decision is nonconstructive and whose counterexample generation is separate.Source: §8 · pp. 23–24

Incremental and checkpointed lexing

• Certificate-based edit bounds need no cached scanner state, unlike incremental lexing, but apply only where the token set supplies an anchor.The next certified anchor witnessed in unchanged suffix bytes is a boundary in both versions; hopper uses this approach for range edits and may relex the whole input if no anchor is found.Source: §8 · p. 24

Cutting at a boundary, and deciding where one is

• Certificates provide a token-set-derived sufficient cut condition, stronger than a boundary at the origin and distinct from checks made at known joins.The paper does not decide the weaker predicate that an origin is a boundary at every occurrence without requiring the final-byte-covering token to start there.Source: §8 · pp. 24–25

Parallel scanning

• Certified-anchor parallel scanning avoids entry-state enumeration and reconciliation, unlike several exact or speculative alternatives, but can cut only where the grammar permits.Anchor supply determines where this approach is available; the cited approaches include transition enumeration, speculation, partition-and-restart scanning, and XML preparsing.Source: §8 · p. 25

The neighbouring quantity; Self-synchronization

• A bounded scanner confirmation distance does not guarantee certified origins: for T = {aa}, the inventory is empty and the anchor-free span is unbounded.The paper also reports three as the computed anchor-free span for the UTF-8 token-set shape, while noting that the distance itself is already known.Source: §8 · pp. 25–26

Expected density under coverage, worst-case gaps without it

• Unlike coverage-based local chunking and expected-density analyses, the paper measures certified-anchor gaps and supply without assuming every window contains a selected position.The paper connects bounded anchor-free span to unavoidable sets [34] and universal hitting sets [29], while restoring tokenization semantics to the question.Source: §8 · p. 26

9 Conclusion

• A certificate is a window and origin such that every occurrence in every completely tokenizable input has its final-byte-covering token begin at that origin.Every certified position is a boundary, but not every boundary is certified.Source: §9 · p. 27
• Certification is decided at inventory scale with witnesses, and its consequences include splitting, editing, delimiting, and anchor-free-span results checked by programs.The artifact cuts at precomputed anchors without speculation or reconciliation and asserts boundary-stream equality on every run.Source: §9 · p. 27
• The theory concerns greedy maximal-munch scans of literal and regular token sets, while campaign grammars enter through class abstractions checked against byte-level scans.Density remains a measured corpus fact rather than a grammar-wide guarantee.Source: §9 · p. 27

A Reproduction and provenance

• The check-paper script regenerates every quoted in-bundle emission and compares it byte for byte, rebuilding scanner statistics when the pinned build is supplied.It also rebuilds the manuscript and checks named measurements against their producing emissions.Source: A Reproduction and provenance · p. 27
• The gate refuses to skip absent inputs: GPT-2 reference files are checked against published digests, and the verify-all script fetches and verifies twitter.json.Campaign corpora ship with the bundle, allowing campaign emissions to rerun without network access.Source: A Reproduction and provenance · p. 28
• The scanner runner pins the munch repository commit and probe-source digests, binding the measurements to that checkout rather than an arbitrary local version.The scanner probe links the library and includes its grammar header, so a source digest alone would not identify everything executed.Source: A Reproduction and provenance · p. 28
• The library tests compare three decisions and a supply measurement with the exploration programs, while its recomputation probe reproduces emissions from library decisions.Across eleven emissions, 228 lines match byte for byte; seven agree up to omitted remainder fields and two use different names for the same decision, with none differing.Source: A Reproduction and provenance · pp. 28–29
• Two scope differences remain: the library’s conservative window model can undercount certified windows, and its campaign density verdict corroborates rather than establishes the emission’s result.The probe’s anchor-free-span check covers byte expansions admitted by the conservative model, a subset of the exact class-window inventory.Source: A Reproduction and provenance · p. 29