Encoded Context-Free Grammars and Uniform Computability of Emptiness

This file introduces a concrete encoded representation of context-free grammars (EncodedCFG) that is Primcodable, enabling a genuine uniform computability theorem for CFG emptiness where the grammar itself is the argument.

Encoding

An EncodedCFG T is a triple (numNT, initial, rules) where:

• numNT : ℕ — the number of nonterminals minus one (the actual nonterminal type is Fin (numNT + 1), ensuring it is always nonempty)
• initial : ℕ — index of the initial nonterminal (taken mod numNT + 1)
• rules : List (ℕ × List (ℕ ⊕ T)) — production rules, where Sum.inl k represents nonterminal k % (numNT + 1) and Sum.inr t represents terminal t

The underlying type is ℕ × ℕ × List (ℕ × List (ℕ ⊕ T)), which inherits Primcodable from the standard Mathlib instances for products, sums, lists, and ℕ (plus Primcodable T). It is Primcodable because each component is: ℕ has Primcodable.nat, ⊕ has Primcodable.sum, List has Primcodable.list, and × has Primcodable.prod.

Main results

• EncodedCFG — the encoded grammar type
• EncodedCFG.toCFGrammar — translation to the project's CF_grammar T

The Encoded Grammar Type

def EncodedCFG (T : Type) : Type

An encoded context-free grammar over terminal alphabet T.

Equations

• EncodedCFG T = (ℕ × ℕ × List (ℕ × List (ℕ ⊕ T)))

instance EncodedCFG.instPrimcodable {T : Type} [Primcodable T] : Primcodable (EncodedCFG T)

Equations

• EncodedCFG.instPrimcodable = inferInstanceAs (Primcodable (ℕ × ℕ × List (ℕ × List (ℕ ⊕ T))))

instance EncodedCFG.instDecidableEq {T : Type} [DecidableEq T] : DecidableEq (EncodedCFG T)

Equations

• EncodedCFG.instDecidableEq = instDecidableEqProd

def EncodedCFG.numNT {T : Type} (G : EncodedCFG T) : ℕ

Equations

• G.numNT = G.1

def EncodedCFG.initialIdx {T : Type} (G : EncodedCFG T) : ℕ

Equations

• G.initialIdx = G.2.1

def EncodedCFG.rawRules {T : Type} (G : EncodedCFG T) : List (ℕ × List (ℕ ⊕ T))

Equations

• G.rawRules = G.2.2

def EncodedCFG.ntCount {T : Type} (G : EncodedCFG T) : ℕ

Equations

• G.ntCount = G.numNT + 1

theorem EncodedCFG.ntCount_pos {T : Type} (G : EncodedCFG T) : 0 < G.ntCount

def EncodedCFG.toNT {T : Type} (G : EncodedCFG T) (k : ℕ) : Fin G.ntCount

Equations

• G.toNT k = ⟨k % G.ntCount, ⋯⟩

def EncodedCFG.toSymbol {T : Type} (G : EncodedCFG T) : ℕ ⊕ T → symbol T (Fin G.ntCount)

Equations

• G.toSymbol (Sum.inl k) = symbol.nonterminal (G.toNT k)
• G.toSymbol (Sum.inr t) = symbol.terminal t

def EncodedCFG.toCFGrammar {T : Type} (G : EncodedCFG T) : CF_grammar T

Equations

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

instance EncodedCFG.instFintypeNtToCFGrammar {T : Type} (G : EncodedCFG T) : Fintype G.toCFGrammar.nt

Equations

• G.instFintypeNtToCFGrammar = inferInstanceAs (Fintype (Fin G.ntCount))

instance EncodedCFG.instDecidableEqNtToCFGrammar {T : Type} (G : EncodedCFG T) : DecidableEq G.toCFGrammar.nt

Equations

• G.instDecidableEqNtToCFGrammar = inferInstanceAs (DecidableEq (Fin G.ntCount))