Fresh Start Symbol for Indexed Grammars

This file proves that every indexed grammar can be transformed into one whose start symbol does not appear on the right-hand side of any production rule, while preserving the generated language.

This is Step 1 of Aho's Normal Form theorem for indexed grammars.

References

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

Lifting functions

def IndexedGrammar.liftRhsSym {T : Type} (g : IndexedGrammar T) : IRhsSymbol T g.nt g.flag → IRhsSymbol T (Option g.nt) g.flag

Lift an RHS symbol to the Option nonterminal type.

Equations

• g.liftRhsSym (IRhsSymbol.terminal t) = IRhsSymbol.terminal t
• g.liftRhsSym (IRhsSymbol.nonterminal n f) = IRhsSymbol.nonterminal (some n) f

def IndexedGrammar.liftRule {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) : IRule T (Option g.nt) g.flag

Lift a production rule to the Option nonterminal type.

Equations

• g.liftRule r = { lhs := some r.lhs, consume := r.consume, rhs := List.map g.liftRhsSym r.rhs }

def IndexedGrammar.freshStart {T : Type} (g : IndexedGrammar T) : IndexedGrammar T

The grammar with a fresh start symbol none : Option g.nt. Has one start rule S' → S (where S' = none, S = some g.initial) and all original rules lifted.

Equations

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

def IndexedGrammar.liftISym {T : Type} (g : IndexedGrammar T) : g.ISym → g.freshStart.ISym

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

Equations

• g.liftISym (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal t
• g.liftISym (IndexedGrammar.ISym.indexed n σ) = IndexedGrammar.ISym.indexed (some n) σ

Key helper: expandRhs commutes with lifting

theorem IndexedGrammar.expandRhs_liftRhsSym {T : Type} (g : IndexedGrammar T) (rhs : List (IRhsSymbol T g.nt g.flag)) (σ : List g.flag) : List.map g.liftISym (g.expandRhs rhs σ) = g.freshStart.expandRhs (List.map g.liftRhsSym rhs) σ

theorem IndexedGrammar.map_liftISym_terminal {T : Type} (g : IndexedGrammar T) (w : List T) : List.map ISym.terminal w = List.map g.liftISym (List.map ISym.terminal w)

Forward direction: g.Language ⊆ (freshStart g).Language

theorem IndexedGrammar.freshStart_lift_transforms {T : Type} (g : IndexedGrammar T) {w₁ w₂ : List g.ISym} (h : g.Transforms w₁ w₂) : g.freshStart.Transforms (List.map g.liftISym w₁) (List.map g.liftISym w₂)

theorem IndexedGrammar.freshStart_lift_derives {T : Type} (g : IndexedGrammar T) {w₁ w₂ : List g.ISym} (h : g.Derives w₁ w₂) : g.freshStart.Derives (List.map g.liftISym w₁) (List.map g.liftISym w₂)

theorem IndexedGrammar.freshStart_language_forward {T : Type} (g : IndexedGrammar T) {w : List T} (h : w ∈ g.Language) : w ∈ g.freshStart.Language

Backward direction: (freshStart g).Language ⊆ g.Language

def IndexedGrammar.Proper {T : Type} (g : IndexedGrammar T) (w : List g.freshStart.ISym) : Prop

A sentential form of freshStart g is "proper" if it contains no occurrence of the fresh start symbol none.

Equations

• g.Proper w = ∀ s ∈ w, ∀ (σ : List g.freshStart.flag), s ≠ IndexedGrammar.ISym.indexed none σ

theorem IndexedGrammar.proper_of_map_liftISym {T : Type} (g : IndexedGrammar T) (w : List g.ISym) : g.Proper (List.map g.liftISym w)

theorem IndexedGrammar.proper_of_proper_transforms {T : Type} (g : IndexedGrammar T) {w₁ w₂ : List g.freshStart.ISym} (hp : g.Proper w₁) (ht : g.freshStart.Transforms w₁ w₂) : g.Proper w₂

theorem IndexedGrammar.proper_of_proper_derives {T : Type} (g : IndexedGrammar T) {w₁ w₂ : List g.freshStart.ISym} (hp : g.Proper w₁) (hd : g.freshStart.Derives w₁ w₂) : g.Proper w₂

noncomputable def IndexedGrammar.unliftISym {T : Type} (g : IndexedGrammar T) [Inhabited T] : g.freshStart.ISym → g.ISym

Unlift a sentential-form symbol. For proper forms, this is the inverse of liftISym.

Equations

• g.unliftISym (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal t
• g.unliftISym (IndexedGrammar.ISym.indexed (some n) σ) = IndexedGrammar.ISym.indexed n σ
• g.unliftISym (IndexedGrammar.ISym.indexed none a) = IndexedGrammar.ISym.terminal default

noncomputable def IndexedGrammar.unliftSF {T : Type} (g : IndexedGrammar T) [Inhabited T] (w : List g.freshStart.ISym) : List g.ISym

Unlift a proper sentential form.

Equations

• g.unliftSF w = List.map g.unliftISym w

theorem IndexedGrammar.unlift_lift {T : Type} (g : IndexedGrammar T) [Inhabited T] (s : g.ISym) : g.unliftISym (g.liftISym s) = s

theorem IndexedGrammar.unliftSF_map_liftISym {T : Type} (g : IndexedGrammar T) [Inhabited T] (w : List g.ISym) : g.unliftSF (List.map g.liftISym w) = w

theorem IndexedGrammar.freshStart_unlift_transforms {T : Type} (g : IndexedGrammar T) [Inhabited T] {w₁ w₂ : List g.freshStart.ISym} (hp : g.Proper w₁) (ht : g.freshStart.Transforms w₁ w₂) : g.Transforms (g.unliftSF w₁) (g.unliftSF w₂)

theorem IndexedGrammar.freshStart_unlift_derives {T : Type} (g : IndexedGrammar T) [Inhabited T] {w₁ w₂ : List g.freshStart.ISym} (hp : g.Proper w₁) (hd : g.freshStart.Derives w₁ w₂) : g.Derives (g.unliftSF w₁) (g.unliftSF w₂)

theorem IndexedGrammar.freshStart_first_step {T : Type} (g : IndexedGrammar T) {w : List g.freshStart.ISym} (ht : g.freshStart.Transforms [ISym.indexed none []] w) : w = [ISym.indexed (some g.initial) []]

theorem IndexedGrammar.unliftSF_terminal {T : Type} (g : IndexedGrammar T) [Inhabited T] (w : List T) : g.unliftSF (List.map ISym.terminal w) = List.map ISym.terminal w

theorem IndexedGrammar.freshStart_language_backward {T : Type} (g : IndexedGrammar T) [Inhabited T] {w : List T} (h : w ∈ g.freshStart.Language) : w ∈ g.Language

Main result

theorem IndexedGrammar.freshStart_language {T : Type} (g : IndexedGrammar T) [Inhabited T] : g.freshStart.Language = g.Language

The fresh-start grammar generates the same language as the original.

theorem IndexedGrammar.freshStart_startNotOnRhs {T : Type} (g : IndexedGrammar T) : g.freshStart.StartNotOnRhs'

theorem IndexedGrammar.freshStart_noEpsilon {T : Type} (g : IndexedGrammar T) (hne : g.NoEpsilon') : g.freshStart.NoEpsilon'

Adding a fresh start symbol preserves the absence of ε-productions.