Exponential state costs for two-way automata

1 · The essentials

These results concern simple machines that read a sequence of symbols while keeping track of only a limited number of internal states. Some machines can move backward as well as forward, and some can choose among several possible next steps. The first result asks how many states are needed to reverse a machine’s answer, accepting exactly the inputs it previously rejected. It gives examples where this reversal requires exponentially many states, even though both machines can move in either direction and make choices. The second result gives examples where replacing a forward-only machine that can make choices with a machine that cannot make choices also requires exponentially many states, despite allowing the replacement to move backward. In these examples, each collection of available input symbols is finite, but its size is not held fixed across the family. Both main lower-bound results have Lean formalizations.

A picture to help (an imperfect image, not to be taken literally)

As an imperfect image, imagine a reader checking a strip of symbols while keeping just one labeled card to record their current situation. Allowing the reader to reread earlier symbols does not necessarily keep the required collection of cards small when the task changes from finding a successful route through choices to giving a single prescribed answer, or to accepting exactly the previously rejected strips.

Why it matters

The results show that backward movement does not always prevent a large increase in the number of states needed for these changes of machine. Both rule out polynomial state bounds that are independent of alphabet size. The repository summary describes the deterministic simulation result as resolving the Sakoda–Sipser state-succinctness conjecture over growing finite alphabets.

2 · Going further

The first problem is complementation for two-way nondeterministic finite automata: given a machine, how many states are required by another machine of the same kind that accepts exactly its rejected words? For every $n \geq 4$ , the main manuscript constructs an $n$ -state automaton over a finite alphabet whose complement requires at least $\frac{1}{2} 2^{⌊(n - 4) /127 ⌋} - 1$ states. This is an exponential lower bound and excludes a polynomial bound depending only on the original state count, independently of alphabet size.

The companion manuscript studies one-way liveness on $h$ points. Its input is a word of binary relations, and it accepts precisely when their ordered product is nonempty. For every $h \geq 2$ , this language has a nondeterministic automaton with $h + 3$ states and no left moves. Yet every equivalent two-way deterministic automaton with $s$ states satisfies $4 (s + 2)^{2} \geq 2^{⌊(h - 2) /31 ⌋}$ , which forces exponential growth in the required deterministic state count.

At the level described by the abstracts, the shared strategy is to give languages with small source automata and establish exponential state requirements for the target machines. The abstracts do not provide the internal argument establishing those lower bounds. The manuscripts address distinct transformations—complementation and deterministic simulation—and both defeat alphabet-independent polynomial bounds. The second explicitly allows partial transition rules, stay moves, and nonaccepting infinite computations; its finite alphabets grow with $h$ .

Useful notions

Finite-state machines and accepted words
Deterministic versus nondeterministic choices
One-way versus two-way input movement
Polynomial versus exponential growth
Binary relations and their ordered products

What was known before / what is new

Before

The source places the deterministic simulation question in the context of the Sakoda–Sipser state-succinctness conjecture. It does not give earlier bounds or a history of either problem. The shared question is whether the relevant transformation can always be carried out with polynomially many states, without a dependence on alphabet size.

New

The main manuscript supplies an explicit exponential lower bound for complementing two-way nondeterministic automata, with examples for every $n \geq 4$ . The companion supplies a small forward-only nondeterministic machine for one-way liveness and an exponential lower bound for equivalent two-way deterministic machines. Both main lower-bound results have Lean formalizations.

Limits and assumptions

The complementation construction applies for $n \geq 4$ , and the one-way liveness result applies for $h \geq 2$ . The alphabets are finite but are not fixed across the families; the liveness alphabets explicitly grow with $h$ . These statements therefore rule out alphabet-independent polynomial bounds, but do not settle the corresponding fixed-alphabet questions. The deterministic lower bound allows partial transitions, stay moves, and nonaccepting infinite computations. Both manuscripts are marked Lean-formalized for their main results; the supplied source gives no finer description of the formalization scope or proof details.

Mini glossary

Finite automaton: A machine that reads input symbols while tracking one of finitely many internal states.
Nondeterministic automaton: An automaton that can have several possible next steps and accepts when some permitted computation accepts.
Two-way automaton: An automaton whose input reader can move backward as well as forward.
Complementation: Replacing a machine by one that accepts exactly the words the original machine does not accept.
Alphabet: The collection of symbols from which input words are formed.
State lower bound: A minimum number of states that every machine of the specified kind must have to perform the task.

Keywords : Finite automata · State complexity · Exponential lower bounds

AI-generated explanation based on the manuscript. Unofficial. Refer to the manuscript for the authoritative version.

3 · Technical details and sources

Claim made in the manuscript (source text)

Proves exponential lower bounds both for complementing two-way nondeterministic finite automata and for simulating one-way nondeterministic automata by two-way deterministic ones. The latter resolves the Sakoda–Sipser state-succinctness conjecture over growing finite alphabets; both results rule out polynomial state bounds independent of alphabet size.

Verified by Lean: the Lean software checked the part of the reasoning described below, sometimes only part of the manuscript. This does not mean independent mathematicians have validated the result.

Scope of the Lean formalization (source text)

…

lean/docs/129.md

Manuscripts in this family

★

An exponential state lower bound for two-way nondeterministic complementation

25/09/2026

Verified by Lean

We prove that two-way nondeterministic finite automata cannot be complemented with a polynomial number of states independent of the alphabet. For each n ≥ 4 we construct an n-state automaton over a finite alphabet whose complement requires at least $\frac{1}{2} 2^{⌊(n - 4) /127 ⌋} - 1$ states.

PDF GitHub folder Lean formalization

An exponential two-way deterministic state lower bound for one-way liveness

25/09/2026

Verified by Lean

One-way liveness on h points accepts a word of binary relations when their ordered product is nonempty. For every h ≥ 2, it has a nondeterministic automaton with $h + 3$ states and no left moves, whereas every equivalent s-state two-way deterministic automaton satisfies $4 (s + 2)^{2} \geq 2^{⌊(h - 2) /31 ⌋}$ . Partial transition rules, stay moves, and nonaccepting infinite computations are allowed. The alphabets are finite and grow with h, so the result rules out an alphabet-independent polynomial state bound for deterministic two-way simulation, already for one-way nondeterministic sources.

PDF GitHub folder Lean formalization