Linear ⊊ Context-Free

The language {0ⁿ1ⁿ2ᵐ3ᵐ} over Fin 4 (anbncmdm) is context-free (anbncmdm_is_CF, in Langlib.Classes.ContextFree.Examples.AnBnCmDm) but not linear (anbncmdm_not_is_Linear, in Langlib.Classes.Linear.Examples.AnBnCmDm). This file assembles those two facts into the strict inclusion over every finite alphabet with at least 4 elements by transporting the counterexample to the target alphabet.

Main results

• Linear_strict_subclass_CF_of_card — Linear ⊊ CF over every finite alphabet with at least 4 elements.

Arbitrary alphabets with at least 4 elements

theorem Linear_strict_subclass_CF_of_embedding {T : Type} (e : Fin 4 ↪ T) : Linear ⊂ CF

Linear languages are a strict subclass of context-free languages over any alphabet with at least 4 elements.

theorem Linear_strict_subclass_CF_of_card {T : Type} [Fintype T] (hT : 4 ≤ Fintype.card T) : Linear ⊂ CF

Linear languages are a strict subclass of context-free languages over any finite alphabet with at least 4 elements.