Context-Sensitive Languages are Recursive

This file proves the bridge theorem that every context-sensitive language (in the broad S → ε-optional grammar_context_sensitive sense) is recursive, and the corresponding class-level inclusion (CS : Set (Language T)) ⊆ Recursive.

Strategy

is_Recursive_of_is_CS is a direct corollary of the uniform computable membership decider for context-sensitive grammars (computablePred_mem_of_is_CS, in Classes/ContextSensitive/Decidability/Membership.lean): membership in any context-sensitive language is a ComputablePred, and a computable membership predicate is recursive (is_Recursive_of_computable_decide).

Main declarations

• is_Recursive_of_is_CS
• CS_subset_Recursive_class

Main bridge theorems

theorem is_Recursive_of_is_CS {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] {L : Language T} (h : is_CS L) : is_Recursive L

Every context-sensitive language is recursive. Derived from the uniform computable membership decider for context-sensitive grammars (computablePred_mem_of_is_CS).

theorem CS_subset_Recursive_class {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] : CS ⊆ Recursive

The class of context-sensitive languages is a subset of the recursive languages.