Context-Free Non-Closure Under Intersection

This file proves that context-free languages are not closed under intersection.

The witnesses are lang_eq_any = {aⁿbⁿcᵐ | n,m ∈ ℕ} and lang_any_eq = {aⁿbᵐcᵐ | n,m ∈ ℕ}, each context-free (CF_lang_eq_any / CF_lang_any_eq, in Langlib.Classes.ContextFree.Examples.{AnBnCm,AnBmCm}). Their intersection is lang_eq_eq = {aⁿbⁿcⁿ | n ∈ ℕ}, which is not context-free (notCF_lang_eq_eq, in Langlib.Classes.ContextFree.Examples.AnBnCn).

This file supplies the intersection bookkeeping lang_eq_any ⊓ lang_any_eq = lang_eq_eq and assembles the non-closure statements.

Main declarations

• nnyCF_of_CF_i_CF - if L₁ and L₂ are CF, then L₁ ∩ L₂ is not always CF
• CF_notClosedUnderIntersection — CF is not closed under intersection over Fin 3

theorem intersection_of_lang_eq_eq {w : List (Fin 3)} : w ∈ lang_eq_eq → w ∈ lang_eq_any ⊓ lang_any_eq

theorem lang_eq_eq_of_intersection {w : List (Fin 3)} : w ∈ lang_eq_any ⊓ lang_any_eq → w ∈ lang_eq_eq

theorem nnyCF_of_CF_i_CF : ¬∀ (L₁ L₂ : Language (Fin 3)), is_CF L₁ ∧ is_CF L₂ → is_CF (L₁ ⊓ L₂)

The class of context-free languages isn't closed under intersection.

theorem CF_notClosedUnderIntersection : ¬ClosedUnderIntersection is_CF

Context-free languages over Fin 3 are not closed under intersection.

theorem CF_notClosedUnderIntersection_of_three {α : Type} (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : ¬ClosedUnderIntersection is_CF

Context-free languages are not closed under intersection for any type with at least 3 elements. That is, as long as α has at least 3 distinct elements, not all intersections of context-free languages over α are context-free.

theorem CF_notClosedUnderIntersection_of_card {α : Type} [Fintype α] (hα : 3 ≤ Fintype.card α) : ¬ClosedUnderIntersection is_CF

Context-free languages are not closed under intersection for any finite alphabet with at least three symbols.