Documentation

Complexitylib.Models.FiniteAutomaton.Complementation.Internal.Normalization

Two-way complementation: normalization #

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

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

source
theorem Complexity.FiniteAutomaton.Complementation.Internal.tapeSymbol_left_iff {Sigma : Type u_1} (w : List Sigma) (p : Fin (w.length + 2)) :
tapeSymbol w p = Sum.inl 0 ↔ ↑p = 0

Only the first tape position carries the left endmarker.

source
theorem Complexity.FiniteAutomaton.Complementation.Internal.tapeSymbol_right_iff {Sigma : Type u_1} (w : List Sigma) (p : Fin (w.length + 2)) :
tapeSymbol w p = Sum.inl 1 ↔ ↑p = w.length + 1

Only the last original tape position carries the right endmarker.

source
def Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.reindex {Sigma : Type u_1} {Q : Type u_2} {Q' : Type u_3} (A : TwoNFA Sigma Q) (e : Q ≃ Q') :
TwoNFA Sigma Q'

Rename states along an equivalence, retaining all transitions and moves.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.reindex_language {Sigma : Type u_1} {Q : Type u_2} {Q' : Type u_3} (A : TwoNFA Sigma Q) (e : Q ≃ Q') :
    (A.reindex e).language = A.language
    source
    def Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.augmentConfig {Q : Type u_1} {n : ℕ} (c : Q × Fin n) :
    Option Q × Fin (n + 1)

    Embed an original configuration while reserving one state and one exit position.

    Equations
    Instances For
      source
      theorem Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.augmentConfig_injective {Q : Type u_1} {n : ℕ} :
      Function.Injective augmentConfig
      source
      def Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.augmentedStep {Sigma : Type u_1} {Q : Type u_2} (A : TwoNFA Sigma Q) (w : List Sigma) :
      SetRel (Option Q × Fin (w.length + 3)) (Option Q × Fin (w.length + 3))

      Original moves, an accepting stay into the fresh state, and its rightward sweep.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.augmented_run_cases {Sigma : Type u_1} {Q : Type u_2} (A : TwoNFA Sigma Q) (w : List Sigma) {c : Option Q × Fin (w.length + 3)} (hrun : (augmentConfig (A.initial, ⟨0, ⋯⟩), c) ∈ relStar (A.augmentedStep w)) :
        w ∈ A.language ∨ ∃ (x : Q × Fin (w.length + 2)), c = augmentConfig x ∧ ((A.initial, ⟨0, ⋯⟩), x) ∈ relStar (A.step w)

        Before entering the fresh state, every augmented finite path is an original run.

        source
        theorem Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.augmented_sink_exit {Sigma : Type u_1} {Q : Type u_2} (A : TwoNFA Sigma Q) (w : List Sigma) (p : Fin (w.length + 3)) :
        ((none, p), none, ⟨w.length + 2, ⋯⟩) ∈ relStar (A.augmentedStep w)

        The fresh state can sweep from any position to the designated right exit.

        source
        theorem Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.augmented_acceptance {Sigma : Type u_1} {Q : Type u_2} (A : TwoNFA Sigma Q) (w : List Sigma) :
        w ∈ A.language ↔ (augmentConfig (A.initial, ⟨0, ⋯⟩), none, ⟨w.length + 2, ⋯⟩) ∈ relStar (A.augmentedStep w)

        Finite acceptance is equivalent to reaching the designated augmented exit.

        source
        def Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.augmentedMove {Sigma : Type u_1} {Q : Type u_2} (A : TwoNFA Sigma Q) (symbol : Fin 2 ⊕ Sigma) (move : Fin 3) :
        SetRel (Option Q) (Option Q)

        Augmented moves at one symbol, including the original endmarker restrictions.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Complexity.FiniteAutomaton.Complementation.Internal.TwoNFA.augmentedStep_local_iff {Sigma : Type u_1} {Q : Type u_2} (A : TwoNFA Sigma Q) (w : List Sigma) (c d : Option Q × Fin (w.length + 3)) :
          (c, d) ∈ A.augmentedStep w ↔ ∃ (p : Fin (w.length + 2)), c.2 = p.castSucc ∧ ∃ (move : Fin 3), (c.1, d.1) ∈ A.augmentedMove (tapeSymbol w p) move ∧ ↑↑d.2 = ↑↑p + ↑↑move - 1

          The global augmented graph is exactly the graph of the local moves and head displacement.