Regular Languages

This file defines the class of regular languages via unrestricted grammars satisfying the right-regular rule-shape property.

def right_regular_output {T N : Type} (s : List (symbol T N)) : Prop

An output string has right-regular form if it is one of:

• [terminal a, nonterminal B],
• [terminal a], or
• [].

Equations

• right_regular_output s = ((∃ (a : T) (B : N), s = [symbol.terminal a, symbol.nonterminal B]) ∨ (∃ (a : T), s = [symbol.terminal a]) ∨ s = [])

def grammar_right_regular {T : Type} (g : grammar T) : Prop

An unrestricted grammar is right-regular if every rule is context-free and has right-regular output.

Equations

• grammar_right_regular g = ∀ r ∈ g.rules, r.input_L = [] ∧ r.input_R = [] ∧ right_regular_output r.output_string

def is_RG {T : Type} (L : Language T) : Prop

A language is regular if it is generated by some right-regular unrestricted grammar.

Equations

• is_RG L = ∃ (g : grammar T), grammar_right_regular g ∧ grammar_language g = L

def is_RG_via_rg {T : Type} (L : Language T) : Prop

Characterization of regular languages via RG_grammar.

Equations

• is_RG_via_rg L = ∃ (g : RG_grammar T), RG_language g = L

def RG {T : Type} : Set (Language T)

The class of regular languages.

Equations

• RG = setOf is_RG