Decidability of Universality

This file proves that universality is decidable for regular languages.

Main results

• regular_universality_decidable – universality of a regular language is decidable
• regular_computableUniversality – universality is uniformly computable for encoded right-regular grammars (ComputableUniversality)

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

Universality of a regular language is decidable.

Equations

• regular_universality_decidable L hL = id (⋯.mpr (regular_emptiness_decidable Lᶜ ⋯))

def Regular.EncodedRG.regularSearchBound {T : Type} (c : EncodedRG T) : ℕ

A coarse subset-DFA state bound for the encoded right-regular grammar.

Equations

• c.regularSearchBound = 2 ^ (c.1 + 2)

theorem Regular.EncodedRG.subsetDFA_card_le_regularSearchBound {T : Type} (c : EncodedRG T) : Fintype.card (Set (Option c.toRG.FinNT)) ≤ c.regularSearchBound

theorem Regular.EncodedRG.regularSearchBound_primrec {T : Type} [Primcodable T] : Primrec regularSearchBound

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

The raw uniform universality decider for encoded right-regular grammars.

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

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