One-way-liveness proof: Normalization

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Automata/Normalization.lean

Module and namespace names, imports, and formatting are adapted to complexitylib. The machine definitions are shared through Models.FiniteAutomaton.Defs.

structure Complexity.FiniteAutomaton.Machine (Alpha Q : Type) : Type

A deterministic automaton on an arbitrary state type.

• initial : Q

  The initial control state.

• accepting : Set Q

  The accepting control states.

• transition : Q → Symbol Alpha → Option (Q × Move)

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

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

@[reducible, inline]

abbrev Complexity.FiniteAutomaton.Machine.Config {Alpha Q : Type} (w : List Alpha) : Type

A position on the endmarked word and a control state.

Equations

• Complexity.FiniteAutomaton.Machine.Config w = (Fin (w.length + 2) × Q)

def Complexity.FiniteAutomaton.Machine.Step {Alpha Q : Type} (M : Machine Alpha Q) (w : List Alpha) (c c' : Config w) : Prop

One deterministic transition on the scanned input symbol.

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.Machine.Accepts {Alpha Q : Type} (M : Machine Alpha Q) (positive : Bool) (w : List Alpha) : Prop

A finite run from the initial configuration reaches an accepting state.

Equations

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

def Complexity.FiniteAutomaton.DMachine.toMachine {Alpha : Type} {s : ℕ} (M : DMachine Alpha s) : Machine Alpha (Fin s)

View a numbered-state deterministic automaton as an arbitrary-state machine.

Equations

• M.toMachine = { initial := M.initial, accepting := M.accepting, transition := M.transition, left_boundary := ⋯, right_boundary := ⋯ }

theorem Complexity.FiniteAutomaton.DMachine.toMachine_accepts {Alpha : Type} {s : ℕ} (M : DMachine Alpha s) (positive : Bool) (w : List Alpha) : M.toMachine.Accepts positive w ↔ M.Accepts positive w

def Complexity.FiniteAutomaton.Machine.positiveCopy {Alpha Q : Type} (M : Machine Alpha Q) : Machine Alpha (Option Q)

A fresh nonaccepting initial state copies the original initial row.

Equations

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

theorem Complexity.FiniteAutomaton.Machine.positiveCopy_step {Alpha Q : Type} (M : Machine Alpha Q) (w : List Alpha) (i : Fin (w.length + 2)) (q : Option Q) (c' : Config w) : M.positiveCopy.Step w (i, q) c' ↔ ∃ (r : Q), c'.2 = some r ∧ M.Step w (i, q.getD M.initial) (c'.1, r)

theorem Complexity.FiniteAutomaton.Machine.positiveCopy_reach {Alpha Q : Type} (M : Machine Alpha Q) (w : List Alpha) (c c' : Config w) : Relation.ReflTransGen (M.positiveCopy.Step w) (c.1, some c.2) (c'.1, some c'.2) ↔ Relation.ReflTransGen (M.Step w) c c'

theorem Complexity.FiniteAutomaton.Machine.positiveCopy_accepts {Alpha Q : Type} (M : Machine Alpha Q) (w : List Alpha) : M.positiveCopy.Accepts false w ↔ M.Accepts true w

noncomputable def Complexity.FiniteAutomaton.Machine.sinkCopy {Alpha Q : Type} (M : Machine Alpha Q) : Machine Alpha (Option Q)

Sink normalization also replaces missing transitions at accepting states.

Equations

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

theorem Complexity.FiniteAutomaton.Machine.sinkCopy_step_old {Alpha Q : Type} (M : Machine Alpha Q) (w : List Alpha) (c : Config w) (c' : Config w) : M.sinkCopy.Step w (c.1, some c.2) c' ↔ c.2 ∈ M.accepting ∧ c' = (c.1, none) ∨ c.2 ∉ M.accepting ∧ ∃ (r : Q), c'.2 = some r ∧ M.Step w c (c'.1, r)

theorem Complexity.FiniteAutomaton.scanned_eq_left_iff {Alpha : Type} (w : List Alpha) (i : Fin (w.length + 2)) : scanned w i = Symbol.left ↔ ↑i = 0

theorem Complexity.FiniteAutomaton.scanned_eq_right_iff {Alpha : Type} (w : List Alpha) (i : Fin (w.length + 2)) : scanned w i = Symbol.right ↔ ↑i = w.length + 1

def Complexity.FiniteAutomaton.Machine.terminal {Alpha Q : Type} (w : List Alpha) : Config w

The fresh sink state at the right endmarker.

Equations

• Complexity.FiniteAutomaton.Machine.terminal w = (⟨w.length + 1, ⋯⟩, none)

theorem Complexity.FiniteAutomaton.Machine.sinkCopy_sweep {Alpha Q : Type} (M : Machine Alpha Q) (w : List Alpha) (i : Fin (w.length + 2)) : Relation.ReflTransGen (M.sinkCopy.Step w) (i, none) (terminal w)

theorem Complexity.FiniteAutomaton.Machine.sinkCopy_reach_iff {Alpha Q : Type} (M : Machine Alpha Q) (w : List Alpha) (c : Config w) : Relation.ReflTransGen (M.sinkCopy.Step w) (c.1, some c.2) (terminal w) ↔ ∃ (a : Config w), Relation.ReflTransGen (M.Step w) c a ∧ a.2 ∈ M.accepting

theorem Complexity.FiniteAutomaton.Machine.sinkCopy_accepts {Alpha Q : Type} (M : Machine Alpha Q) (w : List Alpha) : Relation.ReflTransGen (M.sinkCopy.Step w) (⟨0, ⋯⟩, some M.initial) (terminal w) ↔ M.Accepts false w

theorem Complexity.FiniteAutomaton.Machine.sinkCopy_terminal {Alpha Q : Type} (M : Machine Alpha Q) (w : List Alpha) : M.sinkCopy.transition (terminal w).2 (scanned w (terminal w).1) = none