Indexed Languages Are Closed Under Union

Given indexed grammars g₁ and g₂, we construct an indexed grammar whose language is g₁.Language ∪ g₂.Language.

The construction introduces a fresh start symbol with two rules that jump to the respective initial symbols of g₁ and g₂.

Proof idea: lift the nonterminals and flags of the two grammars into disjoint summands and add one fresh start symbol. The only first step chooses the left or right grammar, and the lifting lemmas identify the resulting derivations with the original component derivations.

Main declarations

• Indexed_of_Indexed_u_Indexed

inductive UnionNT (N₁ N₂ : Type) : Type

The combined nonterminal type for the union grammar.

• start {N₁ N₂ : Type} : UnionNT N₁ N₂
• inl {N₁ N₂ : Type} : N₁ → UnionNT N₁ N₂
• inr {N₁ N₂ : Type} : N₂ → UnionNT N₁ N₂

inductive UnionFlag (F₁ F₂ : Type) : Type

The combined flag type for the union grammar.

• inl {F₁ F₂ : Type} : F₁ → UnionFlag F₁ F₂
• inr {F₁ F₂ : Type} : F₂ → UnionFlag F₁ F₂

def liftRhs1 {T N₁ N₂ F₁ F₂ : Type} : IRhsSymbol T N₁ F₁ → IRhsSymbol T (UnionNT N₁ N₂) (UnionFlag F₁ F₂)

Equations

• liftRhs1 (IRhsSymbol.terminal t) = IRhsSymbol.terminal t
• liftRhs1 (IRhsSymbol.nonterminal n none) = IRhsSymbol.nonterminal (UnionNT.inl n) none
• liftRhs1 (IRhsSymbol.nonterminal n (some f)) = IRhsSymbol.nonterminal (UnionNT.inl n) (some (UnionFlag.inl f))

def liftRhs2 {T N₁ N₂ F₁ F₂ : Type} : IRhsSymbol T N₂ F₂ → IRhsSymbol T (UnionNT N₁ N₂) (UnionFlag F₁ F₂)

Equations

• liftRhs2 (IRhsSymbol.terminal t) = IRhsSymbol.terminal t
• liftRhs2 (IRhsSymbol.nonterminal n none) = IRhsSymbol.nonterminal (UnionNT.inr n) none
• liftRhs2 (IRhsSymbol.nonterminal n (some f)) = IRhsSymbol.nonterminal (UnionNT.inr n) (some (UnionFlag.inr f))

def liftRule1 {T N₁ N₂ F₁ F₂ : Type} (r : IRule T N₁ F₁) : IRule T (UnionNT N₁ N₂) (UnionFlag F₁ F₂)

Equations

• liftRule1 r = { lhs := UnionNT.inl r.lhs, consume := Option.map UnionFlag.inl r.consume, rhs := List.map liftRhs1 r.rhs }

def liftRule2 {T N₁ N₂ F₁ F₂ : Type} (r : IRule T N₂ F₂) : IRule T (UnionNT N₁ N₂) (UnionFlag F₁ F₂)

Equations

• liftRule2 r = { lhs := UnionNT.inr r.lhs, consume := Option.map UnionFlag.inr r.consume, rhs := List.map liftRhs2 r.rhs }

def indexed_union {T : Type} (g₁ g₂ : IndexedGrammar T) : IndexedGrammar T

Indexed grammar for the union of two indexed languages.

Equations

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

def liftISym1 {T : Type} (g₁ g₂ : IndexedGrammar T) : g₁.ISym → (indexed_union g₁ g₂).ISym

Equations

• liftISym1 g₁ g₂ (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal t
• liftISym1 g₁ g₂ (IndexedGrammar.ISym.indexed n σ) = IndexedGrammar.ISym.indexed (UnionNT.inl n) (List.map UnionFlag.inl σ)

def liftISym2 {T : Type} (g₁ g₂ : IndexedGrammar T) : g₂.ISym → (indexed_union g₁ g₂).ISym

Equations

• liftISym2 g₁ g₂ (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal t
• liftISym2 g₁ g₂ (IndexedGrammar.ISym.indexed n σ) = IndexedGrammar.ISym.indexed (UnionNT.inr n) (List.map UnionFlag.inr σ)

theorem lift1_expandRhs {T : Type} (g₁ g₂ : IndexedGrammar T) (rhs : List (IRhsSymbol T g₁.nt g₁.flag)) (σ : List g₁.flag) : List.map (liftISym1 g₁ g₂) (g₁.expandRhs rhs σ) = (indexed_union g₁ g₂).expandRhs (List.map liftRhs1 rhs) (List.map UnionFlag.inl σ)

theorem lift2_expandRhs {T : Type} (g₁ g₂ : IndexedGrammar T) (rhs : List (IRhsSymbol T g₂.nt g₂.flag)) (σ : List g₂.flag) : List.map (liftISym2 g₁ g₂) (g₂.expandRhs rhs σ) = (indexed_union g₁ g₂).expandRhs (List.map liftRhs2 rhs) (List.map UnionFlag.inr σ)

theorem lift1_tran {T : Type} (g₁ g₂ : IndexedGrammar T) {w₁ w₂ : List g₁.ISym} (h : g₁.Transforms w₁ w₂) : (indexed_union g₁ g₂).Transforms (List.map (liftISym1 g₁ g₂) w₁) (List.map (liftISym1 g₁ g₂) w₂)

theorem lift2_tran {T : Type} (g₁ g₂ : IndexedGrammar T) {w₁ w₂ : List g₂.ISym} (h : g₂.Transforms w₁ w₂) : (indexed_union g₁ g₂).Transforms (List.map (liftISym2 g₁ g₂) w₁) (List.map (liftISym2 g₁ g₂) w₂)

theorem lift1_deri {T : Type} (g₁ g₂ : IndexedGrammar T) {w₁ w₂ : List g₁.ISym} (h : g₁.Derives w₁ w₂) : (indexed_union g₁ g₂).Derives (List.map (liftISym1 g₁ g₂) w₁) (List.map (liftISym1 g₁ g₂) w₂)

theorem lift2_deri {T : Type} (g₁ g₂ : IndexedGrammar T) {w₁ w₂ : List g₂.ISym} (h : g₂.Derives w₁ w₂) : (indexed_union g₁ g₂).Derives (List.map (liftISym2 g₁ g₂) w₁) (List.map (liftISym2 g₁ g₂) w₂)

theorem union_generates_left {T : Type} (g₁ g₂ : IndexedGrammar T) (w : List T) (h : g₁.Generates w) : (indexed_union g₁ g₂).Generates w

theorem union_generates_right {T : Type} (g₁ g₂ : IndexedGrammar T) (w : List T) (h : g₂.Generates w) : (indexed_union g₁ g₂).Generates w

theorem union_first_step {T : Type} (g₁ g₂ : IndexedGrammar T) {b : List (indexed_union g₁ g₂).ISym} (h : (indexed_union g₁ g₂).Transforms [IndexedGrammar.ISym.indexed UnionNT.start []] b) : b = [IndexedGrammar.ISym.indexed (UnionNT.inl g₁.initial) []] ∨ b = [IndexedGrammar.ISym.indexed (UnionNT.inr g₂.initial) []]

theorem unlift1_tran {T : Type} (g₁ g₂ : IndexedGrammar T) {w₁ : List g₁.ISym} {w₂ : List (indexed_union g₁ g₂).ISym} (ht : (indexed_union g₁ g₂).Transforms (List.map (liftISym1 g₁ g₂) w₁) w₂) : ∃ (w₂g : List g₁.ISym), w₂ = List.map (liftISym1 g₁ g₂) w₂g ∧ g₁.Transforms w₁ w₂g

theorem unlift2_tran {T : Type} (g₁ g₂ : IndexedGrammar T) {w₁ : List g₂.ISym} {w₂ : List (indexed_union g₁ g₂).ISym} (ht : (indexed_union g₁ g₂).Transforms (List.map (liftISym2 g₁ g₂) w₁) w₂) : ∃ (w₂g : List g₂.ISym), w₂ = List.map (liftISym2 g₁ g₂) w₂g ∧ g₂.Transforms w₁ w₂g

theorem unlift1_deri {T : Type} (g₁ g₂ : IndexedGrammar T) {w₁ : List g₁.ISym} {w₂ : List (indexed_union g₁ g₂).ISym} (h : (indexed_union g₁ g₂).Derives (List.map (liftISym1 g₁ g₂) w₁) w₂) : ∃ (w₂g : List g₁.ISym), w₂ = List.map (liftISym1 g₁ g₂) w₂g ∧ g₁.Derives w₁ w₂g

theorem unlift2_deri {T : Type} (g₁ g₂ : IndexedGrammar T) {w₁ : List g₂.ISym} {w₂ : List (indexed_union g₁ g₂).ISym} (h : (indexed_union g₁ g₂).Derives (List.map (liftISym2 g₁ g₂) w₁) w₂) : ∃ (w₂g : List g₂.ISym), w₂ = List.map (liftISym2 g₁ g₂) w₂g ∧ g₂.Derives w₁ w₂g

theorem liftISym1_terminal_inv {T : Type} (g₁ g₂ : IndexedGrammar T) {wg : List g₁.ISym} {w : List T} (h : List.map (liftISym1 g₁ g₂) wg = List.map IndexedGrammar.ISym.terminal w) : wg = List.map IndexedGrammar.ISym.terminal w

theorem liftISym2_terminal_inv {T : Type} (g₁ g₂ : IndexedGrammar T) {wg : List g₂.ISym} {w : List T} (h : List.map (liftISym2 g₁ g₂) wg = List.map IndexedGrammar.ISym.terminal w) : wg = List.map IndexedGrammar.ISym.terminal w

theorem union_backward {T : Type} (g₁ g₂ : IndexedGrammar T) (w : List T) (h : (indexed_union g₁ g₂).Generates w) : g₁.Generates w ∨ g₂.Generates w

theorem Indexed_of_Indexed_u_Indexed {T : Type} (L₁ L₂ : Language T) : is_Indexed L₁ ∧ is_Indexed L₂ → is_Indexed (L₁ + L₂)

The class of indexed languages is closed under union.

theorem Indexed_closedUnderUnion {T : Type} : ClosedUnderUnion is_Indexed

The class of indexed languages is closed under union.