Finite-nonterminal equivalence for non-contracting grammars

restrictGrammar finitizes the nonterminal type of any unrestricted grammar while preserving its language. Here we record that it also preserves non-contractingness, and package the resulting equivalence: every non-contracting grammar is equivalent to one with finitely many nonterminals that is still non-contracting.

Main results

• restrictGrammar_noncontracting — restrictGrammar preserves non-contractingness.
• noncontracting_equivalent_finiteNT — every non-contracting grammar has an equivalent one with Finite nonterminals that is again non-contracting.

Non-contracting preservation under restrictGrammar

restrictGrammar rewrites every rule by mapping each of its symbol lists through restrictSym. Since List.map preserves length, the non-contracting inequality is preserved verbatim.

theorem restrictGrammar_noncontracting {T : Type} (g : grammar T) (hg : grammar_noncontracting g) : grammar_noncontracting (restrictGrammar g)

Restricting a non-contracting grammar to its used nonterminals keeps it non-contracting.

theorem noncontracting_equivalent_finiteNT {T : Type} (g : grammar T) (hg : grammar_noncontracting g) : ∃ (g' : grammar T), Finite g'.nt ∧ grammar_noncontracting g' ∧ grammar_language g' = grammar_language g

Finite-nonterminal equivalence. Every non-contracting grammar is equivalent to a non-contracting grammar with finitely many nonterminals. We take restrictGrammar g, which finitizes the nonterminals, preserves the language, and stays non-contracting.