From 89f1e841c5075f490dfecc5be8e99e6a31b58704 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Sun, 5 Jul 2026 13:28:27 -0700 Subject: [PATCH 1/2] feat: topological characterization of safety and liveness properties of infinite sequences --- Cslib.lean | 3 + Cslib/Computability/Automata/NA/Loop.lean | 2 +- .../Languages/OmegaLanguage.lean | 7 + .../Languages/SafetyLiveness.lean | 68 +++++++++ .../Data/OmegaSequence/Topology.lean | 130 ++++++++++++++++++ .../Topology/ClosedDenseDecomposition.lean | 39 ++++++ references.bib | 13 ++ 7 files changed, 261 insertions(+), 1 deletion(-) create mode 100644 Cslib/Computability/Languages/SafetyLiveness.lean create mode 100644 Cslib/Foundations/Data/OmegaSequence/Topology.lean create mode 100644 Cslib/Foundations/Data/Topology/ClosedDenseDecomposition.lean diff --git a/Cslib.lean b/Cslib.lean index 43c374ae7..c62860cef 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -36,6 +36,7 @@ public import Cslib.Computability.Languages.MyhillNerode public import Cslib.Computability.Languages.OmegaLanguage public import Cslib.Computability.Languages.OmegaRegularLanguage public import Cslib.Computability.Languages.RegularLanguage +public import Cslib.Computability.Languages.SafetyLiveness public import Cslib.Computability.Machines.Turing.SingleTape.Defs public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic public import Cslib.Computability.Machines.Turing.SingleTape.NonDeterministic @@ -70,10 +71,12 @@ public import Cslib.Foundations.Data.OmegaSequence.Flatten public import Cslib.Foundations.Data.OmegaSequence.InfOcc public import Cslib.Foundations.Data.OmegaSequence.Init public import Cslib.Foundations.Data.OmegaSequence.Temporal +public import Cslib.Foundations.Data.OmegaSequence.Topology public import Cslib.Foundations.Data.PFunctor.Free public import Cslib.Foundations.Data.RelatesInSteps public import Cslib.Foundations.Data.Set.Saturation public import Cslib.Foundations.Data.StackTape +public import Cslib.Foundations.Data.Topology.ClosedDenseDecomposition public import Cslib.Foundations.Lint.Basic public import Cslib.Foundations.Logic.InferenceSystem public import Cslib.Foundations.Logic.LogicalEquivalence diff --git a/Cslib/Computability/Automata/NA/Loop.lean b/Cslib/Computability/Automata/NA/Loop.lean index 2b543787f..0e2a6f834 100644 --- a/Cslib/Computability/Automata/NA/Loop.lean +++ b/Cslib/Computability/Automata/NA/Loop.lean @@ -189,7 +189,7 @@ theorem loop_language_eq [Inhabited Symbol] (h : ¬ language na = 0) : ext xl; constructor · rintro ⟨s, _, t, h_acc, h_mtr⟩ by_cases h_xl : xl = [] - · grind [mem_add, mem_one] + · grind [Language.mem_add, Language.mem_one] · have : Nonempty na.start := by obtain ⟨_, s0, _, _⟩ := nonempty_iff_ne_empty.mpr h use s0 diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean index 8b5fbb45c..4f25273ed 100644 --- a/Cslib/Computability/Languages/OmegaLanguage.lean +++ b/Cslib/Computability/Languages/OmegaLanguage.lean @@ -8,6 +8,7 @@ module public import Cslib.Computability.Languages.Language public import Cslib.Foundations.Data.OmegaSequence.Flatten +public import Cslib.Foundations.Data.OmegaSequence.Topology public import Mathlib.Computability.Language public import Mathlib.Order.CompleteBooleanAlgebra public import Mathlib.Order.Filter.AtTopBot.Defs @@ -28,6 +29,8 @@ denote languages (namely, sets of finite sequences of type `List α`). universe sets), and the subset relation are denoted using lattice-theoretic notations (`p ∪ q`, `p ∩ q`, `pᶜ`, `⊥`, `⊤`, and `≤`) and terminologies in definition and theorem names ("inf", "sup", "compl", "bot", "top", "le"). +* `p.closure`: the topological closure of `p`, where `ωLanguage α` inherits the + product topology of `TopologicalSpace (ωSequence α)` * `l * p`: ω-language of `x ++ω y` where `x ∈ l` and `y ∈ p`; referred to as "hmul" in definition and theorem names. * `l^ω`: ω-language of infinite sequences each of which is the concatenation of @@ -131,6 +134,10 @@ lemma iInf_def {ι : Sort v} {p : ι → ωLanguage α} : ⨅ i, p i = ⟨⋂ i, ext simp [iInf, sInf_def] +/-- The topological closure of an ω-language. -/ +def closure (p : ωLanguage α) : ωLanguage α := + _root_.closure p.toSet + /-- The concatenation of a language l and an ω-language `p` is the ω-language made of infinite sequences `x ++ω y` where `x ∈ l` and `y ∈ p`. -/ instance : HMul (Language α) (ωLanguage α) (ωLanguage α) where diff --git a/Cslib/Computability/Languages/SafetyLiveness.lean b/Cslib/Computability/Languages/SafetyLiveness.lean new file mode 100644 index 000000000..54018ac3c --- /dev/null +++ b/Cslib/Computability/Languages/SafetyLiveness.lean @@ -0,0 +1,68 @@ +/- +Copyright (c) 2026 Ching-Tsun Chou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ching-Tsun Chou +-/ + +module + +public import Cslib.Computability.Languages.OmegaLanguage +public import Cslib.Foundations.Data.Topology.ClosedDenseDecomposition + +/-! +# Safety and Liveness properties of ω-sequences + +This file formalizes the main results of [AlpernSchneider1985]. Namely, given +an appropriate topology on ω-sequences: +* Safety properties can be identified with closed sets. +* Liveness properties can be identified with dense sets. +* Every property is the intersection of a safety property and a liveness property. + +## References +* [Alpern, Bowen; Schneider, Fred B. (1985). "Defining liveness". +Information Processing Letters. 21 (4): 181–185.][AlpernSchneider1985] +-/ + +@[expose] public section + +namespace Cslib.ωLanguage + +open Set ωSequence TopologicalSpace + +variable {α : Type*} + +/-- Safety properties are identified with closed sets. -/ +abbrev IsSafety (p : ωLanguage α) : Prop := IsClosed p.toSet + +/-- An alternative characterization of `IsSafety` that justifies its definition: +if an ω-sequence violates a safety property, then it has a finite prefix all of whose +infinite extensions also violate the property. -/ +theorem isSafety_iff (p : ωLanguage α) : + p.IsSafety ↔ ∀ xs, xs ∉ p → ∃ n, ∀ ys, (xs.take n) ++ω ys ∉ p := by + simp [← isOpen_compl_iff, isOpen_iff, mem_def] + +/-- Liveness properties are identified with dense sets. -/ +abbrev IsLiveness (p : ωLanguage α) : Prop := Dense p.toSet + +/-- An alternative characterization of `IsLiveness` that justifies its definition: +any finite sequence can be extended to an infinite sequence satisfying a liveness property. -/ +theorem isLiveness_iff (p : ωLanguage α) : + p.IsLiveness ↔ ∀ (xs : ωSequence α) (n : ℕ), ∃ ys, (xs.take n) ++ω ys ∈ p := by + exact Dense_iff p.toSet + +/-- `SafetyLivenessDecomposition p ps pl` means that `ps` is a safety property, +`pl` is a liveness property, and `ps ⊓ pl = p`. -/ +def SafetyLivenessDecomposition (p ps pl : ωLanguage α) : Prop := + IsSafety ps ∧ IsLiveness pl ∧ ps ⊓ pl = p + +/-- Every property `p` is the intersection of the safety property `p.closure` and +the liveness property `p ⊔ p.closureᶜ`. -/ +theorem SafetyLivenessDecomposition_exists (p : ωLanguage α) : + SafetyLivenessDecomposition p p.closure (p ⊔ p.closureᶜ) := by + obtain ⟨_, _, _⟩ := ClosedDenseDecomposition_exists p.toSet + split_ands + · simpa + · simpa [sup_def, closure, compl_def] + · simpa [ωLanguage.ext_iff, sup_def, closure, compl_def] + +end Cslib.ωLanguage diff --git a/Cslib/Foundations/Data/OmegaSequence/Topology.lean b/Cslib/Foundations/Data/OmegaSequence/Topology.lean new file mode 100644 index 000000000..4f5053781 --- /dev/null +++ b/Cslib/Foundations/Data/OmegaSequence/Topology.lean @@ -0,0 +1,130 @@ +/- +Copyright (c) 2026 Ching-Tsun Chou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ching-Tsun Chou +-/ + +module + +public import Cslib.Foundations.Data.OmegaSequence.Init +public import Mathlib.Topology.Homeomorph.TransferInstance +public import Mathlib.Topology.MetricSpace.PiNat + +/-! +# Topology on ω-sequences + +The topology on ω-sequences is essentially the product topology when `ωSequence α` is +viewed as the product space `Π (n : ℕ), α`, where `α` is equipped with the discrete +topology. The notion of "cylinders" are also ported from `Π (n : ℕ), α` and they form +a topological basis. +-/ + +@[expose] public section + +namespace Cslib.ωSequence + +open Set Homeomorph TopologicalSpace ωSequence + +variable {α : Type*} + +/-- Define the topology on `ωSequence α` using an equivalence from it to the product topology +`ℕ → WithDiscreteTopology α`. -/ +instance : TopologicalSpace (ωSequence α) := + haveI eqv : ωSequence α ≃ (ℕ → WithDiscreteTopology α) := { + toFun xs i := .toTopology ⊥ (xs.get i) + invFun f := ωSequence.mk fun i => (f i).ofTopology + left_inv _ := rfl + right_inv _ := rfl + } + eqv.topologicalSpace + +/-- The homeomorphisim from `ωSequence α` to `ℕ → WithDiscreteTopology α`. -/ +def homeomorph : ωSequence α ≃ₜ (ℕ → WithDiscreteTopology α) := Equiv.homeomorph _ + +@[simp] +lemma homeomorph_apply (xs : ωSequence α) (i : Nat) : + homeomorph xs i = .toTopology ⊥ (xs i) := + rfl + +@[simp] +lemma homeomorph_symm_apply (f : ℕ → WithDiscreteTopology α) : + homeomorph.symm f = ωSequence.mk fun i => (f i).ofTopology := + rfl + +/-- Port the notion of "cylinders" from `ℕ → WithDiscreteTopology α` to `ωSequence α`. -/ +def cylinder (xs : ωSequence α) (n : ℕ) : Set (ωSequence α) := + homeomorph ⁻¹' (PiNat.cylinder (homeomorph xs) n) + +/-- An alternative characterization of cylinders in terms of `ωSequence α` alone. -/ +theorem cylinder_def (xs : ωSequence α) (n : ℕ) : + xs.cylinder n = { ys | ∀ k, k < n → ys k = xs k } := by + simp [cylinder, PiNat.cylinder] + +/-- Yet another alternative characterization of cylinders in terms of `ωSequence α` alone. -/ +theorem cylinder_eq_prepend_range (xs : ωSequence α) (n : ℕ) : + xs.cylinder n = range (xs.take n ++ω ·) := by + ext ys + simp only [cylinder_def, mem_setOf_eq, mem_range] + constructor + · intro h + use ys.drop n + suffices xs.take n = ys.take n by grind + apply List.ext_get <;> grind + · grind [get_append_left] + +/-- All cylinders are open sets. -/ +theorem isOpen_cylinder (xs : ωSequence α) (n : ℕ) : + IsOpen (xs.cylinder n) := by + simp [cylinder, PiNat.isOpen_cylinder] + +/-- Every ω-sequence in an open set belongs to a cylinder which is contained in the set. -/ +theorem nhds_cylinders {xs : ωSequence α} {s : Set (ωSequence α)} (hx : xs ∈ s) (hs : IsOpen s) : + ∃ (ys : ωSequence α) (n : ℕ), xs ∈ ys.cylinder n ∧ ys.cylinder n ⊆ s := by + let xs' := homeomorph xs + have hx' : xs' ∈ homeomorph '' s := by grind + have hs' := (isOpen_image homeomorph).mpr hs + have hb := PiNat.isTopologicalBasis_cylinders (fun _ : ℕ ↦ WithDiscreteTopology α) + obtain ⟨_, ⟨ys', n, rfl⟩, hmm, hss⟩ := IsTopologicalBasis.exists_subset_of_mem_open hb hx' hs' + use homeomorph.symm ys', n + split_ands + · exact mem_preimage.mp hmm + · exact preimage_subset hss <| injOn_of_injective <| Homeomorph.injective homeomorph + +/-- The cylinders form a topological basis. -/ +theorem isTopologicalBasis_cylinders : + IsTopologicalBasis { s | ∃ (xs : ωSequence α) (n : ℕ), s = xs.cylinder n } := by + apply isTopologicalBasis_of_isOpen_of_nhds + · grind [isOpen_cylinder] + · grind [nhds_cylinders] + +/-- A set is open iff any ω-sequence in the set has a finite prefix all of whose infinite +extensions are also in the set. -/ +theorem isOpen_iff (s : Set (ωSequence α)) : + IsOpen s ↔ ∀ xs, xs ∈ s → ∃ n, ∀ ys, (xs.take n) ++ω ys ∈ s := by + simp only [IsTopologicalBasis.isOpen_iff isTopologicalBasis_cylinders, + cylinder_eq_prepend_range, mem_setOf_eq, ↓existsAndEq, mem_range, true_and] + constructor <;> intro h xs hxs + · obtain ⟨_, n, ⟨_, rfl⟩, _⟩ := h xs hxs + use n + grind [take_append_of_le_length] + · obtain ⟨n, _⟩ := h xs hxs + use xs, n, ⟨xs.drop n, ?_⟩ <;> grind + +/-- A set is dense iff any finite sequence can be extended to an infinite sequence in the set. -/ +theorem Dense_iff (s : Set (ωSequence α)) : + Dense s ↔ ∀ (xs : ωSequence α) (n : ℕ), ∃ ys, (xs.take n) ++ω ys ∈ s := by + simp only [IsTopologicalBasis.dense_iff isTopologicalBasis_cylinders, cylinder_eq_prepend_range, + mem_setOf_eq, forall_exists_index] + constructor + · intro h xs n + obtain ⟨ys, h1, _⟩ := h (xs.cylinder n) xs n + (by simp [cylinder_eq_prepend_range]) (by use xs; simp [cylinder_def]) + use ys.drop n + suffices xs.take n = ys.take n by grind + grind [cylinder_eq_prepend_range, take_append_of_le_length] + · rintro h c xs n rfl ⟨_, _, rfl⟩ + obtain ⟨ys, _⟩ := h xs n + use xs.take n ++ω ys + grind + +end Cslib.ωSequence diff --git a/Cslib/Foundations/Data/Topology/ClosedDenseDecomposition.lean b/Cslib/Foundations/Data/Topology/ClosedDenseDecomposition.lean new file mode 100644 index 000000000..9b402f015 --- /dev/null +++ b/Cslib/Foundations/Data/Topology/ClosedDenseDecomposition.lean @@ -0,0 +1,39 @@ +/- +Copyright (c) 2026 Ching-Tsun Chou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ching-Tsun Chou +-/ + +module + +public import Mathlib.Topology.Closure + +/-! +# Closed-dense decomposition + +Every set in a topological space is the intersection of a closed set and a dense set. +-/ + +@[expose] public section + +namespace Cslib + +open Set + +variable {X : Type*} [TopologicalSpace X] + +/-- `ClosedDenseDecomposition s sc sd` means that `sc` is a closed set, `sd` is a dense set, +and `sc ∩ sd = s`. -/ +def ClosedDenseDecomposition (s sc sd : Set X) : Prop := + IsClosed sc ∧ Dense sd ∧ sc ∩ sd = s + +/-- Every set `s` in a topological space is the intersection of the closed set `closure s` +and the dense set `s ∪ (closure)ᶜ`. -/ +theorem ClosedDenseDecomposition_exists (s : Set X) : + ClosedDenseDecomposition s (closure s) (s ∪ (closure s)ᶜ) := by + split_ands + · exact isClosed_closure + · simp only [dense_iff_closure_eq, closure_union, ← compl_subset_iff_union, subset_closure] + · simp [inter_union_distrib_left, subset_closure] + +end Cslib diff --git a/references.bib b/references.bib index 18281428d..177170e76 100644 --- a/references.bib +++ b/references.bib @@ -19,6 +19,19 @@ @inproceedings{Aceto1999 bibsource = {dblp computer science bibliography, https://dblp.org} } +@article{AlpernSchneider1985, + author = {Alpern, Bowen and Schneider, Fred B.}, + title = {Defining liveness}, + journal = {Information Processing Letters}, + volume = {21}, + number = {4}, + pages = {181--185}, + year = {1985}, + issn = {0020-0190}, + doi = {10.1016/0020-0190(85)90056-0}, + url = {https://www.sciencedirect.com/science/article/pii/0020019085900560} +} + @article{AngluinLaird1988, author = {Angluin, Dana and Laird, Philip}, title = {Learning from Noisy Examples}, From 8eb16c37c58c64ea1b09b19afdf053fbab1b1e17 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Thu, 9 Jul 2026 12:11:13 -0700 Subject: [PATCH 2/2] fix a missing Cslib.Init import --- Cslib/Foundations/Data/Topology/ClosedDenseDecomposition.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Cslib/Foundations/Data/Topology/ClosedDenseDecomposition.lean b/Cslib/Foundations/Data/Topology/ClosedDenseDecomposition.lean index 9b402f015..e7279b9ec 100644 --- a/Cslib/Foundations/Data/Topology/ClosedDenseDecomposition.lean +++ b/Cslib/Foundations/Data/Topology/ClosedDenseDecomposition.lean @@ -6,6 +6,7 @@ Authors: Ching-Tsun Chou module +public import Cslib.Init public import Mathlib.Topology.Closure /-!