Greibach normal form

DefinitionGreibach normal form#✓fully proved

A grammar is in Greibach normal form when every production has output either a single terminal followed by nonterminals, or the empty word with the initial nonterminal on the left; and either the initial nonterminal occurs in no output (so an empty production cannot leak the empty word to other nonterminals) or there are no empty outputs at all.

def IsGreibachNormalForm (g : ContextFreeGrammar T) : Prop :=
  (∀ r ∈ g.rules,
    (r.output = [] ∧ r.input = g.initial) ∨
      ∃ (a : T) (α : List g.NT),
        r.output = Symbol.terminal a :: α.map Symbol.nonterminal) ∧
  ((∀ r ∈ g.rules, Symbol.nonterminal g.initial ∉ r.output) ∨
    ∀ r ∈ g.rules, r.output ≠ [])

Sources

• Hopcroft and Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, 1979, Chapter 7 (Greibach normal form); Harrison, Introduction to Formal Language Theory, Addison-Wesley, 1978, Chapter 4.

Used by 1

Used byNonempty Greibach productions begin with a terminal

TheoremNonempty Greibach productions begin with a terminal#✓fully proved

In Greibach normal form, every nonempty production output begins with a terminal followed by nonterminals.

theorem exists_terminal_head_of_output_ne_nil
    (hg : IsGreibachNormalForm g) {r : ContextFreeRule T g.NT}
    (hr : r ∈ g.rules) (hne : r.output ≠ []) :
    ∃ (a : T) (α : List g.NT),
      r.output = Symbol.terminal a :: α.map Symbol.nonterminal

Sources

• Hopcroft and Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, 1979, Chapter 7 (Greibach normal form); Harrison, Introduction to Formal Language Theory, Addison-Wesley, 1978, Chapter 4.

Uses 1

Statement usesGreibach normal form

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.