LanglibThe finite normal-form indexed-to-LBA core #
This module joins the grammar semantics of Aho's machine to its executable certified-row implementation. The only hypothesis below is the parse scheduler's uniform linear bound.
theorem
IndexedGrammar.Aho.is_LBA_pos_language_of_bounded_complete
{T : Type}
{g : IndexedGrammar T}
[Fintype T]
[DecidableEq T]
[Fintype g.nt]
[Fintype g.flag]
[DecidableEq g.nt]
(hNF : g.IsNormalForm)
(hcomplete :
∀ {input : List T} (a : g.NFParse g.initial [] input),
BoundedReaches g input (21 * input.length) (initialConfig g) (finalConfig g input.length))
:
A uniform twenty-one-slots-per-terminal scheduler turns the language of a finite normal-form indexed grammar into an input-sized LBA language.
theorem
IndexedGrammar.Aho.is_LBA_pos_language
{T : Type}
{g : IndexedGrammar T}
[Fintype T]
[DecidableEq T]
[Fintype g.nt]
[Fintype g.flag]
[DecidableEq g.nt]
(hNF : g.IsNormalForm)
:
Every finite normal-form indexed grammar is recognized by a positive-input LBA. The proof
combines the uniform complete_bounded schedule with certified-row exactness and compilation.