Decidability of Emptiness

This file proves that emptiness is decidable for regular languages.

Main results

• regular_emptiness_decidable – emptiness of a regular language is decidable
• regular_computableEmptiness – emptiness is uniformly computable for encoded right-regular grammars (ComputableEmptiness)

Part 1: Regular Languages

theorem DFA.short_word_of_reachable {α : Type u_1} {σ : Type u_2} [Fintype σ] [DecidableEq σ] (M : DFA α σ) (w : List α) : ∃ (w' : List α), w'.length ≤ Fintype.card σ ∧ M.evalFrom M.start w' = M.evalFrom M.start w

Any state reachable by a DFA can be reached by a word of length at most Fintype.card σ. By the pigeonhole principle.

def DFA.reachableSet {α : Type u_1} {σ : Type u_2} [Fintype α] [Fintype σ] [DecidableEq σ] (M : DFA α σ) : Finset σ

The set of states reachable from M.start by following transitions.

Equations

• M.reachableSet = (fun (S : Finset σ) => S ∪ Finset.univ.biUnion fun (a : α) => Finset.image (fun (x : σ) => M.step x a) S)^[Fintype.card σ] {M.start}

theorem DFA.mem_reachableSet_iff {α : Type u_1} {σ : Type u_2} [Fintype α] [Fintype σ] [DecidableEq σ] (M : DFA α σ) (s : σ) : s ∈ M.reachableSet ↔ ∃ (w : List α), M.evalFrom M.start w = s

A state is in reachableSet iff it is reachable from M.start by some word.

noncomputable def dfa_emptiness_decidable {α : Type u_1} {σ : Type u_2} [Fintype α] [Fintype σ] [DecidableEq α] [DecidableEq σ] (M : DFA α σ) [DecidablePred fun (x : σ) => x ∈ M.accept] : Decidable (M.accepts = ∅)

Emptiness of a DFA's accepted language is decidable.

Equations

• dfa_emptiness_decidable M = ⋯.mpr inferInstance

noncomputable def regular_emptiness_decidable {α : Type u_1} [Fintype α] [DecidableEq α] (L : Language α) (hL : L.IsRegular) : Decidable (L = ∅)

Emptiness of a regular language is decidable.

Equations

• regular_emptiness_decidable L hL = ⋯.mpr (dfa_emptiness_decidable (Classical.choose ⋯))

Part 2: Uniform computability over encoded right-regular grammars

theorem Regular.EncodedRG.regular_emptiness_computablePred {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] : ComputablePred fun (c : EncodedRG T) => c.regularLanguageOf = ∅

The raw uniform emptiness decider for encoded right-regular grammars, obtained by composing the context-free emptiness decider with the primitive-recursive translation toCFG : EncodedRG T → EncodedCFG T.

theorem Regular.EncodedRG.regular_computableEmptiness {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] : ComputableEmptiness RG regularLanguageOf

Emptiness is uniformly computable for the regular languages: encoded right-regular grammars are an adequate, effective presentation (regularLanguageOf_characterizes) with uniformly decidable emptiness.