Two-way finite automata

Adapted from OpenAI's one-way-liveness formalization (25 September 2026): https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Automata/Model.lean

The input is enclosed by two distinct endmarkers. Transitions cannot cross these boundaries. Acceptance means that a finite run reaches an accepting state, with no requirement that rejected inputs halt. The Boolean positive parameter selects whether a length-zero accepting run is permitted (false) or excluded (true). NoLeft permits stationary moves as well as right moves. State counts include all states. These are finite automata, independently of the work tapes and time accounting of the library's Turing machines.

inductive Complexity.FiniteAutomaton.Symbol (Alpha : Type u_1) : Type u_1

The input alphabet with distinct left and right endmarkers.

• left {Alpha : Type u_1} : Symbol Alpha
• letter {Alpha : Type u_1} : Alpha → Symbol Alpha
• right {Alpha : Type u_1} : Symbol Alpha

inductive Complexity.FiniteAutomaton.Move : Type

A two-way head may move left, stay, or move right.

• left : Move
• stay : Move
• right : Move

@[instance_reducible]

instance Complexity.FiniteAutomaton.instDecidableEqMove : DecidableEq Move

Equations

• Complexity.FiniteAutomaton.instDecidableEqMove x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Complexity.FiniteAutomaton.Move.Rel : Move → ℕ → ℕ → Prop

The relation between two head positions specified by a move.

Equations

• Complexity.FiniteAutomaton.Move.left.Rel x✝¹ x✝ = (x✝ + 1 = x✝¹)
• Complexity.FiniteAutomaton.Move.stay.Rel x✝¹ x✝ = (x✝ = x✝¹)
• Complexity.FiniteAutomaton.Move.right.Rel x✝¹ x✝ = (x✝ = x✝¹ + 1)

def Complexity.FiniteAutomaton.scanned {Alpha : Type u_1} (w : List Alpha) (i : Fin (w.length + 2)) : Symbol Alpha

The finite word including both endmarkers.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.Configuration {Alpha : Type u_1} (w : List Alpha) (n : ℕ) : Type

A head position on the endmarked word and a finite control state.

Equations

• Complexity.FiniteAutomaton.Configuration w n = (Fin (w.length + 2) × Fin n)

structure Complexity.FiniteAutomaton.DMachine (Alpha : Type u_1) (s : ℕ) : Type u_1

A deterministic two-way finite automaton with exactly s named states.

• initial : Fin s

  The initial control state.

• accepting : Set (Fin s)

  The accepting control states.

• transition : Fin s → Symbol Alpha → Option (Fin s × Move)

  The next control states and head moves for each scanned symbol.

• left_boundary (q q' : Fin s) : self.transition q Symbol.left ≠ some (q', Move.left)
• right_boundary (q q' : Fin s) : self.transition q Symbol.right ≠ some (q', Move.right)

structure Complexity.FiniteAutomaton.NMachine (Alpha : Type u_1) (n : ℕ) : Type u_1

A nondeterministic two-way finite automaton with exactly n named states.

• initial : Fin n

  The initial control state.

• accepting : Set (Fin n)

  The accepting control states.

• transition : Fin n → Symbol Alpha → Set (Fin n × Move)

  The next control states and head moves for each scanned symbol.

• left_boundary (q q' : Fin n) : (q', Move.left) ∉ self.transition q Symbol.left
• right_boundary (q q' : Fin n) : (q', Move.right) ∉ self.transition q Symbol.right

def Complexity.FiniteAutomaton.DMachine.Step {Alpha : Type u_1} {s : ℕ} (M : DMachine Alpha s) (w : List Alpha) (c c' : Configuration w s) : Prop

A deterministic transition and its associated head movement.

Equations

• M.Step w c c' = ∃ (d : Complexity.FiniteAutomaton.Move), M.transition c.2 (Complexity.FiniteAutomaton.scanned w c.1) = some (c'.2, d) ∧ d.Rel ↑c.1 ↑c'.1

def Complexity.FiniteAutomaton.NMachine.Step {Alpha : Type u_1} {n : ℕ} (M : NMachine Alpha n) (w : List Alpha) (c c' : Configuration w n) : Prop

A chosen nondeterministic transition and its associated head movement.

Equations

• M.Step w c c' = ∃ (d : Complexity.FiniteAutomaton.Move), (c'.2, d) ∈ M.transition c.2 (Complexity.FiniteAutomaton.scanned w c.1) ∧ d.Rel ↑c.1 ↑c'.1

def Complexity.FiniteAutomaton.FiniteRun {C : Type u_1} (positive : Bool) (step : C → C → Prop) (c c' : C) : Prop

The positive convention explicitly excludes a length-zero computation.

Equations

• Complexity.FiniteAutomaton.FiniteRun positive step c c' = if positive = true then Relation.TransGen step c c' else Relation.ReflTransGen step c c'

def Complexity.FiniteAutomaton.DMachine.Accepts {Alpha : Type u_1} {s : ℕ} (M : DMachine Alpha s) (positive : Bool) (w : List Alpha) : Prop

A finite run from the left endmarker reaches an accepting state.

Equations

• M.Accepts positive w = ∃ (c : Complexity.FiniteAutomaton.Configuration w s), Complexity.FiniteAutomaton.FiniteRun positive (M.Step w) (⟨0, ⋯⟩, M.initial) c ∧ c.2 ∈ M.accepting

def Complexity.FiniteAutomaton.NMachine.Accepts {Alpha : Type u_1} {n : ℕ} (M : NMachine Alpha n) (positive : Bool) (w : List Alpha) : Prop

Some finite run from the left endmarker reaches an accepting state.

Equations

• M.Accepts positive w = ∃ (c : Complexity.FiniteAutomaton.Configuration w n), Complexity.FiniteAutomaton.FiniteRun positive (M.Step w) (⟨0, ⋯⟩, M.initial) c ∧ c.2 ∈ M.accepting

def Complexity.FiniteAutomaton.NMachine.NoLeft {Alpha : Type u_1} {n : ℕ} (M : NMachine Alpha n) : Prop

No transition moves the input head left; stationary moves are allowed.

Equations

• M.NoLeft = ∀ (q : Fin n) (a : Complexity.FiniteAutomaton.Symbol Alpha) (q' : Fin n), (q', Complexity.FiniteAutomaton.Move.left) ∉ M.transition q a

def Complexity.FiniteAutomaton.NMachine.Recognizes {Alpha : Type u_1} {n : ℕ} (M : NMachine Alpha n) (positive : Bool) (L : Set (List Alpha)) : Prop

The accepted words are exactly the members of the language.

Equations

• M.Recognizes positive L = ∀ (w : List Alpha), M.Accepts positive w ↔ w ∈ L

def Complexity.FiniteAutomaton.DMachine.Recognizes {Alpha : Type u_1} {s : ℕ} (M : DMachine Alpha s) (positive : Bool) (L : Set (List Alpha)) : Prop

The accepted words are exactly the members of the language.

Equations

• M.Recognizes positive L = ∀ (w : List Alpha), M.Accepts positive w ↔ w ∈ L

def Complexity.FiniteAutomaton.PolynomialSimulation (positive : Bool) : Prop

An alphabet-independent polynomial bound for deterministic simulation.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.FiniteAutomaton.OneWayPolynomialSimulation (positive : Bool) : Prop

A polynomial deterministic simulation bound restricted to one-way nondeterministic inputs.

Equations

• One or more equations did not get rendered due to their size.