Every Regular Language Has Generalized Star-Height At Most 13

A regular expression’s star-height counts how deeply repetition is nested. Two stars side by side have height one; a star inside another star has height two. But the height of a displayed expression is not necessarily the minimum height needed for its language: another expression may describe the same language with shallower nesting.

The generalized version also allows complement: the set of all words over the alphabet that are not in a language. Complement adds no height. In particular, all words over an alphabet can be written as the complement of the empty language, with height zero.

The manuscript claims a uniform upper bound: for every finite alphabet Σ and every regular language L over it, there is a generalized regular expression for L over that same alphabet with height at most 13.^† Union and concatenation take the greater height of their inputs; complement adds none; only the Kleene star adds one.

That is a ceiling on depth, not on length. The construction can be enormous. The result does not say that 13 is necessary, nor does it settle whether height one always suffices. If the alphabet is empty, only the empty language and the language containing just the empty word are possible, and both have height zero.

A finite automaton reads a word one letter at a time. Each word induces a transformation of the automaton’s states. The transformations form a finite monoid under composition, with an identity transformation. Some transformations merge states, so the monoid need not have inverses.

The proof represents each element m of a finite monoid by its own basis vector over the two-element field F₂. Multiplication by an element d sends the vector for m to the vector for md. Starting with the identity’s vector therefore lets the computation track the product induced by a word.

Words are parsed into non-empty pieces called episodes, followed by a remainder. The parsing is unique because no episode is a proper prefix of another. This structure gives the proof places to make local predictions about a word’s monoid product and then combine them without requiring any single test to inspect the whole word.

In a prediction trial, the word is divided into consecutive intervals. Each interval has a predicted monoid product; together those predictions give a predicted whole product T*, while the actual whole product is T. Candidate blocks enumerate pairs of vectors: an input vector and a proposed output vector. A block qualifies if its output is its input acted on by T*, all earlier interval predictions are correct, and the entire suffix after the block has its predicted product. The block’s own interval is deliberately left unchecked.

The asymmetry lets a prefix and suffix certify different parts of the trial without either reading all of it. Suppose two qualifying blocks occur, with h before j. The later block certifies the intervals through h; the earlier block certifies the suffix after h. Joined together, those pieces establish that the actual whole product equals T*. This reasoning uses neither inverses nor cancellation.

So if T and T* differ, at most one block can qualify. The construction chooses a shift β to make that block’s input reach its stated output, or chooses zero if there is no qualifying block. The shift is an adjustment to the output of the trial’s linear action: it makes the exceptional input-output pair fit. If T equals T*, zero fits every qualifying pair. That equality does not imply that every interval prediction was correct. A perfect prediction does, however, supply a qualifying block for every input.

The trial is represented as an affine rule, v ↦ vT + β. Here v is the input vector, T is the trial’s linear action, and β is the added shift. Such rules compose into affine rules. Evaluate the composite rule on v and on zero; adding the results removes the shift and recovers the linear action. Over F₂, subtraction and addition are the same. Boolean combinations of input-output graph tests can perform this recovery without adding a star.

The local argument depends on making independently chosen prefix and suffix cuts sound. Whenever both tests pass, they must identify exactly one episode and its fixed update. Every designated episode must also provide a successful cut for every input.

The construction uses a finite clock to constrain successful tag pairs: they either agree or form one fixed mismatched pair, which the affine shift can absorb. Endpoint guards prevent a suffix from stopping too early or swallowing another episode. Local markers define trial boundaries; sufficiently long markerless windows provide periodic runs and many equivalent cut opportunities. These devices yield two outer splits, though the clock, marker, and endpoint proofs are not reproduced in the explainer.

If neither outer split is guaranteed to find a cut, the manuscript identifies five possible witnesses: a first-clock or prediction failure, an unstable inner search, a second-clock failure, a marker just beyond a search window, or an unstable end search. Each witness receives two further splits. One uses a perfect trial; the other recovers a measurement from a complete decision history when no trial is perfect.

The history construction counts every possible history, including paths no real prefix can produce. It makes many copies of each cut kind, more than the number of ambiguous copies, so the suffix can identify the true cut. Both splits compute the same enlarged affine update. Its linear part recovers the previous computation and resets its work register, allowing episodes to compose. The explainer presents these constructions as a roadmap and omits their technical proofs and parameters.

The component tests must themselves have low star-height. Bounded-length prefix tests have height zero. For the unbounded cases, the exact episode-end rule reduces words to a bounded prefix, repetitions of one fixed non-empty word, and a bounded tail.

On a template of that form, finite monoid powers eventually repeat as the repetition count grows. Each accepted residue class beyond the eventual-periodicity threshold can be expressed with one star; finitely many exceptional words add no nesting. This is a restricted-template argument, not a claim that arbitrary monoid tests have height one. Product tests for the unfinished final remainder also have height at most one, so words ending between episodes are covered.

The construction counts depth by letting a split turn a previous bound H into max(2, H + 1). Starting at zero, the first split reaches 2 and the next reaches 3. Two splits for each of the five witness types bring the bound to 11; the periodic-window split reaches 12, and the main split reaches 13.

Recovering linear parts, concatenating the remainder, and taking the accepting union add no depth. The result is the manuscript’s prediction-and-history route to a uniform bound over the same alphabet—not an algorithm for finding a shortest expression. The explainer says its finite checks support the explanation, but are not a formal reproduction of the theorem.