Transitive closure of finite relations

DefinitionSuccessors of a finite set#✓fully proved

Let \(\alpha\) be a finite type and let \(r\) be a decidable relation on \(\alpha\). For a finite set \(Z \subseteq \alpha\), the set of \(r\)-successors of \(Z\) is the finite set \(\mathrm{post}_r(Z) = \{t \in \alpha \mid r(z, t) \text{ for some } z \in Z\}\).

def postFin (Z : Finset α) : Finset α :=
  Finset.univ.filter fun t => ∃ z ∈ Z, r z t

Used by 2

Used byMembership in the set reachable from finitely many sources · One step of the reachability iteration

DefinitionOne step of the reachability iteration#✓fully proved

Let \(\alpha\) be a finite type with decidable equality, let \(r\) be a decidable relation on \(\alpha\), and write \(\mathrm{post}_r(Z)\) for the set of \(r\)-successors of elements of a finite set \(Z \subseteq \alpha\). For a finite set \(A \subseteq \alpha\), the step map sends a finite set \(Z \subseteq \alpha\) to \(\mathrm{post}_r(A) \cup \mathrm{post}_r(Z)\).

Its least fixed point is the set of elements reachable from \(A\) in one or more \(r\)-steps.

def transGenStep (A Z : Finset α) : Finset α :=
  postFin r A ∪ postFin r Z

Uses 1 · Used by 2

Statement usesSuccessors of a finite set

Used byMembership in the set reachable from finitely many sources · Elements reachable from a finite set of sources

DefinitionElements reachable from a finite set of sources#✓fully proved

Let \(\alpha\) be a finite type with decidable equality, let \(r\) be a decidable relation on \(\alpha\), and let \(A \subseteq \alpha\) be a finite set. Write \(\mathrm{post}_r(Z)\) for the set of \(r\)-successors of elements of a finite set \(Z \subseteq \alpha\), and let \(f\) be the step map \(f(Z) = \mathrm{post}_r(A) \cup \mathrm{post}_r(Z)\). The finite set of elements reachable from \(A\) is \(f^{|\alpha|}(\emptyset)\), obtained by applying \(f\) to the empty set \(|\alpha|\) times, where \(|\alpha|\) is the number of elements of \(\alpha\).

Since \(f\) is monotone, this is the least fixed point of \(f\); it consists of the elements reachable from some element of \(A\) in one or more \(r\)-steps.

def transGenFinFrom (A : Finset α) : Finset α :=
  Finset.lfpFin (transGenStep r A)

Uses 2 · Used by 5

Statement usesLeast fixed point of a finset map by finite iteration · One step of the reachability iteration

Used byMembership in the set reachable from a point · Membership in the set reachable from finitely many sources · Elements reachable from a point · Lasso detection by finite reachability · Lasso states of a finite Büchi automaton

DefinitionElements reachable from a point#✓fully proved

Let \(\alpha\) be a finite type with decidable equality, let \(r\) be a decidable relation on \(\alpha\), and let \(a \in \alpha\). The finite set of elements reachable from \(a\) is the finite set of elements reachable from the source set \(\{a\}\), that is, the elements reachable from \(a\) in one or more \(r\)-steps.

def transGenFin (a : α) : Finset α :=
  transGenFinFrom r {a}

Uses 1 · Used by 4

Statement usesElements reachable from a finite set of sources

Used byDecidability of the transitive closure on a finite type · Membership in the set reachable from a point · Lasso detection by finite reachability · Lasso states of a finite Büchi automaton

TheoremMembership in the set reachable from finitely many sources#✓fully proved

Let \(\alpha\) be a finite type with decidable equality, let \(r\) be a decidable relation on \(\alpha\), and let \(A \subseteq \alpha\) be a finite set. An element \(t \in \alpha\) lies in the finite set of elements reachable from \(A\) in one or more \(r\)-steps (computed as a finite least fixed point) if and only if there is some \(a \in A\) such that \((a, t)\) lies in the transitive closure of \(r\).

theorem mem_transGenFinFrom {A : Finset α} {t : α} :
    t ∈ transGenFinFrom r A ↔ ∃ a ∈ A, TransGen r a t

Uses 6 · Used by 2

Statement usesElements reachable from a finite set of sources

Proof usesLeast fixed point of a finset map by finite iteration · Finite iteration from the empty set reaches a fixed point · The finite least fixed point lies in every pre-fixed point · Successors of a finite set · One step of the reachability iteration

Used byMembership in the set reachable from a point · Lasso detection by finite reachability

TheoremMembership in the set reachable from a point#✓fully proved

Let \(\alpha\) be a finite type with decidable equality, let \(r\) be a decidable relation on \(\alpha\), and let \(a \in \alpha\). An element \(t \in \alpha\) lies in the finite set of elements reachable from \(a\) in one or more \(r\)-steps (computed as a finite least fixed point) if and only if \((a, t)\) lies in the transitive closure of \(r\).

theorem mem_transGenFin {a t : α} : t ∈ transGenFin r a ↔ TransGen r a t

Uses 3 · Used by 2

Statement usesElements reachable from a point

Proof usesMembership in the set reachable from finitely many sources · Elements reachable from a finite set of sources

Used byDecidability of the transitive closure on a finite type · Lasso detection by finite reachability

DefinitionDecidability of the transitive closure on a finite type#✓fully proved

Let \(\alpha\) be a finite type with decidable equality and let \(r\) be a decidable relation on \(\alpha\). Then the transitive closure of \(r\) is decidable: for all \(a, t \in \alpha\) it is decidable whether \(t\) is reachable from \(a\) in one or more \(r\)-steps.

The decision is membership of \(t\) in the finite set of elements reachable from \(a\).

@[instance_reducible]
def decidableTransGen : DecidableRel (TransGen r) := fun a t =>
  decidable_of_iff (t ∈ transGenFin r a) mem_transGenFin

Uses 2 · Used by 1

Statement usesMembership in the set reachable from a point · Elements reachable from a point

Used byDecidability of the reflexive-transitive closure on a finite type

DefinitionDecidability of the reflexive-transitive closure on a finite type#✓fully proved

Let \(\alpha\) be a finite type with decidable equality and let \(r\) be a decidable relation on \(\alpha\). Then the reflexive-transitive closure of \(r\) is decidable: for all \(a, t \in \alpha\) it is decidable whether \(t\) is reachable from \(a\) in zero or more \(r\)-steps.

@[instance_reducible]
def decidableReflTransGen : DecidableRel (ReflTransGen r) := fun a t =>
  haveI := decidableTransGen r
  decidable_of_iff (t = a ∨ TransGen r a t) reflTransGen_iff_eq_or_transGen.symm

Uses 1

Statement usesDecidability of the transitive closure on a finite type

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.