Lax Lean Archive

Reachability and unreachability in directed graphs

Lax485149.Reachability · concepts/Lax485149/Reachability.lean · lax-485149

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    An instance is a directed graph with marked source vertices and marked target vertices: a structure over the vocabulary with a binary relation of edges and two unary relations of sources and targets. It is a yes-instance of REACH when some marked target is reachable from some marked source by a directed path, possibly empty; REACH is the decision problem of the structures isomorphic to such an instance. UNREACH is the complement of REACH: no marked target is reachable from a marked source.

    Concept map
    4 concepts; 22 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.ModelTheory.Semantics
    2import Mathlib.Logic.Relation
    3import Lax904597.Problems
    4import Lax485149.Problems
    5import Lax485149.Complement
    6
    7/-!
    8---
    9title: Reachability and unreachability in directed graphs
    10type: definition
    11---
    12An instance is a directed graph with marked source vertices and marked target
    13vertices: a structure over the vocabulary with a binary relation of edges
    14and two unary relations of sources and targets. It is a yes-instance of
    15REACH when some marked target is reachable from some marked source by a
    16directed path, possibly empty; REACH is the decision problem of the
    17structures isomorphic to such an instance. UNREACH is the complement of
    18REACH: no marked target is reachable from a marked source.
    19-/
    20
    21namespace Lax485149.Reachability
    22
    23open FirstOrder FirstOrder.Language FirstOrder.Language.Structure
    24open Lax904597.Problems Lax485149.Problems Lax485149.Complement
    25
    26/-- The relation symbols of graphs with marked sources and targets. -/
    27inductive stGraphRel : ℕ → Type where
    28 /-- `edge a b`: there is an edge from `a` to `b`. -/
    29 | edge : stGraphRel 2
    30 /-- `source a`: the vertex `a` is a marked source. -/
    31 | source : stGraphRel 1
    32 /-- `target a`: the vertex `a` is a marked target. -/
    33 | target : stGraphRel 1
    34 deriving DecidableEq
    35
    36/-- The relational vocabulary of directed graphs with marked sources and
    37targets. -/
    38def stGraph : Language :=
    39 ⟨fun _ => Empty, stGraphRel⟩
    40
    41instance instIsRelationalStGraph : IsRelational stGraph := fun _ =>
    42 (inferInstance : IsEmpty Empty)
    43
    44/-- `edge a b`: there is an edge from `a` to `b`. -/
    45abbrev sgEdge : stGraph.Relations 2 := .edge
    46
    47/-- `source a`: the vertex `a` is a marked source. -/
    48abbrev sgSource : stGraph.Relations 1 := .source
    49
    50/-- `target a`: the vertex `a` is a marked target. -/
    51abbrev sgTarget : stGraph.Relations 1 := .target
    52
    53/-- `edge a b`: there is an edge from `a` to `b`. -/
    54def SGEdge {A : Type} [stGraph.Structure A] (a0 : A) (a1 : A) : Prop :=
    55 RelMap sgEdge ![a0, a1]
    56
    57/-- `source a`: the vertex `a` is a marked source. -/
    58def SGSource {A : Type} [stGraph.Structure A] (a0 : A) : Prop :=
    59 RelMap sgSource ![a0]
    60
    61/-- `target a`: the vertex `a` is a marked target. -/
    62def SGTarget {A : Type} [stGraph.Structure A] (a0 : A) : Prop :=
    63 RelMap sgTarget ![a0]
    64
    65/-- Some marked target is reachable from some marked source, along a
    66(possibly empty) directed path. -/
    67def Reachable (A : Type) [stGraph.Structure A] : Prop :=
    68 ∃ s t : A, SGSource s ∧ SGTarget t ∧ Relation.ReflTransGen SGEdge s t
    69
    70/-- REACH: is some marked target reachable from some marked source? -/
    71def REACH : DecisionProblem stGraph := DecisionProblem.ofPred fun A _ => Reachable A
    72
    73/-- UNREACH, the complement of REACH: no marked target is reachable from a
    74marked source. -/
    75def UNREACH : DecisionProblem stGraph := DecisionProblem.compl REACH
    76
    77end Lax485149.Reachability
    78
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…