Langlib

Langlib.Automata.LinearBounded.Equivalence.LBAToCSG

LBA → Context-Sensitive Grammar (Myhill's Construction) #

This file constructs a context-sensitive grammar from a nondeterministic linear bounded automaton (LBA), establishing the direction LBA → CSG.

Given an LBA M with tape alphabet Γ, states Λ, and input embedding embed : T ↪ Γ, we construct a context-sensitive grammar whose language equals the LBA's language.

The nonterminals encode the LBA's computation at each tape cell, simulation rules mirror transitions, and cleanup rules recover terminals upon acceptance.

Simulation rules #

For interior head moves (left/right), the simulation uses a three-step process because CS rules can only rewrite one nonterminal at a time:

  1. Step 1: Remove the head from the current cell, write the new tape symbol, and record the pending state in a cellPending nonterminal. The transition check (q', a', d) ∈ M.transition q a is enforced here.

  2. Step 2: Place the head on the adjacent cell with the correct state q'. The state is read from the cellPending context, ensuring correctness.

  3. Step 3: Convert the cellPending nonterminal back to a normal cell with q = none.

References #

Nonterminal Type #

source
inductive MyhillConstruction.MyhillNT (T Γ Λ : Type) :
Type

Nonterminals for the Myhill construction.

Instances For
    source
    instance MyhillConstruction.instDecidableEqMyhillNT {T✝ Γ✝ Λ✝ : Type} [DecidableEq T✝] [DecidableEq Γ✝] [DecidableEq Λ✝] :
    DecidableEq (MyhillNT T✝ Γ✝ Λ✝)
    Equations
    source
    def MyhillConstruction.instDecidableEqMyhillNT.decEq {T✝ Γ✝ Λ✝ : Type} [DecidableEq T✝] [DecidableEq Γ✝] [DecidableEq Λ✝] (x✝ x✝¹ : MyhillNT T✝ Γ✝ Λ✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      instance MyhillConstruction.instFintypeMyhillNT {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] :
      Fintype (MyhillNT T Γ Λ)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[reducible, inline]
      abbrev MyhillConstruction.cellSym {T Γ Λ : Type} (lb rb : Bool) (q : Option Λ) (a : Γ) (t : T) :
      symbol T (MyhillNT T Γ Λ)

      Abbreviation for a cell nonterminal as a grammar symbol.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev MyhillConstruction.cellPendingSym {T Γ Λ : Type} (lb rb dir : Bool) (q' : Λ) (a : Γ) (t : T) :
        symbol T (MyhillNT T Γ Λ)

        Abbreviation for a cellPending nonterminal as a grammar symbol. The dir flag records the move direction (true = right move, false = left move) so that only the matching step2 rule can consume the pending — without it, an interior pending (false, false) would be accepted by both step2 rules, letting a right move's state land on the wrong (left) neighbour.

        Equations
        Instances For
          source
          def MyhillConstruction.myhillAllRules {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) :
          List (csrule T (MyhillNT T Γ Λ))

          All grammar rules for the Myhill construction, organized by phase.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem MyhillConstruction.myhillAllRules_output_nonempty {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (r : csrule T (MyhillNT T Γ Λ)) :
            r ∈ myhillAllRules M embed → r.output_string ≠ []

            Every rule in the Myhill construction has non-empty output string.

            source
            def MyhillConstruction.myhillGrammar {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) :
            CS_grammar T

            The Myhill context-sensitive grammar recognizing the LBA's language.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem MyhillConstruction.single_cell_init_rule_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (t : T) :
              { context_left := [], input_nonterminal := MyhillNT.start, context_right := [], output_string := [cellSym true true (some M.initial) (embed t) t] } ∈ myhillAllRules M embed
              source
              theorem MyhillConstruction.right_cell_init_rule_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (t : T) :
              { context_left := [], input_nonterminal := MyhillNT.start, context_right := [], output_string := [symbol.nonterminal MyhillNT.startAux, cellSym false true none (embed t) t] } ∈ myhillAllRules M embed

              Rightmost initial cell (laid first, with startAux on its left).

              source
              theorem MyhillConstruction.middle_cell_init_rule_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (t : T) :
              { context_left := [], input_nonterminal := MyhillNT.startAux, context_right := [], output_string := [symbol.nonterminal MyhillNT.startAux, cellSym false false none (embed t) t] } ∈ myhillAllRules M embed

              A middle initial cell, inserted just to the right of startAux.

              source
              theorem MyhillConstruction.left_cell_init_rule_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (t : T) :
              { context_left := [], input_nonterminal := MyhillNT.startAux, context_right := [], output_string := [cellSym true false (some M.initial) (embed t) t] } ∈ myhillAllRules M embed

              Leftmost initial cell carrying the start state (laid last, removing startAux).

              source
              theorem MyhillConstruction.accept_rule_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (q : Λ) (hq : M.accept q = true) (a : Γ) (t : T) (lb rb : Bool) :
              { context_left := [], input_nonterminal := MyhillNT.cell lb rb (some q) a t, context_right := [], output_string := [symbol.terminal t] } ∈ myhillAllRules M embed
              source
              theorem MyhillConstruction.left_propagation_rule_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (t₁ : T) (a : Γ) (t₂ : T) (lb rb : Bool) :
              { context_left := [symbol.terminal t₁], input_nonterminal := MyhillNT.cell lb rb none a t₂, context_right := [], output_string := [symbol.terminal t₂] } ∈ myhillAllRules M embed
              source
              theorem MyhillConstruction.right_propagation_rule_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (a : Γ) (t₁ t₂ : T) (lb rb : Bool) :
              { context_left := [], input_nonterminal := MyhillNT.cell lb rb none a t₁, context_right := [symbol.terminal t₂], output_string := [symbol.terminal t₁] } ∈ myhillAllRules M embed

              Simulation rule membership lemmas #

              source
              theorem MyhillConstruction.sim_stay_rule_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (q q' : Λ) (a a' : Γ) (t : T) (lb rb : Bool) (h : (q', a', DLBA.Dir.stay) ∈ M.transition q a) :
              { context_left := [], input_nonterminal := MyhillNT.cell lb rb (some q) a t, context_right := [], output_string := [cellSym lb rb (some q') a' t] } ∈ myhillAllRules M embed
              source
              theorem MyhillConstruction.sim_right_boundary_rule_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (q q' : Λ) (a a' : Γ) (t : T) (lb : Bool) (h : (q', a', DLBA.Dir.right) ∈ M.transition q a) :
              { context_left := [], input_nonterminal := MyhillNT.cell lb true (some q) a t, context_right := [], output_string := [cellSym lb true (some q') a' t] } ∈ myhillAllRules M embed
              source
              theorem MyhillConstruction.sim_left_boundary_rule_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (q q' : Λ) (a a' : Γ) (t : T) (rb : Bool) (h : (q', a', DLBA.Dir.left) ∈ M.transition q a) :
              { context_left := [], input_nonterminal := MyhillNT.cell true rb (some q) a t, context_right := [], output_string := [cellSym true rb (some q') a' t] } ∈ myhillAllRules M embed
              source
              theorem MyhillConstruction.sim_right_interior_step1_boundary_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (q q' : Λ) (a a' : Γ) (t₁ t₂ : T) (rb₂ : Bool) (hi : Option Λ) (b : Γ) (h : (q', a', DLBA.Dir.right) ∈ M.transition q a) :
              { context_left := [], input_nonterminal := MyhillNT.cell true false (some q) a t₁, context_right := [cellSym false rb₂ hi b t₂], output_string := [cellPendingSym true false true q' a' t₁] } ∈ myhillAllRules M embed
              source
              theorem MyhillConstruction.sim_right_interior_step1_interior_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (q q' : Λ) (a a' : Γ) (t₁ t₂ : T) (rb₂ : Bool) (hi : Option Λ) (b : Γ) (lb₀ : Bool) (a₀ : Γ) (t₀ : T) (h : (q', a', DLBA.Dir.right) ∈ M.transition q a) :
              { context_left := [cellSym lb₀ false none a₀ t₀], input_nonterminal := MyhillNT.cell false false (some q) a t₁, context_right := [cellSym false rb₂ hi b t₂], output_string := [cellPendingSym false false true q' a' t₁] } ∈ myhillAllRules M embed
              source
              theorem MyhillConstruction.sim_right_interior_step2_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (q' : Λ) (a' : Γ) (t₁ t₂ : T) (lb₁ rb₂ : Bool) (b : Γ) :
              { context_left := [cellPendingSym lb₁ false true q' a' t₁], input_nonterminal := MyhillNT.cell false rb₂ none b t₂, context_right := [], output_string := [cellSym false rb₂ (some q') b t₂] } ∈ myhillAllRules M embed
              source
              theorem MyhillConstruction.sim_left_interior_step1_boundary_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (q q' : Λ) (a a' : Γ) (t₁ t₂ : T) (lb₁ : Bool) (hi : Option Λ) (b : Γ) (h : (q', a', DLBA.Dir.left) ∈ M.transition q a) :
              { context_left := [cellSym lb₁ false hi b t₁], input_nonterminal := MyhillNT.cell false true (some q) a t₂, context_right := [], output_string := [cellPendingSym false true false q' a' t₂] } ∈ myhillAllRules M embed
              source
              theorem MyhillConstruction.sim_left_interior_step1_interior_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (q q' : Λ) (a a' : Γ) (t₁ t₂ : T) (lb₁ : Bool) (hi : Option Λ) (b : Γ) (rb₀ : Bool) (a₀ : Γ) (t₀ : T) (h : (q', a', DLBA.Dir.left) ∈ M.transition q a) :
              { context_left := [cellSym lb₁ false hi b t₁], input_nonterminal := MyhillNT.cell false false (some q) a t₂, context_right := [cellSym false rb₀ none a₀ t₀], output_string := [cellPendingSym false false false q' a' t₂] } ∈ myhillAllRules M embed
              source
              theorem MyhillConstruction.sim_left_interior_step2_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (q' : Λ) (a' : Γ) (t₁ t₂ : T) (lb₁ rb₂ : Bool) (b : Γ) :
              { context_left := [], input_nonterminal := MyhillNT.cell lb₁ false none b t₁, context_right := [cellPendingSym false rb₂ false q' a' t₂], output_string := [cellSym lb₁ false (some q') b t₁] } ∈ myhillAllRules M embed
              source
              theorem MyhillConstruction.pending_resolution_rule_mem {T Γ Λ : Type} [Fintype T] [Fintype Γ] [Fintype Λ] (M : LBA.Machine Γ Λ) (embed : T ↪ Γ) (q' : Λ) (a' : Γ) (t : T) (lb rb dir : Bool) :
              { context_left := [], input_nonterminal := MyhillNT.cellPending lb rb dir q' a' t, context_right := [], output_string := [cellSym lb rb none a' t] } ∈ myhillAllRules M embed