Normal Form for Indexed Grammars

This file defines the normal form for indexed grammars following Aho (1968), and states the equivalence theorem that every indexed grammar can be converted to an equivalent one in normal form.

An indexed grammar is in normal form if:

1. The start symbol does not appear on the right-hand side of any production.
2. There are no ε-productions (except possibly S → ε).
3. Each production has one of the four forms:
   • A → BC (binary split, no flag consumed)
   • Af → B (flag consumption)
   • A → Bf (flag push)
   • A → a (terminal production)

References

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

def IndexedGrammar.IRule.IsNF {T N F : Type} [DecidableEq N] (r : IRule T N F) (s : N) : Prop

A production rule is in normal form with respect to a start symbol s if it has one of the four canonical forms:

• A → BC (binary split)
• Af → B (flag consumption)
• A → Bf (flag push)
• A → a (terminal production) and no nonterminal on the right-hand side is the start symbol s.

Equations

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

def IndexedGrammar.IsNormalForm {T : Type} (g : IndexedGrammar T) [DecidableEq g.nt] : Prop

An indexed grammar is in normal form if every production rule is in normal form with respect to the start symbol.

Equations

• g.IsNormalForm = ∀ r ∈ g.rules, IndexedGrammar.IRule.IsNF r g.initial