Strict Inclusions in the Chomsky Hierarchy

This file proves strict subset relationships between the language classes in the Chomsky hierarchy, using results already established elsewhere in the project.

Main results

• CF_strict_subclass_RE — The class CF is a strict subclass of RE.
• CF_strictSubclass_RE — Compatibility theorem phrased as inclusion plus witness.

theorem is_RE_of_is_CF_strict : (∀ (T : Type) (L : Language T), is_CF L → is_RE L) ∧ ∃ (T : Type) (L : Language T), is_RE L ∧ ¬is_CF L

The class of context-free languages is a strict subclass of the class of recursively enumerable languages: every CF language is RE, but there exists an RE language that is not CF.

theorem CF_subclass_RE_and_exists_strict : (∀ (T : Type), CF ⊆ RE) ∧ ∃ (T : Type), CF ⊂ RE

A class-level formulation of CF_strictSubclass_RE: for every alphabet, CF ⊆ RE, and for some alphabet the inclusion is strict.

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

For any alphabet with at least 3 symbols, context-free languages form a strict subclass of recursively enumerable languages.