Least and greatest fixed points on finite sets

10 fully proved

Finite Iteration

DefinitionLeast fixed point of a finset map by finite iteration#✓fully proved

Let \(\alpha\) be a finite type with \(|\alpha|\) elements, let \(f\) map subsets of \(\alpha\) to subsets of \(\alpha\), and write \(f^n\) for the \(n\)-fold iterate of \(f\). Then \(\mathrm{lfp}_{\mathrm{fin}}(f)\) is the set \(f^{|\alpha|}(\emptyset)\), obtained by applying \(f\) to the empty set \(|\alpha|\) times.

For monotone \(f\) the iteration has stabilized after \(|\alpha|\) steps, and the result is the least fixed point of \(f\).

def lfpFin (f : Finset α → Finset α) : Finset α :=
  f^[Fintype.card α] ∅

Used by 10

Used byFinite existential-until set · Correctness of the finite fixed-point computation of EU · Finite iteration from the empty set reaches a fixed point · The finite least fixed point lies in every pre-fixed point · Finite iteration computes the least fixed point · Membership in the set reachable from finitely many sources · Elements reachable from a finite set of sources · A state is reachable exactly when some word leads to it · Reachable states of a DFA · The early-stopping search finds exactly the reachable states

DefinitionGreatest fixed point of a finset map by finite iteration#✓fully proved

Let \(\alpha\) be a finite type with \(|\alpha|\) elements, let \(f\) map subsets of \(\alpha\) to subsets of \(\alpha\), and write \(f^n\) for the \(n\)-fold iterate of \(f\). Then \(\mathrm{gfp}_{\mathrm{fin}}(f)\) is the set \(f^{|\alpha|}(\alpha)\), obtained by applying \(f\) to the whole of \(\alpha\) \(|\alpha|\) times.

For monotone \(f\) the iteration has stabilized after \(|\alpha|\) steps, and the result is the greatest fixed point of \(f\).

def gfpFin (f : Finset α → Finset α) : Finset α :=
  f^[Fintype.card α] Finset.univ

Used by 5

Used byFinite existential-globally set · Correctness of the finite fixed-point computation of EG · Finite iteration from the whole type reaches a fixed point · Every post-fixed point lies in the finite greatest fixed point · Finite iteration computes the greatest fixed point

TheoremFinite iteration from the empty set reaches a fixed point#✓fully proved

Let \(\alpha\) be a finite type with \(|\alpha|\) elements, let \(f\) be a map from subsets of \(\alpha\) to subsets of \(\alpha\) that is monotone for inclusion, and let \(\mathrm{lfp}_{\mathrm{fin}}(f) = f^{|\alpha|}(\emptyset)\) be the result of applying \(f\) to \(\emptyset\) \(|\alpha|\) times. Then \(\mathrm{lfp}_{\mathrm{fin}}(f)\) is a fixed point of \(f\), that is, \(f(\mathrm{lfp}_{\mathrm{fin}}(f)) = \mathrm{lfp}_{\mathrm{fin}}(f)\).

The iterates of \(f\) from \(\emptyset\) form an increasing chain, and until it stabilizes each step strictly increases the cardinality, which is bounded by \(|\alpha|\).

theorem lfpFin_fixed {f : Finset α → Finset α} (hf : Monotone f) :
    f (lfpFin f) = lfpFin f

Uses 1 · Used by 4

Statement usesLeast fixed point of a finset map by finite iteration

Used byFinite iteration computes the least fixed point · Membership in the set reachable from finitely many sources · A state is reachable exactly when some word leads to it · The early-stopping search finds exactly the reachable states

TheoremFinite iteration from the whole type reaches a fixed point#✓fully proved

Let \(\alpha\) be a finite type with \(|\alpha|\) elements, let \(f\) be a map from subsets of \(\alpha\) to subsets of \(\alpha\) that is monotone for inclusion, and let \(\mathrm{gfp}_{\mathrm{fin}}(f) = f^{|\alpha|}(\alpha)\) be the result of applying \(f\) to \(\alpha\) \(|\alpha|\) times. Then \(\mathrm{gfp}_{\mathrm{fin}}(f)\) is a fixed point of \(f\), that is, \(f(\mathrm{gfp}_{\mathrm{fin}}(f)) = \mathrm{gfp}_{\mathrm{fin}}(f)\).

The iterates of \(f\) from \(\alpha\) form a decreasing chain, and until it stabilizes each step strictly decreases the cardinality.

theorem gfpFin_fixed {f : Finset α → Finset α} (hf : Monotone f) :
    f (gfpFin f) = gfpFin f

Uses 1 · Used by 3

Statement usesGreatest fixed point of a finset map by finite iteration

Used byFinite iteration computes the greatest fixed point · Correctness of Moore's refinement · Moore's minimal automaton

TheoremThe finite least fixed point lies in every pre-fixed point#✓fully proved

Let \(\alpha\) be a finite type with \(|\alpha|\) elements, let \(f\) be a map from subsets of \(\alpha\) to subsets of \(\alpha\) that is monotone for inclusion, and let \(\mathrm{lfp}_{\mathrm{fin}}(f) = f^{|\alpha|}(\emptyset)\) be the result of applying \(f\) to \(\emptyset\) \(|\alpha|\) times. If \(Z \subseteq \alpha\) satisfies \(f(Z) \subseteq Z\), then \(\mathrm{lfp}_{\mathrm{fin}}(f) \subseteq Z\).

Every iterate of \(f\) from \(\emptyset\) is contained in \(Z\), by induction.

theorem lfpFin_le {f : Finset α → Finset α} (hf : Monotone f)
    {Z : Finset α} (hZ : f Z ⊆ Z) : lfpFin f ⊆ Z

Uses 1 · Used by 2

Statement usesLeast fixed point of a finset map by finite iteration

Used byMembership in the set reachable from finitely many sources · A state is reachable exactly when some word leads to it

TheoremEvery post-fixed point lies in the finite greatest fixed point#✓fully proved

Let \(\alpha\) be a finite type with \(|\alpha|\) elements, let \(f\) be a map from subsets of \(\alpha\) to subsets of \(\alpha\) that is monotone for inclusion, and let \(\mathrm{gfp}_{\mathrm{fin}}(f) = f^{|\alpha|}(\alpha)\) be the result of applying \(f\) to \(\alpha\) \(|\alpha|\) times. If \(Z \subseteq \alpha\) satisfies \(Z \subseteq f(Z)\), then \(Z \subseteq \mathrm{gfp}_{\mathrm{fin}}(f)\).

\(Z\) is contained in every iterate of \(f\) from \(\alpha\), by induction.

theorem le_gfpFin {f : Finset α → Finset α} (hf : Monotone f)
    {Z : Finset α} (hZ : Z ⊆ f Z) : Z ⊆ gfpFin f

Uses 1

Statement usesGreatest fixed point of a finset map by finite iteration

Bridge

TheoremFinset and predicate iterations from the bottom agree#✓fully proved

Let \(\alpha\) be a type, let \(f\) map finite subsets of \(\alpha\) to finite subsets of \(\alpha\), and let \(F\) map predicates on \(\alpha\) to predicates on \(\alpha\). For a finite set \(Z \subseteq \alpha\) write \(P_Z\) for the predicate \(t \mapsto t \in Z\), and suppose that for every finite \(Z \subseteq \alpha\) and every \(s \in \alpha\), \(s \in f(Z)\) if and only if \(F(P_Z)(s)\) holds. Write \(f^n\) and \(F^n\) for the \(n\)-fold iterates and \(\bot\) for the predicate that is false everywhere. Then for every \(n \in \mathbb{N}\) and every \(s \in \alpha\), \(s \in f^n(\emptyset)\) if and only if \(F^n(\bot)(s)\) holds.

theorem mem_finset_iterate_iff {F : (α → Prop) → α → Prop}
    {f : Finset α → Finset α}
    (hbridge : ∀ Z s, s ∈ f Z ↔ F (fun t => t ∈ Z) s) :
    ∀ n s, s ∈ f^[n] ∅ ↔ (F^[n] (fun _ => False)) s

Used by 1

Used byFinite iteration computes the least fixed point

TheoremFinset and predicate iterations from the top agree#✓fully proved

Let \(\alpha\) be a finite type, let \(f\) map subsets of \(\alpha\) to subsets of \(\alpha\), and let \(F\) map predicates on \(\alpha\) to predicates on \(\alpha\). For \(Z \subseteq \alpha\) write \(P_Z\) for the predicate \(t \mapsto t \in Z\), and suppose that for every \(Z \subseteq \alpha\) and every \(s \in \alpha\), \(s \in f(Z)\) if and only if \(F(P_Z)(s)\) holds. Write \(f^n\) and \(F^n\) for the \(n\)-fold iterates and \(\top\) for the predicate that is true everywhere. Then for every \(n \in \mathbb{N}\) and every \(s \in \alpha\), \(s \in f^n(\alpha)\) if and only if \(F^n(\top)(s)\) holds.

theorem mem_finset_iterate_univ_iff {F : (α → Prop) → α → Prop}
    {f : Finset α → Finset α}
    (hbridge : ∀ Z s, s ∈ f Z ↔ F (fun t => t ∈ Z) s) :
    ∀ n s, s ∈ f^[n] Finset.univ ↔ (F^[n] (fun _ => True)) s

Used by 1

Used byFinite iteration computes the greatest fixed point

TheoremFinite iteration computes the least fixed point#✓fully proved

Let \(\alpha\) be a finite type with \(|\alpha|\) elements, let \(f\) be a map from subsets of \(\alpha\) to subsets of \(\alpha\) that is monotone for inclusion, and let \(\mathrm{lfp}_{\mathrm{fin}}(f) = f^{|\alpha|}(\emptyset)\) be the result of applying \(f\) to \(\emptyset\) \(|\alpha|\) times. Let \(F\) be a map from predicates on \(\alpha\) to predicates on \(\alpha\) that is monotone for the pointwise order. For \(Z \subseteq \alpha\) write \(P_Z\) for the predicate \(t \mapsto t \in Z\), and suppose that for every \(Z \subseteq \alpha\) and every \(s \in \alpha\), \(s \in f(Z)\) if and only if \(F(P_Z)(s)\) holds. Then for every \(s \in \alpha\), \(s \in \mathrm{lfp}_{\mathrm{fin}}(f)\) if and only if \(s\) satisfies the least fixed point of \(F\) in the complete lattice of predicates on \(\alpha\).

One inclusion is iteration into the fixed point; the other is Park induction: the \(|\alpha|\)-th iterate of \(F\) from the everywhere-false predicate is pre-fixed because the corresponding iterate of \(f\) has stabilized, transported through the hypothesis relating \(f\) and \(F\).

theorem mem_lfpFin_iff_lfp {F : (α → Prop) → α → Prop}
    {f : Finset α → Finset α}
    (hfm : Monotone f) (hFm : Monotone F)
    (hbridge : ∀ Z s, s ∈ f Z ↔ F (fun t => t ∈ Z) s) (s : α) :
    s ∈ lfpFin f ↔
      (⟨F, hFm⟩ : (α → Prop) →o (α → Prop)).lfp s

Uses 3 · Used by 1

Statement usesLeast fixed point of a finset map by finite iteration

Proof usesFinite iteration from the empty set reaches a fixed point · Finset and predicate iterations from the bottom agree

Used byCorrectness of the finite fixed-point computation of EU

TheoremFinite iteration computes the greatest fixed point#✓fully proved

Let \(\alpha\) be a finite type with \(|\alpha|\) elements, let \(f\) be a map from subsets of \(\alpha\) to subsets of \(\alpha\) that is monotone for inclusion, and let \(\mathrm{gfp}_{\mathrm{fin}}(f) = f^{|\alpha|}(\alpha)\) be the result of applying \(f\) to \(\alpha\) \(|\alpha|\) times. Let \(F\) be a map from predicates on \(\alpha\) to predicates on \(\alpha\) that is monotone for the pointwise order. For \(Z \subseteq \alpha\) write \(P_Z\) for the predicate \(t \mapsto t \in Z\), and suppose that for every \(Z \subseteq \alpha\) and every \(s \in \alpha\), \(s \in f(Z)\) if and only if \(F(P_Z)(s)\) holds. Then for every \(s \in \alpha\), \(s \in \mathrm{gfp}_{\mathrm{fin}}(f)\) if and only if \(s\) satisfies the greatest fixed point of \(F\) in the complete lattice of predicates on \(\alpha\).

This is dual to the corresponding statement for least fixed points.

theorem mem_gfpFin_iff_gfp {F : (α → Prop) → α → Prop}
    {f : Finset α → Finset α}
    (hfm : Monotone f) (hFm : Monotone F)
    (hbridge : ∀ Z s, s ∈ f Z ↔ F (fun t => t ∈ Z) s) (s : α) :
    s ∈ gfpFin f ↔
      (⟨F, hFm⟩ : (α → Prop) →o (α → Prop)).gfp s

Uses 3 · Used by 1

Statement usesGreatest fixed point of a finset map by finite iteration

Proof usesFinite iteration from the whole type reaches a fixed point · Finset and predicate iterations from the top agree

Used byCorrectness of the finite fixed-point computation of EG

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.