Context-Free Closure Under Bijections

This file proves that context-free languages are preserved under renaming terminals along an equivalence.

Strategy

We reuse the unrestricted-level result bijection_grammar_language by showing that the CF bijection construction commutes with the embedding into unrestricted grammars. The derivation correspondence is proved only once at the unrestricted level; the CF file only needs to verify structure preservation.

Main declarations

• CF_of_map_CF
• CF_of_map_injective_CF_rev
• bijection_CF_grammar
• bijection_CF_grammar_language
• CF_of_bijemap_CF
• CF_of_bijemap_CF_rev
• CF_bijemap_iff_CF

theorem CF_of_map_CF {T₁ T₂ : Type} (f : T₁ → T₂) (L : Language T₁) : is_CF L → is_CF ((Language.map f) L)

Context-free languages are closed under alphabet maps.

theorem CF_of_map_injective_CF_rev {T₁ T₂ : Type} {f : T₁ → T₂} (hf : Function.Injective f) (L : Language T₁) : is_CF ((Language.map f) L) → is_CF L

Injective alphabet maps reflect context-freeness.

def bijection_CF_grammar {T₁ T₂ : Type} (g : CF_grammar T₁) (π : T₁ ≃ T₂) : CF_grammar T₂

Map a CF grammar along a terminal bijection.

Equations

• bijection_CF_grammar g π = { nt := g.nt, initial := g.initial, rules := List.map (fun (r : g.nt × List (symbol T₁ g.nt)) => (r.1, List.map (map_symbol π) r.2)) g.rules }

theorem bijection_CF_grammar_language {T₁ T₂ : Type} (g : CF_grammar T₁) (π : T₁ ≃ T₂) : CF_language (bijection_CF_grammar g π) = (CF_language g).bijemapLang π

The bijection CF grammar generates exactly the π-image of the original language.

theorem CF_of_bijemap_CF {T₁ T₂ : Type} (π : T₁ ≃ T₂) (L : Language T₁) : is_CF L → is_CF (L.bijemapLang π)

The class of context-free languages is closed under bijection between terminal alphabets.

theorem CF_of_bijemap_CF_rev {T₁ T₂ : Type} (π : T₁ ≃ T₂) (L : Language T₁) : is_CF (L.bijemapLang π) → is_CF L

The converse direction of CF_of_bijemap_CF, obtained by applying the forward result to the inverse bijection.

@[simp]

theorem CF_bijemap_iff_CF {T₁ T₂ : Type} (π : T₁ ≃ T₂) (L : Language T₁) : is_CF (L.bijemapLang π) ↔ is_CF L

A language is context-free iff its image under a bijection of terminal alphabets is context-free.