REACH is NL-complete

The FO(TC) discharge: every DescriptiveComplexity.TCDefinable problem admits an ordered first-order reduction to DescriptiveComplexity.REACH (DescriptiveComplexity.reach_hard_of_tcDefinable). With REACH ∈ NL (DescriptiveComplexity.reach_mem_NL) and NL = FO(TC) (DescriptiveComplexity.tcDefinable_iff_mem_NL) this closes REACH's completeness for DescriptiveComplexity.NL (DescriptiveComplexity.REACH_NL_complete) – directed s-t reachability being the canonical NL-complete problem (Jones 1975; Immerman 1999, ch. 3).

The reduction is the walk itself

Where the discharges of the clausal fragments have to emit an instance – one propositional clause per clause of the program and per instantiation of its universally quantified variables – the discharge into REACH has nothing to build: the graph of the walk of a DescriptiveComplexity.TCSpec already is a marked graph, and reachability in it is what the specification accepts by definition.

The fit is exact, and it is the tags that make it so. A TCSpec walks on nodes that are a mode together with a k-tuple (DescriptiveComplexity.TCSpec.Node), which is literally the universe Tag × A^dim of a tagged interpretation (DescriptiveComplexity.FOInterpretation.Map) at Tag := spec.Mode and dim := spec.k. So the interpretation

   edge((m, x̄), (m', ȳ))  :=  step m m' (x̄, ȳ)
   source((m, x̄))         :=  src m x̄
   target((m, x̄))         :=  tgt m x̄

is nothing but the specification's three formulas, relabelled from their Fin k ⊕ Fin k (resp. Fin k) variables to the argument-major variables Fin n × Fin k an interpretation uses. There is no junk to gate away: every tagged tuple is a genuine node of the walk, so an ordinary (unrelativized) ordered reduction suffices.

One wrinkle: a reduction must map nonempty structures to nonempty structures, so its tag type must be nonempty, while a TCSpec may perfectly well have no modes at all (and then accept nothing). DescriptiveComplexity.TCSpec.pad, already at hand from the complementation proof, adds one spare isolated mode and changes no acceptance, which is exactly the fix.

What this does not claim

As everywhere in this library, no machine model is involved: NL is defined by the Krom fragment (DescriptiveComplexity.SigmaSOKromDefinable), and the NL-hardness proved here is hardness for that class. Grädel's capture theorem against logarithmic-space machines (Grädel 1992) is not formalized. Note also how much of the library this one-page reduction rests on: REACH ∈ NL is Immerman–Szelepcsényi, and the passage from an SO-Krom definition to an FO(TC) one is the translation of DescriptiveComplexity.KromTransitiveClosure.

The interpretation

The variables of a DescriptiveComplexity.TCSpec formula are one or two k-tuples; those of an interpretation's defining formula are indexed by argument-then-coordinate. The two selectors below are the renamings between them.

def DescriptiveComplexity.TCDischarge.stepVar {L : FirstOrder.Language} (spec : TCSpec L) : Fin spec.k ⊕ Fin spec.k → Fin 2 × Fin spec.k

The renaming of the transition formula's variables: the current tuple is the first argument of edge, the next one is its second argument.

Equations

• DescriptiveComplexity.TCDischarge.stepVar spec = Sum.elim (fun (i : Fin spec.k) => (0, i)) fun (i : Fin spec.k) => (1, i)

def DescriptiveComplexity.TCDischarge.endVar {L : FirstOrder.Language} (spec : TCSpec L) : Fin spec.k → Fin 1 × Fin spec.k

The renaming of an endpoint formula's variables: the tuple is the only argument of source, resp. target.

Equations

• DescriptiveComplexity.TCDischarge.endVar spec i = (0, i)

noncomputable def DescriptiveComplexity.TCDischarge.edgeF {L : FirstOrder.Language} (spec : TCSpec L) (m m' : spec.Mode) : (L.sum FirstOrder.Language.order).Formula (Fin 2 × Fin spec.k)

The defining formula of edge at a pair of modes: the transition formula of those modes.

Equations

• DescriptiveComplexity.TCDischarge.edgeF spec m m' = FirstOrder.Language.Formula.relabel (DescriptiveComplexity.TCDischarge.stepVar spec) (spec.step m m')

noncomputable def DescriptiveComplexity.TCDischarge.srcF {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin spec.k)

The defining formula of source at a mode: the source formula of that mode.

Equations

• DescriptiveComplexity.TCDischarge.srcF spec m = FirstOrder.Language.Formula.relabel (DescriptiveComplexity.TCDischarge.endVar spec) (spec.src m)

noncomputable def DescriptiveComplexity.TCDischarge.tgtF {L : FirstOrder.Language} (spec : TCSpec L) (m : spec.Mode) : (L.sum FirstOrder.Language.order).Formula (Fin 1 × Fin spec.k)

The defining formula of target at a mode: the target formula of that mode.

Equations

• DescriptiveComplexity.TCDischarge.tgtF spec m = FirstOrder.Language.Formula.relabel (DescriptiveComplexity.TCDischarge.endVar spec) (spec.tgt m)

noncomputable def DescriptiveComplexity.TCDischarge.tcInterp {L : FirstOrder.Language} (spec : TCSpec L) : FOInterpretation (L.sum FirstOrder.Language.order) FirstOrder.Language.stGraph spec.Mode spec.k

The graph of the walk, as an interpretation into the vocabulary of marked graphs: a vertex is a node of the specification – a mode together with a k-tuple – an arc is a transition, and the marks are the specification's starting and accepting nodes.

Equations

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

Correctness

theorem DescriptiveComplexity.TCDischarge.realize_edgeF {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (m m' : spec.Mode) (v : Fin 2 × Fin spec.k → A) : (edgeF spec m m').Realize v ↔ spec.Step (m, fun (i : Fin spec.k) => v (0, i)) (m', fun (i : Fin spec.k) => v (1, i))

theorem DescriptiveComplexity.TCDischarge.realize_srcF {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (m : spec.Mode) (v : Fin 1 × Fin spec.k → A) : (srcF spec m).Realize v ↔ spec.IsSrc (m, fun (i : Fin spec.k) => v (0, i))

theorem DescriptiveComplexity.TCDischarge.realize_tgtF {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (m : spec.Mode) (v : Fin 1 × Fin spec.k → A) : (tgtF spec m).Realize v ↔ spec.IsTgt (m, fun (i : Fin spec.k) => v (0, i))

theorem DescriptiveComplexity.TCDischarge.sgEdge_tcInterp {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (a b : (tcInterp spec).Map A) : SGEdge a b ↔ spec.Step a b

An arc of the interpreted graph is a transition of the walk.

theorem DescriptiveComplexity.TCDischarge.sgSource_tcInterp {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (a : (tcInterp spec).Map A) : SGSource a ↔ spec.IsSrc a

A marked source of the interpreted graph is a starting node of the walk.

theorem DescriptiveComplexity.TCDischarge.sgTarget_tcInterp {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (a : (tcInterp spec).Map A) : SGTarget a ↔ spec.IsTgt a

A marked target of the interpreted graph is an accepting node of the walk.

theorem DescriptiveComplexity.TCDischarge.reflTransGen_tcInterp {L : FirstOrder.Language} (spec : TCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (a b : (tcInterp spec).Map A) : Relation.ReflTransGen SGEdge a b ↔ spec.Reach a b

A directed path of the interpreted graph is a walk of the specification, and conversely.

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

Correctness of the discharge: a marked target of the interpreted graph is reachable from a marked source exactly when the specification accepts. Both directions are the identity on nodes – the graph is the walk.

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

The generic FO(TC) reduction: an ordered first-order reduction to REACH from any problem defined, on nonempty finite ordered structures, by a single transitive closure whose modes are nonempty.

Equations

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

NL-completeness

theorem DescriptiveComplexity.reach_hard_of_tcDefinable {L : FirstOrder.Language} (P : DecisionProblem L) (hP : TCDefinable P) : Nonempty (OrderedFOReduction P REACH)

NL-hardness of REACH, machine-free: every FO(TC) definable problem admits an ordered first-order reduction to REACH. The interpretation is the graph of the walk itself; padding the specification with one spare mode (DescriptiveComplexity.TCSpec.pad) is only there to keep the tag type nonempty, as a reduction requires.

theorem DescriptiveComplexity.reach_NL_hard : NL.Hard REACH

REACH is NL-hard: an SO-Krom definable problem is FO(TC) definable (DescriptiveComplexity.tcDefinable_iff_mem_NL, i.e. Immerman–Szelepcsényi through the two translations), and an FO(TC) definition reduces to reachability in the graph of its walk.

theorem DescriptiveComplexity.REACH_NL_complete : NL.Complete REACH

REACH is NL-complete. Membership is DescriptiveComplexity.reach_mem_NL – which is Immerman–Szelepcsényi, the Krom fragment defining non-reachability head-on; hardness is DescriptiveComplexity.reach_NL_hard, the FO(TC) discharge. Directed s-t reachability is the canonical NL-complete problem (Jones 1975), here complete under order-invariant first-order reductions rather than logarithmic-space ones.

theorem DescriptiveComplexity.unreach_NL_hard : NL.Hard UNREACH

UNREACH is NL-hard, by complementing the reduction: the complement of a problem in NL is in NL (DescriptiveComplexity.mem_NL_compl_iff), that complement reduces to REACH, and the very same interpretation reduces the problem itself to UNREACH (DescriptiveComplexity.OrderedFOReduction.compl, the correctness of a reduction being an equivalence).

theorem DescriptiveComplexity.UNREACH_NL_complete : NL.Complete UNREACH

UNREACH is NL-complete as well, and the two halves come from opposite sides. Membership is the head-on Krom program (DescriptiveComplexity.unreach_mem_NL): a clausal fragment states closure and rejection, so non-reachability is what it defines directly. Hardness is DescriptiveComplexity.unreach_NL_hard, which needs NL = coNL; without Immerman–Szelepcsényi neither half would be available for both problems, and the two would sit on either side of a complement that is not known to be crossable.