Langlib

Langlib.Classes.ContextFree.Decidability.Characterization

EncodedCFG characterizes the context-free languages #

This file proves that the encoded-grammar encoding EncodedCFG denotes exactly the context-free languages:

∀ L, L ∈ CF ↔ ∃ c : EncodedCFG T, contextFreeLanguageOf c = L

Soundness (every code denotes a context-free language): an EncodedCFG decodes — by construction — to a CF_grammar (toCFGrammar), so its language is is_CF_via_cfg, hence is_CF.

Completeness (every context-free language is encoded): a context-free language has a CF_grammar presentation with finitely many nonterminals (exists_fintype_nt); we reindex those nonterminals to Fin (n+1) and read the grammar off as an EncodedCFG. Reindexing the nonterminals along an equivalence preserves the language (cf_language_eq_of_rename), proved with the lifting machinery (lift_deri / sink_deri).

Renaming nonterminals preserves the language #

source
theorem ContextFree.EncodedCFG.cf_language_eq_of_rename {T : Type} {g₀ g : CF_grammar T} (e : g₀.nt ≃ g.nt) (hinit : g.initial = e g₀.initial) (hfwd : ∀ r ∈ g₀.rules, lift_rule (⇑e) r ∈ g.rules) (hbwd : ∀ r ∈ g.rules, ∃ r₀ ∈ g₀.rules, lift_rule (⇑e) r₀ = r) :
CF_language g = CF_language g₀

Renaming the nonterminals of a context-free grammar along an equivalence preserves its language. Both directions go through the lifting machinery: lift_deri pushes a derivation forward along e, and sink_deri pulls one back along e.symm.

The encoding #

source
def ContextFree.EncodedCFG.encodeSymbol {T N : Type} {k : ℕ} (f : N → Fin (k + 1)) :
symbol T N → ℕ ⊕ T

Encode a symbol over Fin (k+1)-valued nonterminals into the raw ℕ ⊕ T format.

Equations
Instances For
    source
    def ContextFree.EncodedCFG.encodeCFG {T : Type} {k : ℕ} (g : CF_grammar T) (e : g.nt ≃ Fin (k + 1)) :
    EncodedCFG T

    Encode a context-free grammar whose nonterminals are indexed by Fin (k+1) (via the equivalence e) as an EncodedCFG.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem ContextFree.EncodedCFG.toNT_val {T : Type} {G : EncodedCFG T} (A : Fin G.ntCount) :
      G.toNT ↑A = A

      toNT is the identity (up to Fin.val) on indices already in range.

      source
      theorem ContextFree.EncodedCFG.encodeCFG_initial {T : Type} {k : ℕ} (g : CF_grammar T) (e : g.nt ≃ Fin (k + 1)) :
      (encodeCFG g e).toCFGrammar.initial = e g.initial
      source
      theorem ContextFree.EncodedCFG.encodeCFG_rules {T : Type} {k : ℕ} (g : CF_grammar T) (e : g.nt ≃ Fin (k + 1)) :
      (encodeCFG g e).toCFGrammar.rules = List.map (lift_rule ⇑e) g.rules

      Soundness and completeness #

      source
      theorem ContextFree.EncodedCFG.contextFreeLanguageOf_isCF {T : Type} (G : EncodedCFG T) :
      contextFreeLanguageOf G ∈ CF

      Soundness: every code denotes a context-free language.

      source
      theorem ContextFree.EncodedCFG.cf_language_encodeCFG {T : Type} {k : ℕ} (g : CF_grammar T) (e : g.nt ≃ Fin (k + 1)) :
      CF_language (encodeCFG g e).toCFGrammar = CF_language g

      The language of the encoding of a finite-nonterminal grammar is the grammar's language.

      source
      theorem ContextFree.EncodedCFG.contextFreeLanguageOf_complete {T : Type} (L : Language T) (hL : L ∈ CF) :
      ∃ (G : EncodedCFG T), contextFreeLanguageOf G = L

      Completeness: every context-free language is denoted by some code.

      source
      theorem ContextFree.EncodedCFG.contextFreeLanguageOf_characterizes {T : Type} :
      Characterizes CF contextFreeLanguageOf

      EncodedCFG characterizes the context-free languages (the library's class CF).