Context-Free Grammars as Unrestricted Grammars

This file gives an alternative characterization of context-free 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 context-free grammar is one where each rule has no context: i.e., for every rule, input_L = [] and input_R = []. In other words, each rule rewrites a single nonterminal A to a string γ, independently of the surrounding context.

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

Main declarations

• is_CF_via_cfg — language class induced by CF_grammar
• is_CF_via_cfg_implies_is_CF — conversion to the default unrestricted characterization
• is_CF_implies_is_CF_via_cfg — extraction of a CF_grammar witness
• is_CF_iff_is_CF_via_cfg — equivalence of the two characterizations

Forward direction: CF_grammar → context-free unrestricted grammar

def grammar_of_cfg {T : Type} (g : CF_grammar T) : grammar T

Convert a context-free grammar to the corresponding unrestricted grammar with empty left and right contexts in every rule.

Equations

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

theorem CF_language_eq_grammar_language {T : Type} (g : CF_grammar T) : CF_language g = grammar_language (grammar_of_cfg g)

theorem grammar_of_cfg_context_free {T : Type} (g : CF_grammar T) : grammar_context_free (grammar_of_cfg g)

The unrestricted grammar obtained from a context-free grammar (via grammar_of_cfg) satisfies the context-free property.

theorem is_CF_via_cfg_implies_is_CF {T : Type} {L : Language T} (h : is_CF_via_cfg L) : is_CF L

Every language generated by a CF_grammar satisfies the default unrestricted characterization.

Backward direction: context-free unrestricted grammar → CF_grammar

def cfrule_of_grule {T N : Type} (r : grule T N) : N × List (symbol T N)

Convert an unrestricted grammar rule (from a context-free unrestricted grammar) into a context-free rule (a pair of nonterminal and output string).

Equations

• cfrule_of_grule r = (r.input_N, r.output_string)

def cfg_of_grammar {T : Type} (g : grammar T) (_hg : grammar_context_free g) : CF_grammar T

Construct a CF_grammar from a context-free unrestricted grammar.

Equations

• cfg_of_grammar g _hg = { nt := g.nt, initial := g.initial, rules := List.map cfrule_of_grule g.rules }

theorem cfg_of_grammar_transforms_iff {T : Type} (g : grammar T) (hg : grammar_context_free g) (w₁ w₂ : List (symbol T g.nt)) : CF_transforms (cfg_of_grammar g hg) w₁ w₂ ↔ grammar_transforms g w₁ w₂

theorem cfg_of_grammar_derives_iff {T : Type} (g : grammar T) (hg : grammar_context_free g) (w₁ w₂ : List (symbol T g.nt)) : CF_derives (cfg_of_grammar g hg) w₁ w₂ ↔ grammar_derives g w₁ w₂

The derivation relation of the constructed CF_grammar coincides with that of the original unrestricted grammar.

theorem cfg_of_grammar_language_eq {T : Type} (g : grammar T) (hg : grammar_context_free g) : CF_language (cfg_of_grammar g hg) = grammar_language g

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

theorem is_CF_implies_is_CF_via_cfg {T : Type} {L : Language T} (h : is_CF L) : is_CF_via_cfg L

Every language satisfying the default unrestricted characterization is generated by a CF_grammar.

Equivalence

theorem is_CF_iff_is_CF_via_cfg {T : Type} {L : Language T} : is_CF L ↔ is_CF_via_cfg L

The default unrestricted characterization of context-freeness agrees with the CF_grammar characterization.