Context-Free Closure Under Reversal

This file proves that context-free languages are closed under word reversal.

Strategy

Instead of re-proving the derivation-reversal argument from scratch, we reuse grammar_language_reversal_grammar (the unrestricted result) together with a commutation lemma that shows reversing a CF grammar and then embedding it into an unrestricted grammar gives the same result as embedding first and then reversing.

Main declarations

• reversal_CF_grammar — reverse the RHS of every CF rule
• grammar_of_cfg_reversal_comm — commutation with the CF→unrestricted embedding
• CF_of_reverse_CF
• CF_of_reverse_CF_rev
• CF_reverse_iff_CF

def reversal_CF_grammar {T : Type} (g : CF_grammar T) : CF_grammar T

Reverse the right-hand side of every rule in a context-free grammar.

Equations

• reversal_CF_grammar g = { nt := g.nt, initial := g.initial, rules := List.map (fun (r : g.nt × List (symbol T g.nt)) => (r.1, r.2.reverse)) g.rules }

theorem grammar_of_cfg_reversal_comm {T : Type} (g : CF_grammar T) : grammar_of_cfg (reversal_CF_grammar g) = reversal_grammar (grammar_of_cfg g)

Reversing a CF grammar and then embedding it as an unrestricted grammar gives the same grammar as embedding first and then applying the unrestricted reversal.

theorem CF_of_reverse_CF {T : Type} (L : Language T) : is_CF L → is_CF L.reverse

The class of context-free languages is closed under reversal.

theorem CF_of_reverse_CF_rev {T : Type} (L : Language T) : is_CF L.reverse → is_CF L

The converse direction of CF_of_reverse_CF, using that reversal is an involution.

@[simp]

theorem CF_reverse_iff_CF {T : Type} (L : Language T) : is_CF L.reverse ↔ is_CF L

A language is context-free iff its reversal is context-free.

theorem CF_closedUnderReverse {T : Type} : ClosedUnderReverse is_CF

The class of context-free languages is closed under reversal.