Membership in context-sensitive languages is computable

Statement

Given a context-sensitive grammar g, the predicate “does the word w belong to the language generated by g?” is computable — there is an actual algorithm that always halts with the correct yes/no answer, uniform in the encoded grammar.

In Lean

Mirroring the structure of contextFree_computableMembership for context-free grammars:

• contextSensitive_computableMembership — the headline uniform class-level result, ComputableMembership CS contextSensitiveLanguageOf', bundling adequacy (Characterizes CS), effectivity (MembershipSemiDecidable), and the joint decider in an encoded grammar c and word w.
• computablePred_mem_of_is_CS — the per-language corollary: for any is_CS L, ComputablePred (fun w => w ∈ L).

Proof idea

The decider memCode c w runs a bounded derivation-sequence search: a non-contracting grammar can never shorten a sentential form, so any derivation of w uses forms of length ≤ |w|, drawn from a finite alphabet — there are only finitely many, bounding both the length and the breadth of the search. The search enumerates candidate rule-application sequences up to that bound and checks whether any reaches w (memCode_sound / memCode_complete).

The whole search is primitive recursive in the encoded grammar and the word together (memCode_primrec, built on the uniform primrec_applyRuleSeq_uniform), which directly yields the uniform ComputablePred; the per-language and Decidable forms are immediate corollaries. This uniform computability is also the engine behind the diagonalization in CS ⊊ Recursive.

Keywords / also known as

context-sensitive membership decidable, CSL membership computable, ComputablePred context-sensitive, deciding membership in a context-sensitive grammar, type-1 membership algorithm, LBA membership decidable.

Formalized in Lean 4 with Mathlib, in Langlib.