Terminal Isolation for Indexed Grammars

This file constructs a terminal-isolation transformation for indexed grammars. Given an indexed grammar with no ε-productions, it produces an equivalent grammar where every rule's RHS is either a single terminal or consists entirely of nonterminals.

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

def IndexedGrammar.tiLiftRhsSym {T : Type} (g : IndexedGrammar T) : IRhsSymbol T g.nt g.flag → IRhsSymbol T (g.nt ⊕ T) g.flag

Transform an RHS symbol by replacing terminals with fresh nonterminals.

Equations

• g.tiLiftRhsSym (IRhsSymbol.terminal t) = IRhsSymbol.nonterminal (Sum.inr t) none
• g.tiLiftRhsSym (IRhsSymbol.nonterminal n f) = IRhsSymbol.nonterminal (Sum.inl n) f

def IndexedGrammar.tiEmbedRhsSym {T : Type} (g : IndexedGrammar T) : IRhsSymbol T g.nt g.flag → IRhsSymbol T (g.nt ⊕ T) g.flag

Transform an RHS symbol for the identity embedding (no terminal replacement).

Equations

• g.tiEmbedRhsSym (IRhsSymbol.terminal t) = IRhsSymbol.terminal t
• g.tiEmbedRhsSym (IRhsSymbol.nonterminal n f) = IRhsSymbol.nonterminal (Sum.inl n) f

def IndexedGrammar.collectTerminals {T : Type} (g : IndexedGrammar T) : List T

Collect all terminals appearing in all rules' RHS.

Equations

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

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

The terminal-isolation grammar. Every terminal in a rule's RHS is replaced with a fresh nonterminal Sum.inr t, and for each such terminal a rule Sum.inr t → t is added.

Equations

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

Properties of the construction

theorem IndexedGrammar.termIsolate_noEpsilon {T : Type} (g : IndexedGrammar T) (hne : g.NoEpsilon') : g.termIsolate.NoEpsilon'

theorem IndexedGrammar.termIsolate_terminalsIsolated {T : Type} (g : IndexedGrammar T) : g.termIsolate.TerminalsIsolated

theorem IndexedGrammar.termIsolate_startNotOnRhs {T : Type} (g : IndexedGrammar T) (hfresh : g.StartNotOnRhs') : g.termIsolate.StartNotOnRhs'

Lifting/projection for sentential forms

def IndexedGrammar.tiLiftISym {T : Type} (g : IndexedGrammar T) : g.ISym → g.termIsolate.ISym

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

Equations

• g.tiLiftISym (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal t
• g.tiLiftISym (IndexedGrammar.ISym.indexed n σ) = IndexedGrammar.ISym.indexed (Sum.inl n) σ

def IndexedGrammar.tiProjISym {T : Type} (g : IndexedGrammar T) : g.termIsolate.ISym → g.ISym

Project a sentential-form symbol from termIsolate g to g, sending Sum.inr t to terminal t.

Equations

• g.tiProjISym (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal t
• g.tiProjISym (IndexedGrammar.ISym.indexed (Sum.inl n) σ) = IndexedGrammar.ISym.indexed n σ
• g.tiProjISym (IndexedGrammar.ISym.indexed (Sum.inr t) a) = IndexedGrammar.ISym.terminal t

theorem IndexedGrammar.tiProjISym_tiLiftISym {T : Type} (g : IndexedGrammar T) (s : g.ISym) : g.tiProjISym (g.tiLiftISym s) = s

theorem IndexedGrammar.tiProjISym_terminal {T : Type} (g : IndexedGrammar T) (t : T) : g.tiProjISym (ISym.terminal t) = ISym.terminal t

Forward direction: g.Generates w → termIsolate.Generates w

theorem IndexedGrammar.termIsolate_inr_derives_terminal {T : Type} (g : IndexedGrammar T) (t : T) (ht : t ∈ g.collectTerminals) : g.termIsolate.Derives [ISym.indexed (Sum.inr t) []] [ISym.terminal t]

theorem IndexedGrammar.terminal_in_collectTerminals {T : Type} (g : IndexedGrammar T) {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) {t : T} (ht : IRhsSymbol.terminal t ∈ r.rhs) : t ∈ g.collectTerminals

theorem IndexedGrammar.termIsolate_resolve_inr {T : Type} (g : IndexedGrammar T) (rhs : List (IRhsSymbol T g.nt g.flag)) (σ : List g.flag) (r : IRule T g.nt g.flag) (hr : r ∈ g.rules) (hrhs : rhs = r.rhs) : g.termIsolate.Derives (g.termIsolate.expandRhs (List.map g.tiLiftRhsSym rhs) σ) (List.map g.tiLiftISym (g.expandRhs rhs σ))

theorem IndexedGrammar.termIsolate_lift_transforms {T : Type} (g : IndexedGrammar T) {w₁ w₂ : List g.ISym} (h : g.Transforms w₁ w₂) : g.termIsolate.Derives (List.map g.tiLiftISym w₁) (List.map g.tiLiftISym w₂)

theorem IndexedGrammar.termIsolate_lift_derives {T : Type} (g : IndexedGrammar T) {w₁ w₂ : List g.ISym} (h : g.Derives w₁ w₂) : g.termIsolate.Derives (List.map g.tiLiftISym w₁) (List.map g.tiLiftISym w₂)

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

theorem IndexedGrammar.termIsolate_language_forward {T : Type} (g : IndexedGrammar T) {w : List T} (h : g.Generates w) : g.termIsolate.Generates w

Backward direction: termIsolate.Generates w → g.Generates w

def IndexedGrammar.tiProjSF {T : Type} (g : IndexedGrammar T) : List g.termIsolate.ISym → List g.ISym

Project a sentential form.

Equations

• g.tiProjSF = List.map g.tiProjISym

def IndexedGrammar.TIResolved {T : Type} (g : IndexedGrammar T) (w : List g.termIsolate.ISym) : Prop

A sentential form is "resolved" if it contains no Sum.inr nonterminals.

Equations

• g.TIResolved w = ∀ s ∈ w, ∀ (t : T) (σ : List g.termIsolate.flag), s ≠ IndexedGrammar.ISym.indexed (Sum.inr t) σ

theorem IndexedGrammar.tiResolved_terminals {T : Type} (g : IndexedGrammar T) (w : List T) : g.TIResolved (List.map ISym.terminal w)

theorem IndexedGrammar.tiProjSF_expandRhs_transformed {T : Type} (g : IndexedGrammar T) (r : IRule T g.nt g.flag) (σ : List g.flag) : g.tiProjSF (g.termIsolate.expandRhs (List.map g.tiLiftRhsSym r.rhs) σ) = g.expandRhs r.rhs σ

theorem IndexedGrammar.termIsolate_proj_transforms {T : Type} (g : IndexedGrammar T) {w₁ w₂ : List g.termIsolate.ISym} (ht : g.termIsolate.Transforms w₁ w₂) : g.Derives (g.tiProjSF w₁) (g.tiProjSF w₂)

theorem IndexedGrammar.termIsolate_proj_derives {T : Type} (g : IndexedGrammar T) {w₁ w₂ : List g.termIsolate.ISym} (hd : g.termIsolate.Derives w₁ w₂) : g.Derives (g.tiProjSF w₁) (g.tiProjSF w₂)

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

theorem IndexedGrammar.termIsolate_language_backward {T : Type} (g : IndexedGrammar T) {w : List T} (h : g.termIsolate.Generates w) : g.Generates w

theorem IndexedGrammar.termIsolate_generates_iff {T : Type} (g : IndexedGrammar T) (w : List T) : g.termIsolate.Generates w ↔ g.Generates w

Main result

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

Terminal isolation preserves the language of any indexed grammar. This unconditional packaging is used by the arbitrary-ε pipeline before the ε-free invariant is available.

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

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