Context-Free Inclusions

This file relates the project's context-free grammars to context-sensitive, unrestricted, and mathlib formulations.

Main declarations

• is_CS_of_is_CF / CF_subclass_CS
• is_CF_iff_isContextFree

def CF_no_epsilon' {T : Type} (g : CF_grammar T) : Prop

A context-free grammar has no ε-productions (every rule has a non-empty right-hand side).

Equations

• CF_no_epsilon' g = ∀ r ∈ g.rules, r.2 ≠ []

def csg_of_cfg {T : Type} (g : CF_grammar T) (hne : CF_no_epsilon' g) : CS_grammar T

Convert a context-free grammar without ε-productions to a context-sensitive grammar. The CS rules have empty context (α = β = []) and γ = rule output.

Equations

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

theorem CF_language_eq_CS_language {T : Type} (g : CF_grammar T) (hne : CF_no_epsilon' g) : CF_language g = CS_language (csg_of_cfg g hne)

theorem is_CS_of_is_CF {T : Type} {L : Language T} (h : is_CF L) : is_CS L

Context-free languages are context-sensitive.

Context-sensitive grammars require non-empty rule outputs, so the ε-productions of the context-free grammar are first removed (ContextFreeGrammar.eliminateEmpty), yielding a non-contracting grammar for L \ {ε}. The empty word is re-adjoined when ε ∈ L using is_CS_insert_empty_of_CS_grammar.

theorem CF_subclass_CS {T : Type} : CF ⊆ CS

Context-free languages form a subclass of the context-sensitive languages.