Elementary Context-Free Languages

This file builds basic context-free grammars witnessing simple languages.

Main declarations

• language_of_cfg_empty_lang
• language_of_cfg_empty_word
• language_of_cfg_symbol_star

def cfg_empty_lang {T : Type} : CF_grammar T

Context-free grammar for the empty Language (i.e., ∈ always gives false).

Equations

• cfg_empty_lang = { nt := Fin 1, initial := 0, rules := [] }

theorem language_of_cfg_empty_lang {T : Type} : CF_language cfg_empty_lang = 0

Characterization of the empty Language.

def cfg_empty_word {T : Type} : CF_grammar T

Context-free grammar for the singleton Language that contains [] as its only word.

Equations

• cfg_empty_word = { nt := Fin 1, initial := 0, rules := [(0, [])] }

theorem language_of_cfg_empty_word {T : Type} : CF_language cfg_empty_word = {[]}

Characterization of the singleton Language.

def cfg_symbol_star {T : Type} (a : T) : CF_grammar T

Context-free grammar for a Language {a}.star where a is a given terminal symbol.

Equations

• cfg_symbol_star a = { nt := Fin 1, initial := 0, rules := [(0, [symbol.terminal a, symbol.nonterminal 0]), (0, [])] }

theorem language_of_cfg_symbol_star {T : Type} (a : T) : CF_language (cfg_symbol_star a) = fun (w : List T) => ∃ (n : ℕ), w = List.replicate n a

Characterization of the {a}.star Language.