Normal Form for Indexed Grammars

This file assembles the normal form theorem for indexed grammars following Aho (1968).

An indexed grammar is in normal form if every production has one of the four forms:

1. A → BC — binary split, no flag consumed, no flag pushed
2. Af → B — flag consumption (pop)
3. A → Bf — flag push
4. A → a — terminal production

and the start symbol does not appear on the right-hand side of any production.

Main results

• IndexedGrammar.exists_normalForm_all — every ε-free indexed grammar has an equivalent grammar in normal form
• IndexedGrammar.exists_normalForm — compatibility wrapper for non-empty words
• IndexedGrammar.exists_finiteSupport_normalForm_nonempty — every indexed grammar has a finite-support normal-form grammar preserving all non-empty words

Proof outline

The proof proceeds by a sequence of language-preserving transformations:

1. Fresh start (FreshStart.lean, fully proved): introduce a new start symbol that does not appear on any right-hand side.
2. ε-free pass-through (EpsilonElim.lean): use the explicit ε-free hypothesis.
3. Terminal isolation (TerminalIsolation.lean, fully proved): replace terminals in multi-symbol right-hand sides with dedicated nonterminals.
4. Flag separation (FlagSeparation.lean): split rules with complex flag operations.
5. Binarization (Binarization.lean): replace right-hand sides of length ≥ 3 with chains of binary rules.

References

• A. V. Aho, "Indexed grammars — an extension of context-free grammars", JACM 15(4), 1968.

Aho's Normal Form Theorem

theorem IndexedGrammar.exists_terminalIsolated_flagsSeparated_all {T : Type} (g : IndexedGrammar T) : ∃ (g' : IndexedGrammar T), g'.TerminalsIsolated ∧ g'.FlagsSeparated ∧ (g.StartNotOnRhs' → g'.StartNotOnRhs') ∧ ∀ (w : List T), g'.Generates w ↔ g.Generates w

Before ε-elimination is available, any indexed grammar can still be made terminal-isolated and flag-separated without changing its language. This is the structural preprocessing target for the arbitrary-ε part of the normal-form construction.

theorem IndexedGrammar.exists_noEpsilon_of_exists_noEpsilon_terminalIsolated_flagsSeparated {T : Type} (helim : ∀ (g₀ : IndexedGrammar T), g₀.TerminalsIsolated → g₀.FlagsSeparated → ∃ (g' : IndexedGrammar T), g'.NoEpsilon' ∧ (g₀.StartNotOnRhs' → g'.StartNotOnRhs') ∧ ∀ (w : List T), w ≠ [] → (g'.Generates w ↔ g₀.Generates w)) (g : IndexedGrammar T) : ∃ (g' : IndexedGrammar T), g'.NoEpsilon' ∧ (g.StartNotOnRhs' → g'.StartNotOnRhs') ∧ ∀ (w : List T), w ≠ [] → (g'.Generates w ↔ g.Generates w)

It is enough to prove ε-elimination after terminal isolation and flag separation. The preprocessing is language-preserving and can be run before the ε-free invariant exists.

theorem IndexedGrammar.exists_noEpsilon_preserving_nonempty {T : Type} (g : IndexedGrammar T) : ∃ (g' : IndexedGrammar T), g'.NoEpsilon' ∧ ∀ (w : List T), w ≠ [] → (g'.Generates w ↔ g.Generates w)

Every indexed grammar has an ε-free grammar preserving all non-empty generated words.

The construction first makes the grammar flag-separated, restricts to finite support, and then applies the exact finite nullable-summary ε-elimination.

theorem IndexedGrammar.exists_normalForm_all {T : Type} [Inhabited T] (g : IndexedGrammar T) (hne : g.NoEpsilon') : ∃ (g' : IndexedGrammar T), (∃ (x : DecidableEq g'.nt), g'.IsNormalForm) ∧ ∀ (w : List T), g'.Generates w ↔ g.Generates w

Normal-form theorem for ε-free indexed grammars. For every indexed grammar g with no ε-productions, there exists an indexed grammar g' in normal form such that g' generates exactly the same words as g.

theorem IndexedGrammar.exists_normalForm {T : Type} [Inhabited T] (g : IndexedGrammar T) (hne : g.NoEpsilon') : ∃ (g' : IndexedGrammar T), (∃ (x : DecidableEq g'.nt), g'.IsNormalForm) ∧ ∀ (w : List T), w ≠ [] → (g'.Generates w ↔ g.Generates w)

Compatibility form of the normal-form theorem, preserving all non-empty words.

theorem IndexedGrammar.exists_finiteSupport_normalForm_all {T : Type} [Inhabited T] (g : IndexedGrammar T) (hne : g.NoEpsilon') : ∃ (g' : IndexedGrammar T) (x : Fintype g'.nt) (x : Fintype g'.flag) (x : DecidableEq g'.nt), g'.IsNormalForm ∧ ∀ (w : List T), g'.Generates w ↔ g.Generates w

Every ε-free indexed grammar has a finite-support normal-form grammar preserving all generated words.

theorem IndexedGrammar.exists_finiteSupport_normalForm {T : Type} [Inhabited T] (g : IndexedGrammar T) (hne : g.NoEpsilon') : ∃ (g' : IndexedGrammar T) (x : Fintype g'.nt) (x : Fintype g'.flag) (x : DecidableEq g'.nt), g'.IsNormalForm ∧ ∀ (w : List T), w ≠ [] → (g'.Generates w ↔ g.Generates w)

Compatibility form of the finite-support normal-form theorem, preserving all non-empty generated words.

theorem IndexedGrammar.exists_finiteSupport_normalForm_nonempty {T : Type} [Inhabited T] (g : IndexedGrammar T) : ∃ (g' : IndexedGrammar T) (x : Fintype g'.nt) (x : Fintype g'.flag) (x : DecidableEq g'.nt), g'.IsNormalForm ∧ ∀ (w : List T), w ≠ [] → (g'.Generates w ↔ g.Generates w)

Every indexed grammar has a finite-support normal-form grammar preserving all non-empty generated words. The empty word is intentionally omitted: normal-form grammars are ε-free.