Langlib

Langlib.Automata.LinearBounded.Equivalence.CSGToLBA.Construction

CSG → LBA (Kuroda): the simulating machine and its single-step semantics #

This file builds the backward-simulating LBA kMachine g₀ for a non-contracting grammar g₀ with finitely many nonterminals, and develops all the shared infrastructure used by both halves of the language equality:

The completeness and soundness arguments live in CSGToLBA/Completeness.lean and CSGToLBA/Soundness.lean.

References #

source
def KurodaConstruction.symbolEquivSum (T N : Type) :
symbol T N ≃ T ⊕ N

symbol T N is in bijection with the sum T ⊕ N (terminal ↦ left, nonterminal ↦ right). Used to transport Fintype onto the grammar-symbol work alphabet.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance KurodaConstruction.instFintypeSymbol (T N : Type) [Fintype T] [Fintype N] :
    Fintype (symbol T N)

    The grammar-symbol alphabet is finite whenever both the terminal and nonterminal alphabets are.

    Equations

    The simulating machine #

    We build a backward (reductive) simulator. On input w the tape starts with the |w| input cells some (Sum.inl wᵢ); the machine first converts them to work cells some (Sum.inr (isLeftEnd, isRightEnd, workSym)), where each workSym is a grammar symbol (initially the terminal wᵢ) or the blank # (none). The boundary bits are set during the conversion sweep: cell 0 is the start (the head begins there), and the right end is detected the moment the rightward sweep re-reads an already-converted cell (the clamp at the last cell).

    It then nondeterministically replays a derivation in reverse: each grammar rule input_L ++ [N] ++ input_R → output_string is applied as output_string ↦ input_L ++ [N] ++ input_R, padding the freed cells with #. Symbols are kept contiguous by bubbling blanks past symbols (a length-preserving swap of adjacent work cells). The machine accepts when the non-blank work symbols spell exactly [S] (the start symbol), verified by a sweep between the boundary markers.

    source
    def KurodaConstruction.ruleBound {T : Type} (g₀ : grammar T) :
    ℕ

    A bound on rule lengths: at least every rule's output length.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev KurodaConstruction.KWork {T : Type} (g₀ : grammar T) :
      Type

      The work symbol stored in a cell: a grammar symbol, or the blank # (none).

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev KurodaConstruction.KGamma {T : Type} (g₀ : grammar T) :
        Type

        The work-cell alphabet Γ: (isLeftEnd, isRightEnd, workSymbol).

        Equations
        Instances For
          source
          inductive KurodaConstruction.KState {T : Type} (g₀ : grammar T) :
          Type

          Control states of the backward simulator.

          • init0 {T : Type} {g₀ : grammar T} : KState g₀

            Convert cell 0 (the known left end): mark isLeftEnd, keep the terminal.

          • initSweep {T : Type} {g₀ : grammar T} : KState g₀

            Convert subsequent cells left-to-right; detect the right end on a clamp.

          • sim {T : Type} {g₀ : grammar T} : KState g₀

            Roaming simulation state: move freely, or start applying a rule / the accept check.

          • applyRule {T : Type} {g₀ : grammar T} (r : Fin g₀.rules.length) (k : Fin (ruleBound g₀ + 1)) : KState g₀

            Applying the r-th rule backward in a single left-to-right pass: skip blanks, match the k-th symbol of output_string, writing the replacement (patList[k] if k < |patList|, else blank) into that cell in place.

          • gotoLeft {T : Type} {g₀ : grammar T} : KState g₀

            Go to the left end (marked) to begin the accept check.

          • check {T : Type} {g₀ : grammar T} (seen : Bool) : KState g₀

            Accept-check sweep; seen records whether the unique start symbol was passed.

          • accept {T : Type} {g₀ : grammar T} : KState g₀

            The (unique) accepting state.

          Instances For
            source
            instance KurodaConstruction.instDecidableEqKState {T✝ : Type} {g₀✝ : grammar T✝} [DecidableEq T✝] :
            DecidableEq (KState g₀✝)
            Equations
            source
            def KurodaConstruction.instDecidableEqKState.decEq {T✝ : Type} {g₀✝ : grammar T✝} [DecidableEq T✝] (x✝ x✝¹ : KState g₀✝) :
            Decidable (x✝ = x✝¹)
            Equations
            Instances For
              source
              instance KurodaConstruction.instFintypeKState {T : Type} (g₀ : grammar T) :
              Fintype (KState g₀)
              Equations
              • One or more equations did not get rendered due to their size.
              source
              @[reducible, inline]
              abbrev KurodaConstruction.KCell {T : Type} (g₀ : grammar T) :
              Type

              A tape cell: an input symbol some (Sum.inl t), a work cell some (Sum.inr γ), or blank.

              Equations
              Instances For
                source
                def KurodaConstruction.patList {T : Type} (g₀ : grammar T) (r : grule T g₀.nt) :
                List (symbol T g₀.nt)

                The reverse-rule replacement string for rule r: input_L ++ [N] ++ input_R (what output_string is rewritten back to).

                Equations
                Instances For
                  source
                  def KurodaConstruction.kTransition {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] :
                  KState g₀ → KCell g₀ → Set (KState g₀ × KCell g₀ × DLBA.Dir)

                  The nondeterministic transition relation of the backward simulator.

                  Equations
                  Instances For
                    source
                    def KurodaConstruction.kMachine {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] :
                    LBA.Machine (KCell g₀) (KState g₀)

                    The simulating LBA: backward-reduce the input to the start symbol.

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

                      Decoding the work track #

                      formOf reads the sentential form represented on the tape: the non-blank work symbols, in cell order. The simulation invariant is phrased in terms of formOf.

                      source
                      def KurodaConstruction.formOf {T : Type} (g₀ : grammar T) {n : ℕ} (c : Fin (n + 1) → KGamma g₀) :
                      List (symbol T g₀.nt)

                      The sentential form represented by a tape's work track: the non-blank work symbols, in cell order.

                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem KurodaConstruction.formOf_def {T : Type} (g₀ : grammar T) {n : ℕ} (c : Fin (n + 1) → KGamma g₀) :
                        formOf g₀ c = List.filterMap (fun (γ : KGamma g₀) => γ.2.2) (List.ofFn c)
                        source
                        theorem KurodaConstruction.formOf_of_forall_some {T : Type} (g₀ : grammar T) {n : ℕ} (c : Fin (n + 1) → KGamma g₀) (f : Fin (n + 1) → symbol T g₀.nt) (h : ∀ (i : Fin (n + 1)), (c i).2.2 = some (f i)) :
                        formOf g₀ c = List.ofFn f

                        If every cell carries a (non-blank) work symbol given by f, the form is exactly ofFn f.

                        source
                        theorem KurodaConstruction.ofFn_update {α : Type u_1} {n : ℕ} (W : Fin (n + 1) → α) (i : Fin (n + 1)) (x : α) :
                        List.ofFn (Function.update W i x) = (List.ofFn W).set (↑i) x

                        Updating one value of a finite function corresponds to List.set on its ofFn list.

                        source
                        def KurodaConstruction.formW {T : Type} (g₀ : grammar T) {n : ℕ} (W : Fin (n + 1) → KWork g₀) :
                        List (symbol T g₀.nt)

                        The sentential form represented by a work function W (the marked tape is mkCell ∘ W): the non-blank work symbols, in order. This is what the simulation tracks: after init the tape is always mkCell ∘ W, and applyRule updates W.

                        Equations
                        Instances For
                          source
                          theorem KurodaConstruction.formW_of_forall_some {T : Type} (g₀ : grammar T) {n : ℕ} (W : Fin (n + 1) → KWork g₀) (f : Fin (n + 1) → symbol T g₀.nt) (h : ∀ (i : Fin (n + 1)), W i = some (f i)) :
                          formW g₀ W = List.ofFn f

                          If every work cell is non-blank (W i = some (f i)), the form is exactly ofFn f.

                          source
                          theorem KurodaConstruction.cons_getElem?_filterMap_drop {α : Type u_1} (L : List α) (i : ℕ) :
                          List.filterMap id [L[i]?] ++ List.drop (i + 1) L = List.drop i L

                          [L[i]?].filterMap id ++ L.drop (i+1) = L.drop i — peeling the i-th element of a list.

                          source
                          theorem KurodaConstruction.formW_split {T : Type} (g₀ : grammar T) {n : ℕ} (W : Fin (n + 1) → KWork g₀) (a : ℕ) :
                          formW g₀ W = List.filterMap id (List.take a (List.ofFn W)) ++ List.filterMap id (List.drop a (List.ofFn W))

                          The form decomposes along any tape split point: formW = filterMap(take a) ++ filterMap(drop a).

                          source
                          theorem KurodaConstruction.drop_filterMap_blank {T : Type} (g₀ : grammar T) {n : ℕ} (W : Fin (n + 1) → KWork g₀) (i : Fin (n + 1)) (hb : W i = none) :
                          List.filterMap id (List.drop (↑i) (List.ofFn W)) = List.filterMap id (List.drop (↑i + 1) (List.ofFn W))

                          Reading the non-blank tail at a blank cell: the blank contributes nothing.

                          source
                          theorem KurodaConstruction.drop_filterMap_some {T : Type} (g₀ : grammar T) {n : ℕ} (W : Fin (n + 1) → KWork g₀) (i : Fin (n + 1)) (s : symbol T g₀.nt) (hs : W i = some s) :
                          List.filterMap id (List.drop (↑i) (List.ofFn W)) = s :: List.filterMap id (List.drop (↑i + 1) (List.ofFn W))

                          Reading the non-blank tail at a symbol cell: the symbol is the head.

                          source
                          theorem KurodaConstruction.grammar_transforms_patList {T : Type} (g₀ : grammar T) {r : grule T g₀.nt} (hr : r ∈ g₀.rules) (u v : List (symbol T g₀.nt)) :
                          grammar_transforms g₀ (u ++ patList g₀ r ++ v) (u ++ r.output_string ++ v)

                          A backward rule-write output_string ↦ patList (in any context) is exactly one forward grammar step … patList … → … output_string …. The soundness invariant prepends this step.

                          Step-level glue #

                          source
                          @[simp]
                          theorem KurodaConstruction.kMachine_accept_iff {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] (s : KState g₀) :
                          (kMachine g₀).accept s = true ↔ s = KState.accept

                          The only accepting state is accept.

                          source
                          theorem KurodaConstruction.kStep_mk {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} {cfg : DLBA.Cfg (KCell g₀) (KState g₀) n} {q' : KState g₀} {a : KCell g₀} {d : DLBA.Dir} (hmem : (q', a, d) ∈ kTransition g₀ cfg.state cfg.tape.read) :
                          LBA.Step (kMachine g₀) cfg { state := q', tape := (cfg.tape.write a).moveHead d }

                          Build one Step of kMachine from a transition membership.

                          source
                          theorem KurodaConstruction.kAccepts_of_reaches {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} {cfg cfg' : DLBA.Cfg (KCell g₀) (KState g₀) n} (h : LBA.Reaches (kMachine g₀) cfg cfg') (hacc : cfg'.state = KState.accept) :
                          LBA.Accepts (kMachine g₀) cfg

                          Reaching an accept-state configuration witnesses acceptance.

                          source
                          theorem KurodaConstruction.kStep_echo_left {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} {c : Fin (n + 1) → KCell g₀} {i : Fin (n + 1)} {st st' : KState g₀} (hpos : 0 < ↑i) (hmem : (st', c i, DLBA.Dir.left) ∈ kTransition g₀ st (c i)) :
                          LBA.Step (kMachine g₀) { state := st, tape := { contents := c, head := i } } { state := st', tape := { contents := c, head := ⟨↑i - 1, ⋯⟩ } }

                          An echo step that moves the head left by one, leaving the tape contents unchanged (the transition rewrites the current cell to its own value).

                          source
                          theorem KurodaConstruction.kStep_echo_right {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} {c : Fin (n + 1) → KCell g₀} {i : Fin (n + 1)} {st st' : KState g₀} (hlt : ↑i < n) (hmem : (st', c i, DLBA.Dir.right) ∈ kTransition g₀ st (c i)) :
                          LBA.Step (kMachine g₀) { state := st, tape := { contents := c, head := i } } { state := st', tape := { contents := c, head := ⟨↑i + 1, ⋯⟩ } }

                          An echo step that moves the head right by one, leaving the tape contents unchanged.

                          source
                          theorem KurodaConstruction.kStep_echo_stay {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} {c : Fin (n + 1) → KCell g₀} {i : Fin (n + 1)} {st st' : KState g₀} (hmem : (st', c i, DLBA.Dir.stay) ∈ kTransition g₀ st (c i)) :
                          LBA.Step (kMachine g₀) { state := st, tape := { contents := c, head := i } } { state := st', tape := { contents := c, head := i } }

                          An echo step that keeps the head in place, leaving the tape contents unchanged.

                          source
                          def KurodaConstruction.Marked {T : Type} (g₀ : grammar T) {n : ℕ} (c : Fin (n + 1) → KCell g₀) :
                          Prop

                          The tape carries correct boundary markers: cell k records isLeftEnd = (k = 0) and isRightEnd = (k = n).

                          Equations
                          Instances For
                            source
                            theorem KurodaConstruction.gotoLeft_reaches {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} {c : Fin (n + 1) → KCell g₀} (hmark : Marked g₀ c) (i : Fin (n + 1)) :
                            LBA.Reaches (kMachine g₀) { state := KState.gotoLeft, tape := { contents := c, head := i } } { state := KState.check false, tape := { contents := c, head := 0 } }

                            The gotoLeft sweep: from any head position, echo-move left to the marked left end (cell 0) and enter the accept check.

                            source
                            def KurodaConstruction.mkCell {T : Type} (g₀ : grammar T) {n : ℕ} (k : Fin (n + 1)) (ws : KWork g₀) :
                            KCell g₀

                            A canonical marked work cell at position k carrying work symbol ws.

                            Equations
                            Instances For
                              source
                              theorem KurodaConstruction.marked_mkTape {T : Type} (g₀ : grammar T) {n : ℕ} (W : Fin (n + 1) → KWork g₀) :
                              Marked g₀ fun (k : Fin (n + 1)) => mkCell g₀ k (W k)

                              The canonical tape built from a work-symbol function is Marked.

                              source
                              theorem KurodaConstruction.update_mkCell {T : Type} (g₀ : grammar T) {n : ℕ} (W : Fin (n + 1) → KWork g₀) (i : Fin (n + 1)) (x : KWork g₀) :
                              Function.update (fun (k : Fin (n + 1)) => mkCell g₀ k (W k)) i (mkCell g₀ i x) = fun (k : Fin (n + 1)) => mkCell g₀ k (Function.update W i x k)

                              Updating one cell of a canonical tape with mkCell i x corresponds to updating the work function at i.

                              source
                              theorem KurodaConstruction.check_sweep {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (W : Fin (n + 1) → KWork g₀) (j : Fin (n + 1)) (hj : W j = some (symbol.nonterminal g₀.initial)) (hother : ∀ (k : Fin (n + 1)), k ≠ j → W k = none) (i : Fin (n + 1)) :
                              LBA.Reaches (kMachine g₀) { state := KState.check (decide (↑j < ↑i)), tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := i } } { state := KState.accept, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := Fin.last n } }

                              The accept-check sweep: if the work track spells exactly [S] (one cell j holds the start symbol, all others blank), the check started at any cell i (with the seen flag tracking whether j is behind i) reaches the accepting state.

                              source
                              theorem KurodaConstruction.accept_from_S {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (W : Fin (n + 1) → KWork g₀) (j : Fin (n + 1)) (hj : W j = some (symbol.nonterminal g₀.initial)) (hother : ∀ (k : Fin (n + 1)), k ≠ j → W k = none) (i : Fin (n + 1)) :
                              LBA.Accepts (kMachine g₀) { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := i } }

                              If the work track spells exactly [S], the simulator accepts (from any head position): roam to the left end and run the accept-check sweep.

                              The init conversion sweep #

                              source
                              def KurodaConstruction.tmpCell {T : Type} (g₀ : grammar T) {n : ℕ} (input : Fin (n + 1) → T) (k : Fin (n + 1)) :
                              KCell g₀

                              Cell k converted to a work cell holding terminal (input k), with isRightEnd = false (the right-end bit is set later, on the clamp).

                              Equations
                              Instances For
                                source
                                def KurodaConstruction.cAt {T : Type} (g₀ : grammar T) {n : ℕ} (input : Fin (n + 1) → T) (i : ℕ) (k : Fin (n + 1)) :
                                KCell g₀

                                The tape with cells < i converted, the rest still raw input some (Sum.inl _).

                                Equations
                                Instances For
                                  source
                                  theorem KurodaConstruction.cAt_update {T : Type} (g₀ : grammar T) {n : ℕ} (input : Fin (n + 1) → T) (i : Fin (n + 1)) :
                                  Function.update (cAt g₀ input ↑i) i (tmpCell g₀ input i) = cAt g₀ input (↑i + 1)

                                  Converting cell i updates cAt … i to cAt … (i+1).

                                  source
                                  theorem KurodaConstruction.kConvert_mem {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (input : Fin (n + 1) → T) (i : Fin (n + 1)) (hd0 : decide (↑i = 0) = false) (d : DLBA.Dir) :
                                  (KState.initSweep, tmpCell g₀ input i, d) ∈ kTransition g₀ KState.initSweep (cAt g₀ input (↑i) i) ↔ d = DLBA.Dir.right

                                  The transition-membership for converting an input cell i ≠ 0.

                                  source
                                  theorem KurodaConstruction.kStep_convert_right {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (input : Fin (n + 1) → T) (i : Fin (n + 1)) (hd0 : decide (↑i = 0) = false) (hlt : ↑i < n) :
                                  LBA.Step (kMachine g₀) { state := KState.initSweep, tape := { contents := cAt g₀ input ↑i, head := i } } { state := KState.initSweep, tape := { contents := cAt g₀ input (↑i + 1), head := ⟨↑i + 1, ⋯⟩ } }

                                  One conversion step (interior cell i ≠ 0, i < n): convert and move right.

                                  source
                                  theorem KurodaConstruction.kStep_convert_last {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (input : Fin (n + 1) → T) (i : Fin (n + 1)) (hd0 : decide (↑i = 0) = false) (hin : ↑i = n) :
                                  LBA.Step (kMachine g₀) { state := KState.initSweep, tape := { contents := cAt g₀ input ↑i, head := i } } { state := KState.initSweep, tape := { contents := cAt g₀ input (↑i + 1), head := i } }

                                  The last conversion step (cell n): convert; moving right clamps, staying at n.

                                  source
                                  theorem KurodaConstruction.convert_sweep {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (input : Fin (n + 1) → T) (i : Fin (n + 1)) :
                                  1 ≤ ↑i → LBA.Reaches (kMachine g₀) { state := KState.initSweep, tape := { contents := cAt g₀ input ↑i, head := i } } { state := KState.initSweep, tape := { contents := cAt g₀ input (n + 1), head := Fin.last n } }

                                  The conversion sweep: from cell i ≥ 1 (with cells < i converted), convert the rest of the input left-to-right, ending (after the right-end clamp) at the fully-converted tape on cell n.

                                  source
                                  theorem KurodaConstruction.cAt_full {T : Type} (g₀ : grammar T) {n : ℕ} (input : Fin (n + 1) → T) :
                                  cAt g₀ input (n + 1) = tmpCell g₀ input

                                  After converting all cells, cAt … (n+1) is the fully-converted tape.

                                  source
                                  theorem KurodaConstruction.cfg_eq {T : Type} (g₀ : grammar T) {n : ℕ} {s s' : KState g₀} {c c' : Fin (n + 1) → KCell g₀} {h h' : Fin (n + 1)} (hs : s = s') (hc : c = c') (hh : h = h') :
                                  { state := s, tape := { contents := c, head := h } } = { state := s', tape := { contents := c', head := h' } }

                                  Configuration equality from component equalities (no @[ext] on Cfg/BoundedTape).

                                  source
                                  theorem KurodaConstruction.init_to_tmpCell {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (input : Fin (n + 1) → T) :
                                  LBA.Reaches (kMachine g₀) { state := KState.init0, tape := { contents := cAt g₀ input 0, head := ⟨0, ⋯⟩ } } { state := KState.initSweep, tape := { contents := tmpCell g₀ input, head := Fin.last n } }

                                  The init phase up to the right-end clamp: from the raw input tape (state init0, head 0), reach the fully-converted (isRightEnd = false) tape at cell n.

                                  source
                                  theorem KurodaConstruction.init_reaches {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (input : Fin (n + 1) → T) :
                                  ∃ (h : Fin (n + 1)), LBA.Reaches (kMachine g₀) { state := KState.init0, tape := { contents := cAt g₀ input 0, head := ⟨0, ⋯⟩ } } { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (some (symbol.terminal (input k))), head := h } }

                                  The full init phase: from the raw input tape, reach the canonical marked work tape (state sim), whose work track holds terminal (input k) at every cell (so formOf = input.map).