Context-Sensitive Inclusions

This file embeds context-sensitive grammars into unrestricted grammars and derives the main inclusion result.

Main declarations

• CS_language_eq_grammar_language
• CS_subclass_RE

def grammar_of_csg {T : Type} (g : CS_grammar T) : grammar T

Equations

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

theorem CS_language_eq_grammar_language {T : Type} (g : CS_grammar T) : CS_language g = grammar_language (grammar_of_csg g)

theorem grammar_of_csg_context_sensitive {T : Type} (g : CS_grammar T) : grammar_context_sensitive (grammar_of_csg g)

The unrestricted grammar obtained from a CS_grammar is non-contracting, and hence context-sensitive in the S → ε-optional sense.

theorem is_CS_via_csg_implies_is_CS {T : Type} {L : Language T} (h : is_CS_via_csg L) : is_CS L

Every language generated by an ε-free context-preserving grammar is context-sensitive.

theorem is_RE_of_CS {T : Type} {L : Language T} (h : is_CS L) : is_RE L

theorem CS_subclass_RE {T : Type} : CS ⊆ RE