Linear ⊊ Context-Free

The language {0ⁿ1ⁿ2ᵐ3ᵐ} over Fin 4 (L4) is context-free (L4_is_CF, in Langlib.Classes.ContextFree.Examples.L4) but not linear (L4_not_is_Linear, in Langlib.Classes.Linear.Examples.L4). This file assembles those two facts into the strict inclusion, transported to an arbitrary alphabet T with at least four symbols by relabelling along an embedding e : Fin 4 ↪ T.

Main results

• Linear_strict_subclass_CF — Linear ⊊ CF over Fin 4.
• Linear_strict_subclass_CF_of_card — Linear ⊊ CF for any 4 ≤ Fintype.card T.

theorem Linear_strict_subclass_CF : Linear ⊂ CF

Linear languages are a strict subclass of context-free languages over Fin 4.

Transport to an arbitrary alphabet with at least four symbols

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 that admits an embedding of four distinct symbols.

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 four symbols.