Kuroda Normal Form Skeleton

This file defines Kuroda grammars and states existence of a Kuroda presentation for every recursively enumerable language.

Main declarations

• grule_of_kuroda_rule
• grammar_of_kuroda_grammar
• kuroda_grammar_always_exists

inductive kuroda_rule (T N : Type) : Type

Transformation rule for a grammar in the Kuroda normal form.

• two_two {T N : Type} (A B C D : N) : kuroda_rule T N
• one_two {T N : Type} (A B C : N) : kuroda_rule T N
• one_one {T N : Type} (A : N) (t : T) : kuroda_rule T N
• one_nil {T N : Type} (A : N) : kuroda_rule T N

structure kuroda_grammar (T : Type) : Type 1

Grammar in the Kuroda normal form that generates words over the alphabet T (a type of terminals).

• nt : Type
• initial : self.nt
• rules : List (kuroda_rule T self.nt)

def grule_of_kuroda_rule {T N : Type} : kuroda_rule T N → grule T N

Equations

• grule_of_kuroda_rule (kuroda_rule.two_two A B C D) = { input_L := [], input_N := A, input_R := [symbol.nonterminal B], output_string := [symbol.nonterminal C, symbol.nonterminal D] }
• grule_of_kuroda_rule (kuroda_rule.one_two A B C) = { input_L := [], input_N := A, input_R := [], output_string := [symbol.nonterminal B, symbol.nonterminal C] }
• grule_of_kuroda_rule (kuroda_rule.one_one A t) = { input_L := [], input_N := A, input_R := [], output_string := [symbol.terminal t] }
• grule_of_kuroda_rule (kuroda_rule.one_nil A) = { input_L := [], input_N := A, input_R := [], output_string := [] }

def grammar_of_kuroda_grammar {T : Type} (k : kuroda_grammar T) : grammar T

Equations

• grammar_of_kuroda_grammar k = { nt := k.nt, initial := k.initial, rules := List.map grule_of_kuroda_rule k.rules }