Encoded Right-Regular Grammars

This file introduces a concrete encoded representation of right-regular grammars (EncodedRG) that is Primcodable, together with the language it denotes (regularLanguageOf). It is the shared scaffolding for the uniform computability results proved in Decidability/Membership.lean and Decidability/Emptiness.lean.

Every right-regular grammar is in particular a context-free grammar, so an EncodedRG maps (via toCFG, a primitive-recursive translation) into the encoded context-free grammars EncodedCFG, and regularLanguageOf is defined as the context-free language of that image. The two uniform results are then obtained by composing the already-established uniform CF results (contextFree_computableMembership, contextFree_computableEmptiness) with the primitive-recursive map toCFG.

Restricting the rule shape to the right-regular productions A → a B, A → a, A → ε guarantees that every code denotes a regular language, so this is a faithful encoding of the regular class (and conversely every regular language is generated by some right-regular grammar, hence representable).

Main definitions

• EncodedRG — the encoded right-regular grammar type
• EncodedRG.toCFG — translation to EncodedCFG
• EncodedRG.regularLanguageOf — the denoted language

def Regular.EncodedRG (T : Type) : Type

An encoded right-regular grammar over terminal alphabet T.

The underlying type is ℕ × ℕ × List (ℕ × Option (T × Option ℕ)):

• the first ℕ is the number of nonterminals minus one (so the nonterminal type is Fin (numNT + 1), always nonempty), matching EncodedCFG;
• the second ℕ is the index of the initial nonterminal;
• each rule (lhs, body) has body : Option (T × Option ℕ) encoding exactly one of the three right-regular shapes:
  • none — the rule lhs → ε;
  • some (a, none) — the rule lhs → a;
  • some (a, some B) — the rule lhs → a B.

Because each component is built from ℕ, Option, × and List, the type inherits Primcodable from the standard Mathlib instances (given Primcodable T).

Equations

• Regular.EncodedRG T = (ℕ × ℕ × List (ℕ × Option (T × Option ℕ)))

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

Equations

• Regular.EncodedRG.instPrimcodable = inferInstanceAs (Primcodable (ℕ × ℕ × List (ℕ × Option (T × Option ℕ))))

def Regular.EncodedRG.bodyToRHS {T : Type} : Option (T × Option ℕ) → List (ℕ ⊕ T)

The right-hand side of a rule body in EncodedCFG symbol format.

Equations

• Regular.EncodedRG.bodyToRHS none = []
• Regular.EncodedRG.bodyToRHS (some (a, none)) = [Sum.inr a]
• Regular.EncodedRG.bodyToRHS (some (a, some B)) = [Sum.inr a, Sum.inl B]

def Regular.EncodedRG.toCFG {T : Type} (c : EncodedRG T) : EncodedCFG T

Translate an encoded right-regular grammar to an encoded context-free grammar.

The nonterminal count and initial index are kept; each right-regular rule body is expanded to its context-free right-hand side via bodyToRHS.

Equations

• c.toCFG = (c.1, c.2.1, List.map (fun (r : ℕ × Option (T × Option ℕ)) => (r.1, Regular.EncodedRG.bodyToRHS r.2)) c.2.2)

def Regular.EncodedRG.regularLanguageOf {T : Type} (c : EncodedRG T) : Language T

The language denoted by an encoded right-regular grammar: the context-free language of its context-free image.

Equations

• c.regularLanguageOf = contextFreeLanguageOf c.toCFG

Primitive recursiveness of the translation

theorem Regular.EncodedRG.bodyToRHS_some_primrec {T : Type} [Primcodable T] : Primrec fun (p : T × Option ℕ) => bodyToRHS (some p)

The some-branch of bodyToRHS (case analysis on the optional next nonterminal) is primitive recursive.

theorem Regular.EncodedRG.bodyToRHS_primrec {T : Type} [Primcodable T] : Primrec bodyToRHS

bodyToRHS is primitive recursive.

theorem Regular.EncodedRG.toCFG_primrec {T : Type} [Primcodable T] : Primrec toCFG

toCFG is primitive recursive.