From 7b42cc06dd9a9db2aa340b40f06af19d9b5c1907 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Sun, 9 Nov 2025 15:21:53 -0800 Subject: [PATCH] feat: prove basic properties of deterministic Buchi automata --- Cslib.lean | 1 + Cslib/Computability/Automata/DA.lean | 58 +++++++++++++++---- Cslib/Computability/Automata/DABuchi.lean | 31 ++++++++++ Cslib/Computability/Automata/DAToNA.lean | 35 ++++++++++- Cslib/Computability/Automata/NA.lean | 30 ++++++++-- .../Languages/OmegaRegularLanguage.lean | 35 ++++++++--- 6 files changed, 162 insertions(+), 28 deletions(-) create mode 100644 Cslib/Computability/Automata/DABuchi.lean diff --git a/Cslib.lean b/Cslib.lean index 9cec8a39..dbfef1be 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -1,5 +1,6 @@ import Cslib.Computability.Automata.Acceptor import Cslib.Computability.Automata.DA +import Cslib.Computability.Automata.DABuchi import Cslib.Computability.Automata.DAToNA import Cslib.Computability.Automata.EpsilonNA import Cslib.Computability.Automata.EpsilonNAToNA diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA.lean index 441ab370..5f251e71 100644 --- a/Cslib/Computability/Automata/DA.lean +++ b/Cslib/Computability/Automata/DA.lean @@ -24,6 +24,9 @@ finiteness assumptions), deterministic Buchi automata, and deterministic Muller *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006] -/ +open List Filter Cslib.ωSequence +open scoped Cslib.FLTS + namespace Cslib.Automata structure DA (State Symbol : Type*) extends FLTS State Symbol where @@ -34,6 +37,33 @@ namespace DA variable {State : Type _} {Symbol : Type _} +/-- Helper function for defining `run` below. -/ +@[scoped grind =] +def run' (da : DA State Symbol) (xs : ωSequence Symbol) : ℕ → State + | 0 => da.start + | n + 1 => da.tr (run' da xs n) (xs n) + +/-- Infinite run. -/ +@[scoped grind =] +def run (da : DA State Symbol) (xs : ωSequence Symbol) : ωSequence State := da.run' xs + +@[simp, scoped grind =] +theorem run_zero {da : DA State Symbol} {xs : ωSequence Symbol} : + da.run xs 0 = da.start := + rfl + +@[simp, scoped grind =] +theorem run_succ {da : DA State Symbol} {xs : ωSequence Symbol} {n : ℕ} : + da.run xs (n + 1) = da.tr (da.run xs n) (xs n) := by + rfl + +@[simp, scoped grind =] +theorem mtr_extract_eq_run {da : DA State Symbol} {xs : ωSequence Symbol} {n : ℕ} : + da.mtr da.start (xs.extract 0 n) = da.run xs n := by + induction n + case zero => rfl + case succ n h_ind => grind [extract_succ_right] + /-- A deterministic automaton that accepts finite strings (lists of symbols). -/ structure FinAcc (State Symbol : Type*) extends DA State Symbol where /-- The accept states. -/ @@ -49,19 +79,13 @@ This is the standard string recognition performed by DFAs in the literature. -/ instance : Acceptor (DA.FinAcc State Symbol) Symbol where Accepts (a : DA.FinAcc State Symbol) (xs : List Symbol) := a.mtr a.start xs ∈ a.accept -end FinAcc - -/-- Helper function for defining `run` below. -/ +open Acceptor in @[simp, scoped grind =] -def run' (da : DA State Symbol) (xs : ωSequence Symbol) : ℕ → State - | 0 => da.start - | n + 1 => da.tr (run' da xs n) (xs n) - -/-- Infinite run. -/ -@[scoped grind =] -def run (da : DA State Symbol) (xs : ωSequence Symbol) : ωSequence State := da.run' xs +theorem mem_language {a : FinAcc State Symbol} {xs : List Symbol} : + xs ∈ language a ↔ a.mtr a.start xs ∈ a.accept := + Iff.rfl -open List Filter +end FinAcc /-- Deterministic Buchi automaton. -/ structure Buchi (State Symbol : Type*) extends DA State Symbol where @@ -74,6 +98,12 @@ namespace Buchi instance : ωAcceptor (Buchi State Symbol) Symbol where Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) := ∃ᶠ k in atTop, a.run xs k ∈ a.accept +open ωAcceptor in +@[simp, scoped grind =] +theorem mem_language {a : Buchi State Symbol} {xs : ωSequence Symbol} : + xs ∈ language a ↔ ∃ᶠ k in atTop, a.run xs k ∈ a.accept := + Iff.rfl + end Buchi /-- Deterministic Muller automaton. -/ @@ -87,6 +117,12 @@ namespace Muller instance : ωAcceptor (Muller State Symbol) Symbol where Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) := (a.run xs).infOcc ∈ a.accept +open ωAcceptor in +@[simp, scoped grind =] +theorem mem_language {a : Muller State Symbol} {xs : ωSequence Symbol} : + xs ∈ language a ↔ (a.run xs).infOcc ∈ a.accept := + Iff.rfl + end Muller end DA diff --git a/Cslib/Computability/Automata/DABuchi.lean b/Cslib/Computability/Automata/DABuchi.lean new file mode 100644 index 00000000..27f95c5c --- /dev/null +++ b/Cslib/Computability/Automata/DABuchi.lean @@ -0,0 +1,31 @@ +/- +Copyright (c) 2025 Ching-Tsun Chou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ching-Tsun Chou +-/ + +import Cslib.Computability.Automata.DA +import Cslib.Computability.Automata.NA + +/-! # Deterministic Buchi automata. +-/ + +open Filter + +namespace Cslib.Automata.DA + +open scoped FinAcc Buchi + +variable {State : Type _} {Symbol : Type _} + +open Acceptor ωAcceptor in +/-- The ω-language accepted by a deterministic Buchi automaton is the ω-limit +of the language accepted by the same automaton. +-/ +@[scoped grind =] +theorem buchi_eq_finAcc_omegaLim {da : DA State Symbol} {acc : Set State} : + language (Buchi.mk da acc) = (language (FinAcc.mk da acc))↗ω := by + ext xs ; constructor <;> + { intro h ; apply Frequently.mono h ; simp } + +end Cslib.Automata.DA diff --git a/Cslib/Computability/Automata/DAToNA.lean b/Cslib/Computability/Automata/DAToNA.lean index 128f5f37..566ac264 100644 --- a/Cslib/Computability/Automata/DAToNA.lean +++ b/Cslib/Computability/Automata/DAToNA.lean @@ -26,6 +26,16 @@ def toNA (a : DA State Symbol) : NA State Symbol := instance : Coe (DA State Symbol) (NA State Symbol) where coe := toNA +open scoped FLTS NA in +@[simp, scoped grind =] +theorem toNA_run {a : DA State Symbol} {xs : ωSequence Symbol} {ss : ωSequence State} : + a.toNA.Run xs ss ↔ a.run xs = ss := by + constructor + · rintro _ + ext n + induction n <;> grind + · grind + namespace FinAcc /-- `DA.FinAcc` is a special case of `NA.FinAcc`. -/ @@ -35,8 +45,8 @@ def toNAFinAcc (a : DA.FinAcc State Symbol) : NA.FinAcc State Symbol := open Acceptor in open scoped FLTS NA.FinAcc in -/-- The `NA` constructed from a `DA` has the same language. -/ -@[scoped grind _=_] +/-- The `NA.FinAcc` constructed from a `DA.FinAcc` has the same language. -/ +@[simp, scoped grind _=_] theorem toNAFinAcc_language_eq {a : DA.FinAcc State Symbol} : language a.toNAFinAcc = language a := by ext xs @@ -48,6 +58,27 @@ theorem toNAFinAcc_language_eq {a : DA.FinAcc State Symbol} : end FinAcc +namespace Buchi + +/-- `DA.Buchi` is a special case of `NA.Buchi`. -/ +@[scoped grind =] +def toNABuchi (a : DA.Buchi State Symbol) : NA.Buchi State Symbol := + { a.toNA with accept := a.accept } + +open ωAcceptor in +open scoped NA.Buchi in +/-- The `NA.Buchi` constructed from a `DA.Buchi` has the same ω-language. -/ +@[simp, scoped grind _=_] +theorem toNABuchi_language_eq {a : DA.Buchi State Symbol} : + language a.toNABuchi = language a := by + ext xs ; constructor + · grind + · intro _ + use (a.run xs) + grind + +end Buchi + end NA end Cslib.Automata.DA diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean index 6c6fbfa5..6b3f7b74 100644 --- a/Cslib/Computability/Automata/NA.lean +++ b/Cslib/Computability/Automata/NA.lean @@ -40,6 +40,11 @@ namespace NA variable {State : Type _} {Symbol : Type _} +/-- Infinite run. -/ +@[scoped grind =] +def Run (na : NA State Symbol) (xs : ωSequence Symbol) (ss : ωSequence State) := + ss 0 ∈ na.start ∧ ∀ n, na.Tr (ss n) (xs n) (ss (n + 1)) + /-- A nondeterministic automaton that accepts finite strings (lists of symbols). -/ structure FinAcc (State Symbol : Type*) extends NA State Symbol where /-- The accept states. -/ @@ -56,12 +61,13 @@ instance : Acceptor (FinAcc State Symbol) Symbol where Accepts (a : FinAcc State Symbol) (xs : List Symbol) := ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.MTr s xs s' -end FinAcc +open Acceptor in +@[simp, scoped grind =] +theorem mem_language {a : FinAcc State Symbol} {xs : List Symbol} : + xs ∈ language a ↔ ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.MTr s xs s' := + Iff.rfl -/-- Infinite run. -/ -@[scoped grind =] -def Run (na : NA State Symbol) (xs : ωSequence Symbol) (ss : ωSequence State) := - ss 0 ∈ na.start ∧ ∀ n, na.Tr (ss n) (xs n) (ss (n + 1)) +end FinAcc /-- Nondeterministic Buchi automaton. -/ structure Buchi (State Symbol : Type*) extends NA State Symbol where @@ -72,7 +78,13 @@ namespace Buchi @[scoped grind =] instance : ωAcceptor (Buchi State Symbol) Symbol where Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) := - ∃ ss, ∃ᶠ k in atTop, a.Run xs ss ∧ ss k ∈ a.accept + ∃ ss, a.Run xs ss ∧ ∃ᶠ k in atTop, ss k ∈ a.accept + +open ωAcceptor in +@[simp, scoped grind =] +theorem mem_language {a : Buchi State Symbol} {xs : ωSequence Symbol} : + xs ∈ language a ↔ ∃ ss, a.Run xs ss ∧ ∃ᶠ k in atTop, ss k ∈ a.accept := + Iff.rfl end Buchi @@ -87,6 +99,12 @@ instance : ωAcceptor (Muller State Symbol) Symbol where Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) := ∃ ss, a.Run xs ss ∧ ss.infOcc ∈ a.accept +open ωAcceptor in +@[simp, scoped grind =] +theorem mem_language {a : Muller State Symbol} {xs : ωSequence Symbol} : + xs ∈ language a ↔ ∃ ss, a.Run xs ss ∧ ss.infOcc ∈ a.accept := + Iff.rfl + end Muller end NA diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean index 58493c3f..205b6abf 100644 --- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean +++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean @@ -6,6 +6,9 @@ Authors: Ching-Tsun Chou import Cslib.Computability.Automata.DA import Cslib.Computability.Automata.NA +import Cslib.Computability.Automata.DAToNA +import Cslib.Computability.Automata.DABuchi +import Cslib.Computability.Languages.RegularLanguage import Mathlib.Tactic /-! @@ -14,7 +17,7 @@ import Mathlib.Tactic This file defines ω-regular languages and proves some properties of them. -/ -open Set Function +open Set Function Cslib.Automata.ωAcceptor open scoped Computability open Cslib.Automata @@ -22,18 +25,32 @@ namespace Cslib.ωLanguage variable {Symbol : Type*} -/-- An ω-regular language is one that is accepted by a finite-state Buchi automaton. -/ +/-- An ω-language is ω-regular iff it is accepted by a +finite-state nondeterministic Buchi automaton. -/ def IsRegular (p : ωLanguage Symbol) := - ∃ State : Type, ∃ _ : Finite State, ∃ na : NA.Buchi State Symbol, ωAcceptor.language na = p - -/-- There is an ω-regular language which is not accepted by any deterministic Buchi automaton. -/ -proof_wanted IsRegular.not_det_buchi : + ∃ State : Type, ∃ _ : Finite State, ∃ na : NA.Buchi State Symbol, language na = p + +/-- The ω-language accepted by a finite-state deterministic Buchi automaton is ω-regular. -/ +theorem IsRegular.of_da_buchi {State : Type} [Finite State] (da : DA.Buchi State Symbol) : + (language da).IsRegular := by + use State, inferInstance, da.toNABuchi + simp + +/-- The ω-limit of a regular language is ω-regular. -/ +theorem IsRegular.regular_omegaLim {l : Language Symbol} + (h : l.IsRegular) : (l↗ω).IsRegular := by + obtain ⟨State, _, ⟨da, acc⟩, rfl⟩ := Language.IsRegular.iff_cslib_dfa.mp h + rw [← DA.buchi_eq_finAcc_omegaLim] + apply IsRegular.of_da_buchi + +/-- There is an ω-regular language that is not accepted by any deterministic Buchi automaton. -/ +proof_wanted IsRegular.not_da_buchi : ∃ p : ωLanguage Symbol, p.IsRegular ∧ - ¬ ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Buchi State Symbol, ωAcceptor.language da = p + ¬ ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Buchi State Symbol, language da = p /-- McNaughton's Theorem. -/ -proof_wanted IsRegular.iff_muller_lang {p : ωLanguage Symbol} : +proof_wanted IsRegular.iff_da_muller {p : ωLanguage Symbol} : p.IsRegular ↔ - ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Muller State Symbol, ωAcceptor.language da = p + ∃ State : Type, ∃ _ : Finite State, ∃ da : DA.Muller State Symbol, language da = p end Cslib.ωLanguage