Context-Free Concatenation Bonus Construction

This file records a direct grammar construction for context-free closure under concatenation.

Main declarations

• bonus_CF_of_CF_c_CF

def combined_grammar {T : Type} (gₗ gᵣ : CF_grammar T) : CF_grammar T

Equations

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

def combined_rule_of_rule₁ {T : Type} {g₁ g₂ : CF_grammar T} (r : g₁.nt × List (symbol T g₁.nt)) : (combined_grammar g₁ g₂).nt × List (symbol T (combined_grammar g₁ g₂).nt)

Equations

• combined_rule_of_rule₁ r = (some (Sum.inl r.1), lsTN_of_lsTN₁ r.2)

def combined_rule_of_rule₂ {T : Type} {g₁ g₂ : CF_grammar T} (r : g₂.nt × List (symbol T g₂.nt)) : (combined_grammar g₁ g₂).nt × List (symbol T (combined_grammar g₁ g₂).nt)

Equations

• combined_rule_of_rule₂ r = (some (Sum.inr r.1), lsTN_of_lsTN₂ r.2)

theorem bonus_CF_of_CF_c_CF {T : Type} (L₁ L₂ : Language T) : is_CF L₁ ∧ is_CF L₂ → is_CF (L₁ * L₂)

An explicit grammar construction witnessing closure of context-free languages under concatenation.