REACHd: deterministic reachability, complete for LOGSPACE

The problem REACHd – is some marked target reachable from some marked source along forced arcs? – over the same vocabulary FirstOrder.Language.stGraph as REACH. It is to DescriptiveComplexity.LOGSPACE what REACH is to DescriptiveComplexity.NL, and its two halves are the mirror image of that pair: membership because the problem is a deterministic walk, hardness because the graph of a deterministic walk is such a problem.

No promise, and why

The textbook statement of REACHd restricts the input to graphs of outdegree at most one. A promise problem is awkward here: it would either need a well-formedness conjunct (DescriptiveComplexity.DecisionProblem.ofSentence) carried through every reduction, or leave the yes-instances undefined on the graphs that break the promise – and isomorphism-invariance would then have to be proved of a partial specification.

So the outdegree bound is imposed semantically instead, by the same move determinization makes one level up (DescriptiveComplexity.TCSpec.det): the walk may follow an arc only when it is the only arc out of its source (DescriptiveComplexity.DetEdge). Every marked graph is then a legal instance, the problem is invariant by transport, and on graphs that do have outdegree at most one it is exactly REACH (DescriptiveComplexity.detReachable_iff_reachable) – which is what the hardness proof uses, the interpreted graph of a deterministic walk being functional by construction.

Completeness

• Membership (DescriptiveComplexity.reachd_dtcDefinable): REACHd is a single deterministic transitive closure, at arity one and with a single mode – the very specification DescriptiveComplexity.reachSpec that witnesses DescriptiveComplexity.reach_tcDefinable, read through its determinization. The determinized step relation is DescriptiveComplexity.DetEdge.
• The complement, UNREACHd, is complete as well (DescriptiveComplexity.UNREACHd_LOGSPACE_complete, in DescriptiveComplexity.Problems.ReachabilityDet.Complement), which is how L = coL is obtained.
• Hardness (DescriptiveComplexity.reachd_hard_of_dtcDefinable): the interpretation is the graph of the walk itself (DescriptiveComplexity.TCDischarge.tcInterp), reused verbatim from the FO(TC) discharge; all that is new is that the walk of a determinized specification is functional, so that reachability in the interpreted graph and deterministic reachability agree.

The problem

def DescriptiveComplexity.DetEdge {A : Type} [FirstOrder.Language.stGraph.Structure A] (a b : A) : Prop

A forced arc: an arc that is the only one out of its source. Following these is the deterministic walk on a marked graph, with no promise on the instance.

Equations

• DescriptiveComplexity.DetEdge a b = (DescriptiveComplexity.SGEdge a b ∧ ∀ (c : A), DescriptiveComplexity.SGEdge a c → c = b)

def DescriptiveComplexity.DetReachable (A : Type) [FirstOrder.Language.stGraph.Structure A] : Prop

Some marked target is reachable from some marked source along a (possibly empty) path of forced arcs.

Equations

• DescriptiveComplexity.DetReachable A = ∃ (s : A) (t : A), DescriptiveComplexity.SGSource s ∧ DescriptiveComplexity.SGTarget t ∧ Relation.ReflTransGen DescriptiveComplexity.DetEdge s t

theorem DescriptiveComplexity.detReachable_iff_reachable {A : Type} [FirstOrder.Language.stGraph.Structure A] (h : ∀ (a b c : A), SGEdge a b → SGEdge a c → b = c) : DetReachable A ↔ Reachable A

On a graph of outdegree at most one, deterministic reachability is reachability: every arc is forced.

theorem DescriptiveComplexity.detReachable_iso {A B : Type} [FirstOrder.Language.stGraph.Structure A] [FirstOrder.Language.stGraph.Structure B] (e : FirstOrder.Language.stGraph.Equiv A B) : DetReachable A ↔ DetReachable B

Deterministic reachability is isomorphism-invariant.

def DescriptiveComplexity.REACHd : DecisionProblem FirstOrder.Language.stGraph

REACHd, deterministic reachability: is a marked target reachable from a marked source along forced arcs?

Equations

• DescriptiveComplexity.REACHd = { Holds := fun (A : Type) (inst : FirstOrder.Language.stGraph.Structure A) => DescriptiveComplexity.DetReachable A, iso_invariant := ⋯ }

Membership: REACHd is a deterministic transitive closure

theorem DescriptiveComplexity.det_step_reachSpec {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] (a b : reachSpec.Node A) : reachSpec.det.Step a b ↔ DetEdge (a.2 0) (b.2 0)

The determinized walk of DescriptiveComplexity.reachSpec follows exactly the forced arcs. The uniqueness clause quantifies over successor nodes, which at a single mode and arity one are just the successor vertices.

theorem DescriptiveComplexity.detReach_of_reflTransGen {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {x y : A} (h : Relation.ReflTransGen DetEdge x y) : reachSpec.det.Reach ((), fun (x_1 : Fin reachSpec.det.k) => x) ((), fun (x : Fin reachSpec.det.k) => y)

A path of forced arcs is a walk of the determinized specification.

theorem DescriptiveComplexity.reflTransGen_of_detReach {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {u v : reachSpec.Node A} (h : reachSpec.det.Reach u v) : Relation.ReflTransGen DetEdge (u.2 0) (v.2 0)

A walk of the determinized specification is a path of forced arcs.

theorem DescriptiveComplexity.det_accepts_reachSpec_iff (A : Type) [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] : reachSpec.det.Accepts A ↔ DetReachable A

The determinized specification accepts exactly the graphs with a forced path from a marked source to a marked target.

theorem DescriptiveComplexity.reachd_dtcDefinable : DTCDefinable REACHd

REACHd is FO(DTC) definable: it is a single deterministic transitive closure of the edge relation, at arity one – the specification of REACH read through its determinization.

theorem DescriptiveComplexity.reachd_mem_LOGSPACE : LOGSPACE.Mem REACHd

REACHd is in LOGSPACE.

Hardness: the graph of a deterministic walk

theorem DescriptiveComplexity.TCSpec.pad_functional {L : FirstOrder.Language} {spec : TCSpec L} {A : Type} [L.Structure A] [LinearOrder A] (h : spec.Functional A) : spec.pad.Functional A

Padding a specification with a spare mode preserves functionality: the spare mode has no transitions at all.

theorem DescriptiveComplexity.functional_sgEdge_tcInterp {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (h : spec.Functional A) (a b c : (TCDischarge.tcInterp spec).Map A) (hb : SGEdge a b) (hc : SGEdge a c) : b = c

The graph interpreted from a functional specification has outdegree at most one: its arcs are the transitions of the walk.

theorem DescriptiveComplexity.detReachable_tcInterp_iff {L : FirstOrder.Language} (spec : TCSpec L) (A : Type) [L.Structure A] [LinearOrder A] (h : spec.Functional A) : DetReachable ((TCDischarge.tcInterp spec).Map A) ↔ spec.Accepts A

Correctness of the deterministic discharge: in the graph of a functional walk, deterministic reachability is reachability, hence acceptance.

noncomputable def DescriptiveComplexity.dtcReduction {L : FirstOrder.Language} (spec : TCSpec L) (P : DecisionProblem L) (hP : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], P.Holds A ↔ spec.det.Accepts A) : OrderedFOReduction P REACHd

The generic FO(DTC) reduction: an ordered first-order reduction to REACHd from any problem defined, on nonempty finite ordered structures, by a single deterministic transitive closure. The interpretation is the graph of the determinized walk – functional by construction, which is exactly the condition under which the target problem's forced arcs are all of its arcs.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.reachd_hard_of_dtcDefinable {L : FirstOrder.Language} (P : DecisionProblem L) (hP : DTCDefinable P) : Nonempty (OrderedFOReduction P REACHd)

LOGSPACE-hardness of REACHd, machine-free: every FO(DTC) definable problem admits an ordered first-order reduction to REACHd.

theorem DescriptiveComplexity.reachd_LOGSPACE_hard : LOGSPACE.Hard REACHd

REACHd is LOGSPACE-hard: the FO(DTC) discharge, whose interpretation is the graph of the deterministic walk itself.

theorem DescriptiveComplexity.REACHd_LOGSPACE_complete : LOGSPACE.Complete REACHd

REACHd is LOGSPACE-complete. Both halves are the same observation read in opposite directions: deterministic reachability is a deterministic transitive closure (membership), and a deterministic transitive closure is deterministic reachability in the graph of its walk (hardness). Compare REACH, whose NL-completeness needs Immerman–Szelepcsényi on the membership side; here nothing of the kind is required, the fragment issue that forces it not arising for an operator-based logic.