ε-elimination of context-sensitive grammars

Every context-sensitive language (in the broad S → ε-optional grammar_context_sensitive sense) admits an equivalent — off the empty word — non-contracting grammar with finitely many nonterminals (exists_noncontracting_offEmpty_of_CS). This is the structural normal form used, e.g., in the CS = LBA (Kuroda) construction and in establishing CS ⊆ Recursive.

Strategy

With the standard definition of grammar_context_sensitive, the start symbol S never occurs on a right-hand side once the optional S → ε rule is present. This makes ε-elimination elementary: simply delete every contracting rule (i.e. keep only the non-contracting ones). Concretely, set

g' := { nt := g.nt, initial := g.initial,
        rules := g.rules.filter (fun r => decide (grule_noncontracting r)) }.

g' is non-contracting by construction, and grammar_language g' = grammar_language g \ {[]}. The non-obvious inclusion is ⊇: starting from the single start symbol [S] (with the target word ≠ []), the very first rule fired has empty context and input_N = S; it cannot be the S → ε rule (that yields [], which is stuck), so it is non-contracting and its output is S-free (by initial_not_on_rhs). From there every sentential form stays S-free, and on an S-free form the matched rule is never the S → ε rule, hence non-contracting and kept in g'. So the whole g-derivation is in fact a g'-derivation.

Main declarations

• exists_noncontracting_offEmpty_of_CS

The key language identity

ε-elimination

theorem exists_noncontracting_offEmpty_of_CS {T : Type} (g : grammar T) (hg : grammar_context_sensitive g) : ∃ (g₀ : grammar T), Finite g₀.nt ∧ grammar_noncontracting g₀ ∧ grammar_language g₀ = grammar_language g \ {[]}

ε-elimination. Every broadly-context-sensitive grammar admits an equivalent (off the empty word) ε-free non-contracting grammar with finitely many nonterminals. We take gFilter g (delete the contracting rules) and finitize its nonterminals with restrictGrammar.