Context-sensitive languages: adjoining the empty word

If L is generated by a non-contracting unrestricted grammar (equivalently, by an ε-free context-sensitive grammar), then {ε} ∪ L is context-sensitive.

The construction adds a fresh start symbol S' = none on top of the grammar g₀, together with the two rules S' → ε and S' → S₀. The original rules are lifted unchanged along some : g₀.nt → Option g₀.nt, so they remain non-contracting and S' never occurs on a right-hand side — exactly the side condition the broad definition of is_CS requires when the S → ε rule is present.

This is the closure lemma used to handle the acceptEmpty = true branch of LBA ⊆ CS.

def ContextSensitiveEmptyWord.addEmpty_grammar {T : Type} (g₀ : grammar T) : grammar T

g₀ with a fresh start symbol none, plus rules none → ε and none → S₀, the original rules lifted along some.

Equations

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

def ContextSensitiveEmptyWord.lg {T : Type} (g₀ : grammar T) : lifted_grammar_ T

g₀ lifts into addEmpty_grammar g₀ along some, with id as the (total) sink.

Equations

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

The grammar is context-sensitive

theorem ContextSensitiveEmptyWord.addEmpty_context_sensitive {T : Type} (g₀ : grammar T) (h : grammar_noncontracting g₀) : grammar_context_sensitive (addEmpty_grammar g₀)

Language equality

theorem ContextSensitiveEmptyWord.mem_addEmpty_nil {T : Type} (g₀ : grammar T) : [] ∈ grammar_language (addEmpty_grammar g₀)

theorem ContextSensitiveEmptyWord.mem_addEmpty_of_mem {T : Type} {g₀ : grammar T} {w : List T} (hw : w ∈ grammar_language g₀) : w ∈ grammar_language (addEmpty_grammar g₀)

theorem ContextSensitiveEmptyWord.disj_of_mem_addEmpty {T : Type} {g₀ : grammar T} {w : List T} (ass : w ∈ grammar_language (addEmpty_grammar g₀)) : w = [] ∨ w ∈ grammar_language g₀

theorem ContextSensitiveEmptyWord.grammar_language_addEmpty {T : Type} (g₀ : grammar T) : grammar_language (addEmpty_grammar g₀) = fun (w : List T) => w = [] ∨ grammar_language g₀ w

theorem is_CS_insert_empty_of_noncontracting {T : Type} (g₀ : grammar T) (h : grammar_noncontracting g₀) : is_CS fun (w : List T) => w = [] ∨ grammar_language g₀ w

Adjoining ε to a non-contracting language stays context-sensitive.

theorem is_CS_insert_empty_of_CS_grammar {T : Type} (g : CS_grammar T) : is_CS fun (w : List T) => w = [] ∨ CS_language g w

Adjoining ε to an ε-free context-sensitive language stays context-sensitive.

theorem is_CS_insert_empty_of_is_CS_not_nil {T : Type} {L : Language T} (hL : is_CS L) (hne : [] ∉ L) : is_CS fun (w : List T) => w = [] ∨ L w

Adjoining ε to an ε-free context-sensitive language stays context-sensitive.

This variant starts from the broad is_CS predicate rather than an explicit context-preserving grammar witness. It removes the optional empty-word rule using exists_noncontracting_offEmpty_of_CS, then re-adds ε with a fresh start symbol.

theorem is_CS_insert_empty_of_is_CS {T : Type} {L : Language T} (hL : is_CS L) : is_CS fun (w : List T) => w = [] ∨ L w

Adjoining ε to any context-sensitive language stays context-sensitive.

If ε is already present this is just the same language; otherwise it is the ε-free case above.

theorem is_CS_of_diff_empty_of_is_CS {T : Type} {L : Language T} (hL : is_CS (L \ {[]})) : is_CS L

If the nonempty part of a language is context-sensitive, then the whole language is context-sensitive. The only possible difference is the empty word, which context-sensitive languages can adjoin.