Right-Regular Grammars as Unrestricted Grammars

This file gives an alternative characterization of right-regular grammars as unrestricted grammars satisfying an additional structural property on their rules.

Overview

A standard unrestricted grammar has rules of the form input_L ++ [nonterminal input_N] ++ input_R → output_string where there are no restrictions on the relationship between the left- and right-hand sides.

A right-regular grammar is one where each rule is context-free (i.e., input_L = [] and input_R = []) and the output string takes one of three forms:

• [terminal a, nonterminal B] for some terminal a and nonterminal B,
• [terminal a] for some terminal a, or
• [] (the empty string).

This file proves that the unrestricted characterization agrees with the RG_grammar presentation.

Main declarations

• is_RG_via_rg — language class induced by RG_grammar
• is_RG_via_rg_implies_is_RG — conversion to the default unrestricted characterization
• is_RG_implies_is_RG_via_rg — extraction of an RG_grammar witness
• is_RG_iff_is_RG_via_rg — equivalence of the two characterizations

Forward direction: RG_grammar → right-regular unrestricted grammar

def grule_of_RG_rule {T N : Type} (r : RG_rule T N) : grule T N

Convert an RG_rule into a grule (unrestricted grammar rule).

Equations

• grule_of_RG_rule r = { input_L := [], input_N := r.lhs, input_R := [], output_string := r.output }

def grammar_of_RG {T : Type} (g : RG_grammar T) : grammar T

Build an unrestricted grammar from a right-regular grammar.

Equations

• grammar_of_RG g = { nt := g.nt, initial := g.initial, rules := List.map grule_of_RG_rule g.rules }

theorem grammar_of_RG_right_regular {T : Type} (g : RG_grammar T) : grammar_right_regular (grammar_of_RG g)

The unrestricted grammar built from a right-regular grammar satisfies the right-regular property.

theorem grammar_of_RG_transforms {T : Type} {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : RG_transforms g w₁ w₂) : grammar_transforms (grammar_of_RG g) w₁ w₂

theorem RG_transforms_of_grammar_of_RG {T : Type} {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : grammar_transforms (grammar_of_RG g) w₁ w₂) : RG_transforms g w₁ w₂

theorem grammar_of_RG_derives_iff {T : Type} (g : RG_grammar T) (w₁ w₂ : List (symbol T g.nt)) : grammar_derives (grammar_of_RG g) w₁ w₂ ↔ RG_derives g w₁ w₂

Derivation in the original RG_grammar coincides with derivation in the constructed unrestricted grammar.

theorem grammar_of_RG_language_eq {T : Type} (g : RG_grammar T) : grammar_language (grammar_of_RG g) = RG_language g

The language of the constructed unrestricted grammar equals that of the original right-regular grammar.

theorem is_RG_via_rg_implies_is_RG {T : Type} {L : Language T} (h : is_RG_via_rg L) : is_RG L

Every language generated by an RG_grammar satisfies the default unrestricted characterization.

Backward direction: right-regular unrestricted grammar → RG_grammar

noncomputable def RG_rule_of_grule {T N : Type} (r : grule T N) (_hr : right_regular_output r.output_string) : RG_rule T N

Convert an unrestricted grammar rule (from a right-regular grammar) to an RG_rule. Uses the right-regular output property to determine the rule form.

Equations

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

theorem RG_rule_of_grule_lhs {T N : Type} (r : grule T N) (hr : right_regular_output r.output_string) : (RG_rule_of_grule r hr).lhs = r.input_N

theorem RG_rule_of_grule_output {T N : Type} (r : grule T N) (hr : right_regular_output r.output_string) : (RG_rule_of_grule r hr).output = r.output_string

noncomputable def RG_of_grammar {T : Type} (g : grammar T) (hg : grammar_right_regular g) : RG_grammar T

Construct an RG_grammar from a right-regular unrestricted grammar.

Equations

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

theorem RG_of_grammar_transforms_iff {T : Type} (g : grammar T) (hg : grammar_right_regular g) (w₁ w₂ : List (symbol T g.nt)) : RG_transforms (RG_of_grammar g hg) w₁ w₂ ↔ grammar_transforms g w₁ w₂

theorem RG_of_grammar_derives_iff {T : Type} (g : grammar T) (hg : grammar_right_regular g) (w₁ w₂ : List (symbol T g.nt)) : RG_derives (RG_of_grammar g hg) w₁ w₂ ↔ grammar_derives g w₁ w₂

Derivation in the constructed RG_grammar coincides with derivation in the original unrestricted grammar.

theorem RG_of_grammar_language_eq {T : Type} (g : grammar T) (hg : grammar_right_regular g) : RG_language (RG_of_grammar g hg) = grammar_language g

The language of the constructed RG_grammar equals that of the original grammar.

theorem is_RG_implies_is_RG_via_rg {T : Type} {L : Language T} (h : is_RG L) : is_RG_via_rg L

Every language satisfying the default unrestricted characterization is generated by an RG_grammar.

Equivalence

theorem is_RG_iff_is_RG_via_rg {T : Type} {L : Language T} : is_RG L ↔ is_RG_via_rg L

The default unrestricted characterization of regularity agrees with the RG_grammar characterization.