Decidability of Equivalence for Regular Languages

This file proves that equivalence is decidable for regular languages.

The proof reduces equivalence to emptiness of the symmetric difference: L₁ = L₂ ↔ symmDiff L₁ L₂ = ∅, and the symmetric difference is regular (by closure under complement, intersection, and union).

Main results

• regular_equivalence_decidable — equivalence of two regular languages is decidable.
• regular_computableEquivalence – equivalence is uniformly computable for encoded right-regular grammars (ComputableEquivalence)

theorem eq_iff_symmDiff_eq_bot {α : Type u_1} (L₁ L₂ : Language α) : L₁ = L₂ ↔ symmDiff L₁ L₂ = ⊥

theorem symmDiff_isRegular {α : Type u_1} {L₁ L₂ : Language α} (h₁ : L₁.IsRegular) (h₂ : L₂.IsRegular) : (symmDiff L₁ L₂).IsRegular

noncomputable def regular_equivalence_decidable {α : Type u_1} [Fintype α] [DecidableEq α] (L₁ L₂ : Language α) (h₁ : L₁.IsRegular) (h₂ : L₂.IsRegular) : Decidable (L₁ = L₂)

Equivalence of two regular languages is decidable.

Equations

• regular_equivalence_decidable L₁ L₂ h₁ h₂ = ⋯.mpr (regular_emptiness_decidable (symmDiff L₁ L₂) ⋯)

Uniform computability over encoded right-regular grammars

def Regular.EncodedRG.regularEquivalenceSearchBound {T : Type} (p : EncodedRG T × EncodedRG T) : ℕ

A coarse product subset-DFA state bound for comparing two encoded right-regular grammars.

Equations

• Regular.EncodedRG.regularEquivalenceSearchBound p = p.1.regularSearchBound * p.2.regularSearchBound

theorem Regular.EncodedRG.regular_equivalence_computablePred {T : Type} [Fintype T] [DecidableEq T] [Primcodable T] : ComputablePred fun (p : EncodedRG T × EncodedRG T) => p.1.regularLanguageOf = p.2.regularLanguageOf

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

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

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