Strict Inclusion: CS ⊊ RE

Context-sensitive languages form a strict subclass of the recursively enumerable languages over every finite nonempty terminal alphabet. The result follows by composing the already strict inclusion CS ⊊ Recursive with the inclusion Recursive ⊆ RE.

The nonemptiness threshold is optimal. If the terminal alphabet is empty, then List T contains only the empty word, so there are only two languages; both are context-sensitive. Consequently CS and RE coincide rather than being strictly separated in that case.

Main declarations

• CS_strict_subclass_RE_of_nonempty gives the instance-based formulation.
• CS_strict_subclass_RE_of_card gives the encoding-independent finite-alphabet formulation.

theorem CS_strict_subclass_RE_of_nonempty {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] [Nonempty T] : CS ⊂ RE

Context-sensitive languages form a strict subclass of recursively enumerable languages over every nonempty finite, computably encoded terminal alphabet.

theorem CS_strict_subclass_RE_of_card {T : Type} [Fintype T] (hT : 1 ≤ Fintype.card T) : CS ⊂ RE

Context-sensitive languages form a strict subclass of recursively enumerable languages over every finite terminal alphabet with at least one symbol. The cardinality hypothesis supplies all computability instances internally and is best possible: strictness fails at cardinality zero.