Generalized star height at most three

The explanation

Take every word made of the letters a and b that contains ab somewhere. There are 16 words of length four, and 11 of them qualify. The five that do not are aaaa, baaa, bbaa, bbba and bbbb. A regular expression (a short formula for a set of words) can describe this set. The usual formula reads: anything, then ab, then anything. Writing "anything" needs a star. The star means "repeat as often as you like."

Now allow one more operation, the complement. It means every word not in a given set. The empty set contains no words, so its complement is every word. That writes "anything" with no star at all. So once complement is allowed, the set above needs zero stars. Some sets still need a star. Over the single letter a, take the words of even length. Up to length ten, that is 6 of the 11 possible lengths. Without a star, a one-letter set is always finite or cofinite (missing only finitely many words). The even lengths are neither, so this set needs one star.

The generalized star height of a set of words counts stars inside stars. It is the smallest nesting depth of stars that any formula for the set needs, when complement is allowed. The sets in question are regular languages. These are the sets a finite automaton can recognize. A finite automaton is a machine with finitely many states that reads a word letter by letter. The question asks whether one fixed depth works for every regular language.

Without complement, the answer is no. In 1963, Lawrence Eggan linked ordinary star height to the loops in an automaton's diagram. In 1966, Françoise Dejean and Marcel-Paul Schützenberger showed ordinary star height is unbounded, even with two letters. Those lower bounds do not carry over once complement is added. In 1965, Schützenberger described exactly which languages need no star in the generalized setting. Later work proved a depth of one for special families. Pin, Straubing and Thérien did this in 1992 for languages recognized by certain finite groups. Nothing gave a bound for every regular language.

That was the obstacle: the known results covered only restricted families. A general regular language has no special structure to exploit. Every regular language does come with a finite monoid. That is a finite table recording how each word moves the automaton between states. The task is to compute that table's value for any word with only a few nested stars.

These papers prove a uniform bound (Lean proof listed). Every regular language, over any finite alphabet, has generalized star height at most threeSource 1. The formulas use the same letters as the language, and complement means all other words over those lettersSource 2. Three separate papers give three separate proofs, of the bounds thirteen, four and three. None uses another's numerical resultSource 3. The proof of three cuts each word into pieces called episodes, which can be found in only one waySource 4. It checks the front and back of each piece separately. A clock (a word-length counter that cycles) forces the two checks to agree, or to differ in one way onlySource 5. The paper builds each piece's computation so that this one mismatch still gives the right answerSource 6. Two such splitting steps, each adding one star, reach depth threeSource 7.

The bound limits the nesting only. The paper gives no bound on how long the formulas are or how long building them takesSource 8. It also does not show that any language needs more than one starSource 9. Whether depth one always suffices is still undecided. Howard Straubing's 2002 account treats that as a different question from the existence of a fixed boundSource 10.

How sure is this? A computer proof checker called Lean has checked a formal proof of the main statement. It says every regular language over a finite alphabet has depth at most three. Complements are taken over the same alphabet. The formal statement does not separately encode every construction step of the paper with the bound thirteen. No specialist review has been published.

What it doesn't show. This does not show that any language needs more than one nested star.