Membership in Context-Sensitive Languages

Membership in a context-sensitive language is uniformly computable: there is a single algorithm that, given an encoded context-sensitive grammar and a word, decides membership.

A context-sensitive (noncontracting) grammar is coded with nonterminals fixed to ℕ, as a Code T = List (grule T ℕ) × ℕ (its rule list and initial symbol), which is Primcodable. Membership is decided by a bounded search over derivation sequences (memCode): a candidate sequence of rule applications is replayed from the start symbol and checked against the target word, searching all sequences within a bound that is sufficient for noncontracting grammars.

Main results

• contextSensitive_computableMembership — uniform computability: ComputableMembership for the encoded presentation contextSensitiveLanguageOf.
• contextSensitiveLanguageOf_computableMembership / computablePred_mem_of_is_CS — the weaker per-language computability (ComputablePred), derived from the uniform result.
• Decidable membership instances, derived from computability.

The uniform decider here is also the engine behind CS ⊊ Recursive (Classes/ContextSensitive/Inclusion/StrictRecursive.lean).

Uniform computability of applyRuleSeq

The project's computable_applyRuleSeq proves applyRuleSeq rules init computable for a fixed rule list. For the enumeration we need it uniform in the rules (the grammar is runtime data). We re-derive the Primrec facts threading rules/init as projections rather than constants, reusing the uniform building blocks primrec_applyRuleAt.

theorem primrec_applyRuleSeq_uniform {T N : Type} [DecidableEq T] [DecidableEq N] [Primcodable T] [Primcodable N] : Primrec fun (p : List (grule T N) × List (symbol T N) × List (ℕ × ℕ)) => applyRuleSeq p.1 p.2.1 p.2.2

applyRuleSeq is primitive recursive uniformly in the rule list, initial form, and derivation sequence.

A concrete word-indexed enumeration of context-sensitive languages

We make the enumeration concrete so that the correctness clause becomes definitional and the remaining content splits cleanly into exactly two obligations: uniform computability of the decider (memOracle_computable) and coverage of all CS languages (enum_covers_CS).

A context-sensitive (noncontracting) grammar is coded with nonterminals fixed to ℕ, as a Code T = List (grule T ℕ) × ℕ (its rule list and initial symbol). Code T is Primcodable via the existing grulePrimcodable instance, so it is decodable from a word.

Membership is decided by a bounded search over derivation sequences: a derivation sequence seq : List (ℕ × ℕ) (rule index, position) is replayed from [initial] by applyRuleSeq, and we check whether it yields exactly v. We search all sequences of length ≤ seqBound c v whose entries are bounded (rule index < |rules|, position ≤ |v| + 1). This is a finite, computable search (via the uniform primrec_applyRuleSeq_uniform), and for a noncontracting grammar the bound is large enough to capture a witnessing derivation whenever v is in the language.

@[reducible, inline]

abbrev Code (T : Type) : Type

A coded context-sensitive grammar: nonterminals are ℕ; the data is its rule list and initial nonterminal.

Equations

• Code T = (List (grule T ℕ) × ℕ)

@[reducible]

def ofCode {T : Type} (c : Code T) : grammar T

Interpret a Code as an (unrestricted) grammar with ℕ nonterminals.

Equations

• ofCode c = { nt := ℕ, initial := c.2, rules := c.1 }

def testData {T : Type} [DecidableEq T] (c : Code T) (seq : List (ℕ × ℕ)) (v : List T) : Bool

Replay a derivation sequence from [initial] and check it yields exactly v.

Equations

• testData c seq v = decide (applyRuleSeq c.1 [symbol.nonterminal c.2] seq = some (List.map symbol.terminal v))

def seqAlphabet {T : Type} (c : Code T) (v : List T) : List (ℕ × ℕ)

The finite alphabet of derivation steps (rule index, position) considered for c, v.

Equations

• seqAlphabet c v = List.flatMap (fun (i : ℕ) => List.map (fun (p : ℕ) => (i, p)) (List.range (v.length + 2))) (List.range c.1.length)

def listsOfLen (alph : List (ℕ × ℕ)) : ℕ → List (List (ℕ × ℕ))

All lists of length exactly k over the alphabet alph.

Equations

• listsOfLen alph 0 = [[]]
• listsOfLen alph k.succ = List.flatMap (fun (l : List (ℕ × ℕ)) => List.map (fun (a : ℕ × ℕ) => a :: l) alph) (listsOfLen alph k)

def seqBound {T : Type} (c : Code T) (v : List T) : ℕ

Crude over-approximation of the length of a minimal witnessing derivation sequence (the number of distinct bounded sentential forms).

Equations

• One or more equations did not get rendered due to their size.

def candidateSeqs {T : Type} (c : Code T) (v : List T) : List (List (ℕ × ℕ))

All derivation sequences considered for c, v (length ≤ seqBound, bounded entries).

Equations

• candidateSeqs c v = List.flatMap (listsOfLen (seqAlphabet c v)) (List.range (seqBound c v + 1))

def memCode {T : Type} [DecidableEq T] (c : Code T) (v : List T) : Bool

Bounded derivation-sequence search membership decider for a coded grammar.

Equations

• memCode c v = List.foldr (fun (seq : List (ℕ × ℕ)) (r : Bool) => testData c seq v || r) false (candidateSeqs c v)

theorem memCode_primrec {T : Type} [DecidableEq T] [Primcodable T] : Primrec fun (p : Code T × List T) => memCode p.1 p.2

memCode is primrec jointly in the code and the word.

Coverage: every CS language is enumerated

The proof has two easy structural ingredients (here) and one hard combinatorial ingredient (the bounded-witness lemma memCode_complete).

theorem memCode_sound {T : Type} [DecidableEq T] (c : Code T) (v : List T) (h : memCode c v = true) : v ∈ grammar_language (ofCode c)

Coverage, soundness side. If the bounded search accepts, the word is in the language.

theorem memCode_complete {T : Type} [DecidableEq T] (c : Code T) (v : List T) (hcs : grammar_context_sensitive (ofCode c)) (h : v ∈ grammar_language (ofCode c)) : memCode c v = true

Coverage, completeness side (the hard bounded-witness lemma). For a context-sensitive coded grammar, if v is in the language then there is a witnessing derivation sequence within the search bound.

theorem code_of_CS {T : Type} [DecidableEq T] {L : Language T} (hL : is_CS L) : ∃ (c : Code T), grammar_context_sensitive (ofCode c) ∧ grammar_language (ofCode c) = L

Encoding. Every context-sensitive language is the language of a context-sensitive coded grammar (nonterminals renamed to ℕ).

Uniform computable membership

The language a coded grammar accepts via the bounded search. For a context-sensitive code it equals the grammar's language (memCode_sound / memCode_complete); for an arbitrary code it is whatever the bounded search accepts — in all cases a decidable language.

def contextSensitiveLanguageOf {T : Type} [DecidableEq T] (c : Code T) : Language T

The bounded-search language of a coded grammar.

Equations

• contextSensitiveLanguageOf c = {v : List T | memCode c v = true}

theorem contextSensitive_membership_computablePred {T : Type} [DecidableEq T] [Primcodable T] : ComputablePred fun (p : Code T × List T) => p.2 ∈ contextSensitiveLanguageOf p.1

Uniform computability of context-sensitive membership. Membership is decided by a single algorithm taking the encoded grammar and the word jointly.

This is the raw ComputablePred decider; the packaged uniform statement ComputableMembership is_CS contextSensitiveLanguageOf' (over the noncontracting-code subtype) is assembled in ContextSensitive/Decidability/Characterization.lean.

Computable membership (per language)

Specialising the uniform algorithm to a fixed (encoded) grammar, or to any context-sensitive language, gives the weaker ComputablePred statements.

theorem contextSensitiveLanguageOf_computableMembership {T : Type} [DecidableEq T] [Primcodable T] (c : Code T) : ComputablePred fun (w : List T) => w ∈ contextSensitiveLanguageOf c

Per-grammar computability: membership in a fixed coded grammar's bounded-search language.

theorem exists_code_of_is_CS {T : Type} [DecidableEq T] {L : Language T} (hL : is_CS L) : ∃ (c : Code T), contextSensitiveLanguageOf c = L

Every context-sensitive language is exactly the bounded-search language of some code.

theorem computablePred_mem_of_is_CS {T : Type} [DecidableEq T] [Primcodable T] {L : Language T} (hL : is_CS L) : ComputablePred fun (w : List T) => w ∈ L

Membership in any context-sensitive language is computable (ComputablePred), derived from the uniform algorithm.

Decidable membership

Decidability is a corollary of computability. For a coded grammar the decision procedure is the genuine bounded search; for an abstract context-sensitive language it is extracted classically.

instance decidable_mem_contextSensitiveLanguageOf {T : Type} [DecidableEq T] (c : Code T) (v : List T) : Decidable (v ∈ contextSensitiveLanguageOf c)

Membership in a coded grammar's bounded-search language is decidable (by the search).

Equations

• decidable_mem_contextSensitiveLanguageOf c v = decidable_of_iff (memCode c v = true) ⋯

noncomputable def decidable_mem_of_is_CS {T : Type} [DecidableEq T] [Primcodable T] {L : Language T} (hL : is_CS L) (v : List T) : Decidable (v ∈ L)

Membership in a context-sensitive language is decidable.

Equations

• decidable_mem_of_is_CS hL v = ⋯ ▸ decidable_mem_contextSensitiveLanguageOf ⋯.choose v