Strict Inclusion: CS ⊊ Recursive

Context-sensitive languages form a strict subclass of the recursive languages.

The proof is based on diagonalization.

The uniform computable membership oracle for context-sensitive grammars (memCode / contextSensitive_computableMembership, in Classes/ContextSensitive/Decidability/Membership.lean) supplies a surjective enumeration e : List T → Language T of all context-sensitive languages and a total computable mem : List T → List T → Bool with mem u v = true ↔ v ∈ e u. Define D = {v | v ∉ e v}. Then D is recursive, since its characteristic predicate v ↦ mem v v is computable. And D is not context-sensitive: if e u = D for some u, instantiating the definition of D at v = u and substituting e u = D gives u ∈ D ↔ u ∉ e u ↔ u ∉ D, a contradiction; hence D is not in the range of e. Therefore D is recursive but not context-sensitive, so CS ⊊ Recursive.

The argument requires mem to be total and computable, which holds for CS but not for Recursive (the recursive languages are not recursively enumerable), so it separates CS from Recursive but does not extend to separating Recursive from RE.

theorem diagonal_strict {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] (e : List T → Language T) (mem : List T → List T → Bool) (hmem : ∀ (u v : List T), mem u v = true ↔ v ∈ e u) (hmem_comp : Computable fun (p : List T × List T) => mem p.1 p.2) (hsurj : ∀ (L : Language T), is_CS L → ∃ (u : List T), e u = L) : CS ⊂ Recursive

Abstract diagonalization core (proven). From a correct, computable membership oracle for a word-indexed enumeration covering all context-sensitive languages, the diagonal language is recursive but not context-sensitive, giving CS ⊊ Recursive.

noncomputable def decodeCode {T : Type} [Primcodable T] (u : List T) : Code T

Decode a word into a coded grammar, indexing by the word's length (List.length is onto ℕ for a nonempty alphabet, so this is surjective onto coded grammars). A default empty grammar is used if the code is malformed.

Equations

• decodeCode u = (Encodable.decode u.length).getD ([], 0)

noncomputable def memOracle {T : Type} [DecidableEq T] [Primcodable T] (u v : List T) : Bool

The membership oracle: decode the index word into a coded grammar and run the bounded search.

Equations

• memOracle u v = memCode (decodeCode u) v

noncomputable def enumLang {T : Type} [DecidableEq T] [Primcodable T] (u : List T) : Language T

The enumerated language at index word u. Correctness against memOracle is definitional.

Equations

• enumLang u = {v : List T | memOracle u v = true}

theorem memOracle_computable {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] : Computable fun (p : List T × List T) => memOracle p.1 p.2

Obligation 1 (uniform computability), now discharged. The bounded derivation-sequence search oracle is computable jointly in the grammar-code word and the input word: decodeCode is Encodable.decode ∘ encode and memCode is the bounded search, primrec via the uniform primrec_applyRuleSeq_uniform.

theorem enum_covers_CS {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] [Nonempty T] (L : Language T) : is_CS L → ∃ (u : List T), enumLang u = L

Obligation 2 (coverage). Every context-sensitive language is enumLang u for some index word u. Assembled from memCode_sound/memCode_complete (membership correctness), code_of_CS (encoding), and decodeCode_surj (surjectivity).

theorem exists_cs_enumeration {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] [Nonempty T] : ∃ (e : List T → Language T) (mem : List T → List T → Bool), (∀ (u v : List T), mem u v = true ↔ v ∈ e u) ∧ (Computable fun (p : List T × List T) => mem p.1 p.2) ∧ ∀ (L : Language T), is_CS L → ∃ (u : List T), e u = L

Effective enumeration of context-sensitive languages, assembled from the two obligations memOracle_computable and enum_covers_CS (the correctness clause is definitional, since enumLang u is defined as {v | memOracle u v = true}).

theorem CS_strict_subclass_Recursive {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] [Nonempty T] : CS ⊂ Recursive

Context-sensitive languages are a strict subclass of the recursive languages, CS ⊊ Recursive. Assembled from the proven diagonalization core diagonal_strict and the enumeration obligation exists_cs_enumeration. (Nonemptiness of the alphabet is necessary: over an empty alphabet CS = Recursive.)