Encoded Context-Free Grammars and Uniform Computability of Emptiness

Shows a computability theorem for CFG emptiness where the grammar itself is the argument.

Main results

• encoded_cf_emptiness_decidable — constructive Decidable instance for emptiness of the language of an encoded grammar
• encoded_cf_emptiness_computable — ComputablePred for emptiness, where the grammar is the argument (uniform over all encoded grammars)

Part 1: Productive Nonterminals Algorithm

def ChomskyNormalFormGrammar.productiveInit {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] : Finset g.NT

Initialize the productive nonterminals set: all nonterminals with leaf rules.

Equations

• g.productiveInit = g.rules.biUnion fun (r : ChomskyNormalFormRule T g.NT) => match r with | ChomskyNormalFormRule.leaf n t => {n} | ChomskyNormalFormRule.node n l r => ∅

def ChomskyNormalFormGrammar.productiveStep {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] (S : Finset g.NT) : Finset g.NT

One step of the productive nonterminals fixpoint: add nonterminals whose node rule has both children already in S.

Equations

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

def ChomskyNormalFormGrammar.productiveNTs {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] : Finset g.NT

The set of productive nonterminals, computed by iterating productiveStep g.rules.card times.

Equations

• g.productiveNTs = g.productiveStep^[g.rules.card] g.productiveInit

def ChomskyNormalFormGrammar.ruleInputs {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] : Finset g.NT

The set of all nonterminals that appear as inputs of rules.

Equations

• g.ruleInputs = Finset.image (fun (r : ChomskyNormalFormRule T g.NT) => r.input) g.rules

Part 2: Monotonicity

theorem ChomskyNormalFormGrammar.productiveStep_subset_self {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] (S : Finset g.NT) : S ⊆ g.productiveStep S

theorem ChomskyNormalFormGrammar.iterate_productiveStep_mono {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] {n m : ℕ} (h : n ≤ m) : g.productiveStep^[n] g.productiveInit ⊆ g.productiveStep^[m] g.productiveInit

Part 3: Range bound – productive nonterminals are rule inputs

theorem ChomskyNormalFormGrammar.productiveInit_subset_ruleInputs {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] : g.productiveInit ⊆ g.ruleInputs

theorem ChomskyNormalFormGrammar.productiveStep_subset_ruleInputs {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] {S : Finset g.NT} (hS : S ⊆ g.ruleInputs) : g.productiveStep S ⊆ g.ruleInputs

theorem ChomskyNormalFormGrammar.iterate_productiveStep_subset_ruleInputs {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] (n : ℕ) : g.productiveStep^[n] g.productiveInit ⊆ g.ruleInputs

Part 4: Fixpoint property

theorem ChomskyNormalFormGrammar.productiveNTs_is_fixpoint {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] : g.productiveStep g.productiveNTs = g.productiveNTs

Part 5: Soundness

theorem ChomskyNormalFormGrammar.canDerive_node {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] (n c1 c2 : g.NT) (w1 w2 : List T) (hrule : ChomskyNormalFormRule.node n c1 c2 ∈ g.rules) (h1 : g.canDerive c1 w1) (h2 : g.canDerive c2 w2) : g.canDerive n (w1 ++ w2)

theorem ChomskyNormalFormGrammar.productiveInit_sound {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] (nt : g.NT) (h : nt ∈ g.productiveInit) : ∃ (w : List T), g.canDerive nt w

theorem ChomskyNormalFormGrammar.productiveStep_sound {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] (S : Finset g.NT) (hS : ∀ nt ∈ S, ∃ (w : List T), g.canDerive nt w) (nt : g.NT) (h : nt ∈ g.productiveStep S) : ∃ (w : List T), g.canDerive nt w

theorem ChomskyNormalFormGrammar.productiveNTs_sound {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] (nt : g.NT) (h : nt ∈ g.productiveNTs) : ∃ (w : List T), g.canDerive nt w

Part 6: Completeness

theorem ChomskyNormalFormGrammar.productive_mem_fixpoint {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] (S : Finset g.NT) (h_init : g.productiveInit ⊆ S) (h_fix : g.productiveStep S = S) (nt : g.NT) (w : List T) (hw : g.canDerive nt w) : nt ∈ S

theorem ChomskyNormalFormGrammar.productiveNTs_complete {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] (nt : g.NT) (w : List T) (h : g.canDerive nt w) : nt ∈ g.productiveNTs

Part 7: Main Correctness

theorem ChomskyNormalFormGrammar.mem_productiveNTs_iff {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] (nt : g.NT) : nt ∈ g.productiveNTs ↔ ∃ (w : List T), g.canDerive nt w

theorem ChomskyNormalFormGrammar.language_eq_empty_iff {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] : g.language = ∅ ↔ g.initial ∉ g.productiveNTs

Part 8: Constructive Decidability

def ChomskyNormalFormGrammar.cnf_emptiness_dec {T : Type} (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] : Decidable (g.language = ∅)

Emptiness of a CNF grammar's language is decidable (constructively, without Classical.propDecidable).

Equations

• g.cnf_emptiness_dec = if h : g.initial ∈ g.productiveNTs then isFalse ⋯ else isTrue ⋯

Part 9: Context-Free Languages – General CFG

noncomputable def cf_emptiness_decidable {T : Type} [DecidableEq T] (g : CF_grammar T) [Fintype g.nt] [DecidableEq g.nt] : Decidable (CF_language g = ∅)

Equations

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

Decidability and Computability

noncomputable def encoded_cf_emptiness_decidable {T : Type} [DecidableEq T] (G : EncodedCFG T) : Decidable (CF_language G.toCFGrammar = ∅)

Equations

• encoded_cf_emptiness_decidable G = cf_emptiness_decidable G.toCFGrammar

Direct Emptiness Check

All nonterminal indices are normalized modulo ntCount to ensure the algorithm correctly identifies productive nonterminals regardless of the raw index values used in the encoding.

def allNTsInListN {T : Type} (nc : ℕ) (rhs : List (ℕ ⊕ T)) (S : List ℕ) : Bool

Check whether all nonterminal indices (mod nc) in a rule's RHS appear in the set S (a list of ℕ). Terminals always pass.

Equations

• allNTsInListN nc rhs S = rhs.all fun (s : ℕ ⊕ T) => match s with | Sum.inl k => decide (k % nc ∈ S) | Sum.inr val => true

def prodStepN {T : Type} (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (S : List ℕ) : List ℕ

One step of the productive-nonterminals fixpoint on encoded rules. Each LHS is normalized mod nc before addition.

Equations

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

def prodNTsN {T : Type} (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) : List ℕ

Compute the productive nonterminals by iterating prodStepN.

Equations

• prodNTsN nc rules = (prodStepN nc rules)^[rules.length] []

def checkCFGEmpty {T : Type} (G : EncodedCFG T) : Bool

Check whether the encoded CFG has an empty language.

Equations

• checkCFGEmpty G = !decide (G.initialIdx % G.ntCount ∈ prodNTsN G.ntCount G.rawRules)

Correctness

def IsProductive {T : Type} (g : CF_grammar T) (nt : g.nt) : Prop

Equations

• IsProductive g nt = ∃ (w : List T), CF_derives g [symbol.nonterminal nt] (List.map symbol.terminal w)

theorem CF_language_eq_empty_iff_not_productive {T : Type} (g : CF_grammar T) : CF_language g = ∅ ↔ ¬IsProductive g g.initial

theorem mem_prodStepN_of_mem {T : Type} (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (S : List ℕ) (x : ℕ) (hx : x ∈ S) : x ∈ prodStepN nc rules S

theorem productive_sentential_form {T : Type} (g : CF_grammar T) (syms : List (symbol T g.nt)) (h : ∀ s ∈ syms, match s with | symbol.terminal a => True | symbol.nonterminal nt => IsProductive g nt) : ∃ (w : List T), CF_derives g syms (List.map symbol.terminal w)

theorem productive_from_rule {T : Type} (G : EncodedCFG T) (lhs : ℕ) (rhs : List (ℕ ⊕ T)) (hrule : (lhs, rhs) ∈ G.rawRules) (hprod : ∀ (k : ℕ), Sum.inl k ∈ rhs → IsProductive G.toCFGrammar (G.toNT k)) : IsProductive G.toCFGrammar (G.toNT lhs)

theorem prodStepN_sound_step {T : Type} (G : EncodedCFG T) (S : List ℕ) (hS : ∀ k ∈ S, IsProductive G.toCFGrammar (G.toNT k)) (k : ℕ) : k ∈ prodStepN G.ntCount G.rawRules S → IsProductive G.toCFGrammar (G.toNT k)

theorem prodNTsN_sound {T : Type} (G : EncodedCFG T) (k : ℕ) (hk : k ∈ prodNTsN G.ntCount G.rawRules) : IsProductive G.toCFGrammar (G.toNT k)

theorem mem_prodStepN_of_rule {T : Type} (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (S : List ℕ) (lhs : ℕ) (rhs : List (ℕ ⊕ T)) (hrule : (lhs, rhs) ∈ rules) (hall : allNTsInListN nc rhs S = true) : lhs % nc ∈ prodStepN nc rules S

theorem iterate_nodup {T : Type} (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (n : ℕ) : ((prodStepN nc rules)^[n] []).Nodup

theorem prodNTsN_fixpoint {T : Type} (nc : ℕ) (rules : List (ℕ × List (ℕ ⊕ T))) (x : ℕ) : x ∈ prodStepN nc rules (prodNTsN nc rules) ↔ x ∈ prodNTsN nc rules

theorem fixpoint_rule_closed {T : Type} (G : EncodedCFG T) (S : List ℕ) (hfix : ∀ (x : ℕ), x ∈ prodStepN G.ntCount G.rawRules S ↔ x ∈ S) (nt : Fin G.ntCount) (rhs : List (symbol T (Fin G.ntCount))) (hrule : (nt, rhs) ∈ G.toCFGrammar.rules) (hall : ∀ (nt' : Fin G.ntCount), symbol.nonterminal nt' ∈ rhs → ↑nt' ∈ S) : ↑nt ∈ S

theorem all_nts_in_S_of_derives {T : Type} (G : EncodedCFG T) (S : List ℕ) (hfix : ∀ (x : ℕ), x ∈ prodStepN G.ntCount G.rawRules S ↔ x ∈ S) (syms : List (symbol T (Fin G.ntCount))) (w : List T) (hd : CF_derives G.toCFGrammar syms (List.map symbol.terminal w)) (nt : Fin G.ntCount) : symbol.nonterminal nt ∈ syms → ↑nt ∈ S

theorem fixpoint_captures_productive {T : Type} (G : EncodedCFG T) (S : List ℕ) (hfix : ∀ (x : ℕ), x ∈ prodStepN G.ntCount G.rawRules S ↔ x ∈ S) (nt : Fin G.ntCount) (h : IsProductive G.toCFGrammar nt) : ↑nt ∈ S

For a fixpoint S, if all nonterminals in a sentential form that derives some terminal string have their indices in S, and a rule (nt, rhs) with rhs = that form is in the grammar, then nt's index is in S.

theorem complete_of_fixpoint {T : Type} (G : EncodedCFG T) (S : List ℕ) (hfix : ∀ (x : ℕ), x ∈ prodStepN G.ntCount G.rawRules S ↔ x ∈ S) (k : ℕ) (hk : IsProductive G.toCFGrammar (G.toNT k)) : k % G.ntCount ∈ S

theorem prodNTsN_complete {T : Type} (G : EncodedCFG T) (k : ℕ) (hk : IsProductive G.toCFGrammar (G.toNT k)) : k % G.ntCount ∈ prodNTsN G.ntCount G.rawRules

theorem checkCFGEmpty_iff {T : Type} (G : EncodedCFG T) : checkCFGEmpty G = true ↔ CF_language G.toCFGrammar = ∅

Computability

theorem checkCFGEmpty_computable {T : Type} [Primcodable T] : Computable checkCFGEmpty

theorem encoded_cf_emptiness_computable {T : Type} [Primcodable T] : ComputablePred fun (G : EncodedCFG T) => CF_language G.toCFGrammar = ∅

theorem contextFree_emptiness_computablePred {T : Type} [Primcodable T] : ComputablePred fun (c : EncodedCFG T) => contextFreeLanguageOf c = ∅

Context-free emptiness is uniformly computable for encoded CFGs (raw ComputablePred decider; the packaged ComputableEmptiness over the CF class lives in ContextFree/Decidability/Characterization.lean).

theorem contextFree_computableEmptiness {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] : ComputableEmptiness CF contextFreeLanguageOf

Emptiness is uniformly computable for the context-free languages: encoded context-free grammars are an adequate, effective presentation (contextFreeLanguageOf_characterizes) with uniformly decidable emptiness (ComputableEmptiness).