Deterministic reachability in directed graphs
Lax485149.DeterministicReachability · concepts/Lax485149/DeterministicReachability.lean · lax-485149
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
In a directed graph with marked sources and targets, an edge is forced when it is the only edge leaving . 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
Lean source view on GitHub
| 1 | import Mathlib.ModelTheory.Semantics |
| 2 | import Mathlib.Logic.Relation |
| 3 | import Lax904597.Problems |
| 4 | import Lax485149.Problems |
| 5 | import Lax485149.Complement |
| 6 | import Lax485149.Reachability |
| 7 | |
| 8 | /-! |
| 9 | --- |
| 10 | title: Deterministic reachability in directed graphs |
| 11 | type: definition |
| 12 | --- |
| 13 | In a directed graph with marked sources and targets, an edge is |
| 14 | forced when it is the only edge leaving . An instance is a yes-instance |
| 15 | of REACHd when some marked target is reachable from some marked source by a |
| 16 | possibly empty path of forced edges; no promise is made on the instance, |
| 17 | whose vertices may have any outdegree. REACHd is the decision problem of the |
| 18 | structures isomorphic to such an instance, and UNREACHd is its complement. |
| 19 | -/ |
| 20 | |
| 21 | namespace Lax485149.DeterministicReachability |
| 22 | |
| 23 | open FirstOrder FirstOrder.Language FirstOrder.Language.Structure |
| 24 | open 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 |
| 27 | these is the deterministic walk on a marked graph, with no promise on the |
| 28 | instance. -/ |
| 29 | def 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 |
| 33 | empty) path of forced arcs. -/ |
| 34 | def 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 |
| 38 | marked source along forced arcs? -/ |
| 39 | def REACHd : DecisionProblem stGraph := DecisionProblem.ofPred fun A _ => DetReachable A |
| 40 | |
| 41 | /-- UNREACHd, the complement of REACHd. -/ |
| 42 | def UNREACHd : DecisionProblem stGraph := DecisionProblem.compl REACHd |
| 43 | |
| 44 | end Lax485149.DeterministicReachability |
| 45 |
Used by
Lax485149.DeterministicReachabilityInvarianceLax485149.FirstOrderInTransitiveClosureLax485149.ImmermanSzelepcsenyiLax485149.KromAndTransitiveClosureLax485149.LByAutomataLax485149.LClosureLax485149.LEqCoLLax485149.LSubsetNLLax485149.NLByAutomataLax485149.NLClosureLax485149.NLEqCoNLLax485149.NLIsTransitiveClosureLax485149.NLSubsetNPLax485149.ReachabilityInvarianceLax485149.ReachdLCompleteLax485149.ReachNLCompleteLax485149.TransitiveClosureClosureLax485149.TwoSatInvarianceLax485149.TwoSatNLCompleteLax485149.UnreachdLCompleteLax485149.UnreachNLComplete
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments