OAI.TwoWayComplementation.complementation_lower_bound_finite

The theorem states that for every natural number n ≥ 4 there is a two-way nondeterministic finite automaton A with n states whose input alphabet is the set of binary relations on {0,…,n−3} (subsets of Fin(n−2) × Fin(n−2)), such that the following lower bound holds. Here a two-way automaton has an initial state, a set of accepting states, and a transition map sending a state and the scanned tape symbol (a left endmarker, a right endmarker, or an input letter) to a set of pairs (new state, move), where the move is left, stay or right; the input word sits between the two endmarkers, the head starts on the left endmarker in the initial state, and a word is accepted if some finite sequence of steps reaches an accepting state. For every finite state type Q and every two-way nondeterministic automaton B over the same alphabet with state set Q, if the language of B is exactly the complement of the language of A, then the number of states of B satisfies |Q| ≥ (1/2)·2^⌊(n−4)/127⌋ − 1, where the exponent (n−4)/127 is read as natural-number division, so n−4 is truncated subtraction and the quotient is rounded down. Thus complementing A requires exponentially many states in n/127 for two-way nondeterministic automata.