Deterministic reachability in directed graphs

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

definition

Loading review…

Sign in with ORCID

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

    In a directed graph with marked sources and targets, an edge (a,b)(a, b) is forced when it is the only edge leaving aa. An instance is a yes-instance of REACHd when some marked target is reachable from some marked source by a possibly empty path of forced edges; no promise is made on the instance, whose vertices may have any outdegree. REACHd is the decision problem of the structures isomorphic to such an instance, and UNREACHd is its complement.

    Concept map
    5 concepts; 21 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
    6import Lax485149.Reachability
    7
    8/-!
    9---
    10title: Deterministic reachability in directed graphs
    11type: definition
    12---
    13In a directed graph with marked sources and targets, an edge (a,b)(a, b) is
    14forced when it is the only edge leaving aa. An instance is a yes-instance
    15of REACHd when some marked target is reachable from some marked source by a
    16possibly empty path of forced edges; no promise is made on the instance,
    17whose vertices may have any outdegree. REACHd is the decision problem of the
    18structures isomorphic to such an instance, and UNREACHd is its complement.
    19-/
    20
    21namespace Lax485149.DeterministicReachability
    22
    23open FirstOrder FirstOrder.Language FirstOrder.Language.Structure
    24open Lax904597.Problems Lax485149.Problems Lax485149.Complement Lax485149.Reachability
    25
    26/-- A *forced* arc: an arc that is the only one out of its source. Following
    27these is the deterministic walk on a marked graph, with no promise on the
    28instance. -/
    29def DetEdge {A : Type} [stGraph.Structure A] (a b : A) : Prop :=
    30 SGEdge a b ∧ ∀ c : A, SGEdge a c → c = b
    31
    32/-- Some marked target is reachable from some marked source along a (possibly
    33empty) path of forced arcs. -/
    34def DetReachable (A : Type) [stGraph.Structure A] : Prop :=
    35 ∃ s t : A, SGSource s ∧ SGTarget t ∧ Relation.ReflTransGen DetEdge s t
    36
    37/-- REACHd, deterministic reachability: is a marked target reachable from a
    38marked source along forced arcs? -/
    39def REACHd : DecisionProblem stGraph := DecisionProblem.ofPred fun A _ => DetReachable A
    40
    41/-- UNREACHd, the complement of REACHd. -/
    42def UNREACHd : DecisionProblem stGraph := DecisionProblem.compl REACHd
    43
    44end Lax485149.DeterministicReachability
    45

    Discussion

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

    Loading discussion…