Context-Sensitive Grammar → LBA (Kuroda's Construction)

This is the capstone of the CS → LBA direction. It assembles the two-way correctness of the backward-simulating LBA kMachine g₀ (built in CSGToLBA/Construction.lean, proven complete in CSGToLBA/Completeness.lean and sound in CSGToLBA/Soundness.lean) into the core statement noncontracting_finite_to_LBA: a non-contracting grammar with finitely many nonterminals is recognised by a nondeterministic LBA on a tape of exactly |w| cells.

The empty-word bookkeeping and the reduction from an arbitrary context-sensitive grammar are done in Equivalence/ContextSensitive.lean.

References

• Kuroda, S.-Y. (1964), "Classes of languages and linear-bounded automata".
• Hopcroft, Motwani, Ullman, Introduction to Automata Theory, Languages, and Computation, Chapter 9.

theorem KurodaConstruction.noncontracting_finite_to_LBA {T : Type} [Fintype T] [DecidableEq T] (g₀ : grammar T) (hfin : Finite g₀.nt) (hnc : grammar_noncontracting g₀) : ∃ (Γ : Type) (Λ : Type) (x : Fintype Γ) (x : Fintype Λ) (x : DecidableEq Γ) (x : DecidableEq Λ) (M : LBA.Machine (Option (T ⊕ Γ)) Λ), (LBA.LanguageViaEmbed M fun (t : T) => some (Sum.inl t)) = grammar_language g₀