Strict Inclusion: CF ⊊ CS

Context-free languages form a strict subclass of the context-sensitive languages.

Inclusion CF ⊆ CS is is_CS_of_is_CF. Strictness is witnessed by {aⁿbⁿcⁿ} (lang_eq_eq), which is context-sensitive (lang_eq_eq_is_CS) but not context-free (notCF_lang_eq_eq, via the context-free pumping lemma).

Main declarations

• CF_subclass_CS_and_exists_strict
• CF_strict_subclass_CS

theorem CF_subclass_CS_and_exists_strict : (∀ (T : Type) (L : Language T), is_CF L → is_CS L) ∧ ∃ (T : Type) (L : Language T), is_CS L ∧ ¬is_CF L

CF ⊊ CS: every context-free language is context-sensitive, and there is a context-sensitive language ({aⁿbⁿcⁿ}) that is not context-free.

theorem CF_strict_subclass_CS {T : Type} [Fintype T] (hT : 3 ≤ Fintype.card T) : CF ⊂ CS

For any finite alphabet with at least 3 symbols, the context-free languages form a strict subclass of the context-sensitive languages: CF ⊂ CS.

The witness {aⁿbⁿcⁿ} (lang_eq_eq, over Fin 3) is relabeled into T along an embedding e : Fin 3 ↪ T. Relabeling along an injective map is an ε-free homomorphism, under which CS is closed (CS_closedUnderEpsFreeHomomorphism), so the image stays context-sensitive; were it context-free, injectivity of e would pull {aⁿbⁿcⁿ} itself back into CF (CF_of_map_injective_CF_rev), contradicting notCF_lang_eq_eq.