Binarization for Indexed Grammars

This file constructs a binarization transformation for indexed grammars. Given an indexed grammar with no ε-productions, isolated terminals, separated flags, and a fresh start symbol, it produces an equivalent grammar in normal form.

This is Step 5 of Aho's Normal Form theorem.

def IndexedGrammar.binLiftRhsSym {T : Type} (g : IndexedGrammar T) : IRhsSymbol T g.nt g.flag → IRhsSymbol T (g.nt ⊕ ℕ × ℕ) (Option g.flag)

Lift an RHS symbol to the binarized grammar's nonterminal type.

Equations

• g.binLiftRhsSym (IRhsSymbol.terminal t) = IRhsSymbol.terminal t
• g.binLiftRhsSym (IRhsSymbol.nonterminal n f) = IRhsSymbol.nonterminal (Sum.inl n) (Option.map some f)

noncomputable def IndexedGrammar.binarizeChain {T : Type} (g : IndexedGrammar T) (i : ℕ) (lhs : g.nt ⊕ ℕ × ℕ) (syms : List (IRhsSymbol T (g.nt ⊕ ℕ × ℕ) (Option g.flag))) (idx : ℕ) : List (IRule T (g.nt ⊕ ℕ × ℕ) (Option g.flag))

The auxiliary binarization function.

Equations

• g.binarizeChain i lhs [] idx = []
• g.binarizeChain i lhs [s₁, s₂] idx = [{ lhs := lhs, consume := none, rhs := [s₁, s₂] }]
• g.binarizeChain i lhs (s :: rest) idx = { lhs := lhs, consume := none, rhs := [s, IRhsSymbol.nonterminal (Sum.inr (i, idx)) none] } :: g.binarizeChain i (Sum.inr (i, idx)) rest (idx + 1)

noncomputable def IndexedGrammar.binSingleRule {T : Type} (g : IndexedGrammar T) (i : ℕ) (r : IRule T g.nt g.flag) : List (IRule T (g.nt ⊕ ℕ × ℕ) (Option g.flag))

Binarize a single rule at index i.

Equations

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

noncomputable def IndexedGrammar.binarize {T : Type} (g : IndexedGrammar T) : IndexedGrammar T

The binarized grammar.

Equations

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

Classification of rules under hypotheses

Helper lemmas for IsNormalForm

theorem IndexedGrammar.binarize_isNormalForm {T : Type} (g : IndexedGrammar T) (hne : g.NoEpsilon') (hti : g.TerminalsIsolated) (hfs : g.FlagsSeparated) (hfresh : g.StartNotOnRhs') : ∃ (x : DecidableEq g.binarize.nt), g.binarize.IsNormalForm

Helper lemmas for generates_iff

def IndexedGrammar.liftBinISym {T : Type} (g : IndexedGrammar T) : g.ISym → g.binarize.ISym

Lift a sentential-form symbol from g to g.binarize.

Equations

• g.liftBinISym (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal t
• g.liftBinISym (IndexedGrammar.ISym.indexed n σ) = IndexedGrammar.ISym.indexed (Sum.inl n) (List.map some σ)

Backward direction: g.binarize generates w → g generates w

def IndexedGrammar.stripStack {T : Type} (g : IndexedGrammar T) : List (Option g.flag) → List g.flag

Strip none values from a flag stack, recovering a stack for the original grammar.

Equations

• g.stripStack = List.filterMap id

noncomputable def IndexedGrammar.unbinarizeSym {T : Type} (g : IndexedGrammar T) : g.binarize.ISym → List g.ISym

Unbinarize a single sentential-form symbol. Maps:

• terminal t to [terminal t]
• indexed (Sum.inl n) σ to [indexed n (stripStack σ)]
• indexed (Sum.inr (i, j)) σ to the remaining nonterminals of the i-th rule from position j+1 onward, each with stack stripStack σ.

Equations

• One or more equations did not get rendered due to their size.
• g.unbinarizeSym (IndexedGrammar.ISym.terminal t) = [IndexedGrammar.ISym.terminal t]
• g.unbinarizeSym (IndexedGrammar.ISym.indexed (Sum.inl n) σ) = [IndexedGrammar.ISym.indexed n (g.stripStack σ)]

noncomputable def IndexedGrammar.unbinarizeSF {T : Type} (g : IndexedGrammar T) (w : List g.binarize.ISym) : List g.ISym

Unbinarize a sentential form by flatMapping each symbol.

Equations

• g.unbinarizeSF w = List.flatMap g.unbinarizeSym w

Main theorems

theorem IndexedGrammar.binarize_generates_iff {T : Type} (g : IndexedGrammar T) (hne : g.NoEpsilon') (hti : g.TerminalsIsolated) (hfs : g.FlagsSeparated) (hfresh : g.StartNotOnRhs') (w : List T) : w ≠ [] → (g.binarize.Generates w ↔ g.Generates w)

theorem IndexedGrammar.binarize_generates_iff_all {T : Type} (g : IndexedGrammar T) (hne : g.NoEpsilon') (hti : g.TerminalsIsolated) (hfs : g.FlagsSeparated) (hfresh : g.StartNotOnRhs') (w : List T) : g.binarize.Generates w ↔ g.Generates w

theorem IndexedGrammar.exists_normalForm_from_separated {T : Type} (g : IndexedGrammar T) (hne : g.NoEpsilon') (hti : g.TerminalsIsolated) (hfs : g.FlagsSeparated) (hfresh : g.StartNotOnRhs') : ∃ (g' : IndexedGrammar T), (∃ (x : DecidableEq g'.nt), g'.IsNormalForm) ∧ ∀ (w : List T), g'.Generates w ↔ g.Generates w

theorem IndexedGrammar.exists_normalForm_from_separated' {T : Type} (g : IndexedGrammar T) (hne : g.NoEpsilon') (hti : g.TerminalsIsolated) (hfs : g.FlagsSeparated) (hfresh : g.StartNotOnRhs') : ∃ (g' : IndexedGrammar T), (∃ (x : DecidableEq g'.nt), g'.IsNormalForm) ∧ ∀ (w : List T), w ≠ [] → (g'.Generates w ↔ g.Generates w)