Context-Sensitive Languages

This file defines the class of context-sensitive languages via unrestricted grammars: all rules are non-contracting, except for an optional distinguished start rule S → ε.

def initial_epsilon_rule {T : Type} (g : grammar T) (r : grule T g.nt) : Prop

The distinguished empty-word rule S → ε.

Equations

• initial_epsilon_rule g r = (r.input_L = [] ∧ r.input_N = g.initial ∧ r.input_R = [] ∧ r.output_string = [])

def grule_noncontracting {T N : Type} (r : grule T N) : Prop

The non-contracting rule condition for a single unrestricted grammar rule.

Equations

• grule_noncontracting r = (r.output_string.length ≥ r.input_L.length + 1 + r.input_R.length)

def initial_not_on_rhs {T : Type} (g : grammar T) : Prop

The start symbol does not occur on the right-hand side of any rule.

Equations

• initial_not_on_rhs g = ∀ r ∈ g.rules, symbol.nonterminal g.initial ∉ r.output_string

def grammar_context_sensitive {T : Type} (g : grammar T) : Prop

An unrestricted grammar is context-sensitive if every rule is either the optional distinguished rule S → ε or is non-contracting, and — whenever the S → ε rule is present — the start symbol S never occurs on a right-hand side.

The right-hand-side restriction is part of the standard definition of a context-sensitive grammar: it guarantees that S only ever appears as the initial sentential form, so that the erasing rule S → ε contributes exactly the empty word (and nothing else). Without it, rules such as S → SS together with S → ε would allow contracting derivations of non-empty words, taking the grammar outside the context-sensitive (linear-bounded) class.

Equations

• grammar_context_sensitive g = ((∀ r ∈ g.rules, initial_epsilon_rule g r ∨ grule_noncontracting r) ∧ ((∃ r ∈ g.rules, initial_epsilon_rule g r) → initial_not_on_rhs g))

theorem grammar_context_sensitive_of_noncontracting {T : Type} (g : grammar T) (hg : grammar_noncontracting g) : grammar_context_sensitive g

Every non-contracting grammar is context-sensitive: it has no S → ε rule, so the right-hand-side restriction is vacuous.

def is_CS {T : Type} (L : Language T) : Prop

Predicate that a language is context-sensitive.

Equations

• is_CS L = ∃ (g : grammar T), grammar_context_sensitive g ∧ grammar_language g = L

theorem is_CS_of_is_noncontracting {T : Type} {L : Language T} (h : is_noncontracting L) : is_CS L

Every non-contracting language is context-sensitive.

def is_CS_via_csg {T : Type} (L : Language T) : Prop

Characterization of context-sensitive languages via ε-free context-preserving grammars.

Equations

• is_CS_via_csg L = ∃ (g : CS_grammar T), CS_language g = L

def CS {T : Type} : Set (Language T)

The class of context-sensitive languages.

Equations

• CS = setOf is_CS