UNREACHd, and L = coL

Deterministic logarithmic space is closed under complement (DescriptiveComplexity.LOGSPACE_eq_coLOGSPACE), and UNREACHd – non-reachability along forced arcs – is LOGSPACE-complete (DescriptiveComplexity.UNREACHd_LOGSPACE_complete).

Unlike NL = coNL this needs no inductive counting, and unlike the clausal fragments FO(DTC) has no built-in asymmetry between a problem and its complement: everything reduces to one membership statement, DescriptiveComplexity.unreachd_dtcDefinable. Given it, the complement of any FO(DTC) definable problem is FO(DTC) definable, because a reduction complements along with the problem (DescriptiveComplexity.OrderedFOReduction.compl) and REACHd is LOGSPACE-hard.

Complementing a deterministic walk

REACHdᶜ says that no marked source has a marked target ahead of it. Three things make that a deterministic walk:

• The walk is functional, so from a given vertex there is only one thing to do: follow the forced arc (DescriptiveComplexity.detNext, the successor map, a dead end being its own successor). Reachability along forced arcs is exactly iteration of that map (DescriptiveComplexity.reflTransGen_detEdge_iff_iterate).
• A step budget replaces cycle detection. A walk that has not arrived after |A| - 1 steps never will: taking a minimal number of steps to a vertex makes the visited vertices distinct, so it is bounded by the size of the universe (DescriptiveComplexity.exists_iterate_lt_card). The budget is carried as a third coordinate holding a vertex, counted through DescriptiveComplexity.orank – the universe has exactly as many elements as the walk may take steps.
• The sources are scanned in order. Acceptance quantifies the start node existentially, while the complement must quantify sources universally, so the walk loops over the candidates itself, in the order of the structure, and accepts only after exhausting them.

A node is therefore a mode – scanning or done – with a triple (s, x, c): the source candidate, the current position, the budget. The walk gets stuck exactly when it finds a marked target ahead of a marked source, so it reaches its accepting node exactly when there is nothing to find.

The forced-arc successor map

def DescriptiveComplexity.Stuck {A : Type} [FirstOrder.Language.stGraph.Structure A] (x : A) : Prop

A vertex is stuck when no arc out of it is forced: either it has no outgoing arc at all, or it has several.

Equations

• DescriptiveComplexity.Stuck x = ¬∃ (y : A), DescriptiveComplexity.DetEdge x y

noncomputable def DescriptiveComplexity.detNext {A : Type} [FirstOrder.Language.stGraph.Structure A] (x : A) : A

The successor map of the deterministic walk: the endpoint of the forced arc out of x, and x itself where the walk is stuck – the walk of the forced arcs read as an iterated function, DescriptiveComplexity.stepNext. Making it total is what lets reachability be read as iteration.

Equations

• DescriptiveComplexity.detNext x = DescriptiveComplexity.stepNext DescriptiveComplexity.DetEdge x

theorem DescriptiveComplexity.reflTransGen_detEdge_iff_iterate {A : Type} [FirstOrder.Language.stGraph.Structure A] (s t : A) : Relation.ReflTransGen DetEdge s t ↔ ∃ (n : ℕ), detNext^[n] s = t

Reachability along forced arcs is iteration of the successor map.

The scanning walk

A node is a mode – false while scanning, true once done – together with a triple (s, x, c): the source candidate being tested, the current position of the walk, and the budget, itself a vertex, counted by its rank in the order.

noncomputable def DescriptiveComplexity.UnreachD.srcF {γ : Type} (u : γ) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula γ

u is a marked source, as a formula.

Equations

• DescriptiveComplexity.UnreachD.srcF u = FirstOrder.Language.sgSourceO.formula₁ (FirstOrder.Language.var u)

noncomputable def DescriptiveComplexity.UnreachD.tgtF {γ : Type} (u : γ) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula γ

u is a marked target, as a formula.

Equations

• DescriptiveComplexity.UnreachD.tgtF u = FirstOrder.Language.sgTargetO.formula₁ (FirstOrder.Language.var u)

noncomputable def DescriptiveComplexity.UnreachD.edgeF {γ : Type} (u v : γ) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula γ

There is an arc from u to v, as a formula.

Equations

• DescriptiveComplexity.UnreachD.edgeF u v = FirstOrder.Language.sgEdgeO.formula₂ (FirstOrder.Language.var u) (FirstOrder.Language.var v)

noncomputable def DescriptiveComplexity.UnreachD.detEdgeF {γ : Type} (u v : γ) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula γ

The arc from u to v is forced, as a formula: it is an arc, and it is the only one out of u.

Equations

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

noncomputable def DescriptiveComplexity.UnreachD.stuckF {γ : Type} (u : γ) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula γ

No arc out of u is forced, as a formula.

Equations

• DescriptiveComplexity.UnreachD.stuckF u = FirstOrder.Language.Formula.iAlls (Fin 1) (FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.UnreachD.detEdgeF (Sum.inl u) (Sum.inr 0)))

def DescriptiveComplexity.UnreachD.eqF {γ : Type} (u v : γ) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula γ

Equality of two variables, as a formula.

Equations

• DescriptiveComplexity.UnreachD.eqF u v = (FirstOrder.Language.var u).equal (FirstOrder.Language.var v)

@[simp]

theorem DescriptiveComplexity.UnreachD.realize_srcF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (u : γ) : (srcF u).Realize v ↔ SGSource (v u)

@[simp]

theorem DescriptiveComplexity.UnreachD.realize_tgtF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (u : γ) : (tgtF u).Realize v ↔ SGTarget (v u)

@[simp]

theorem DescriptiveComplexity.UnreachD.realize_edgeF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (u w : γ) : (edgeF u w).Realize v ↔ SGEdge (v u) (v w)

@[simp]

theorem DescriptiveComplexity.UnreachD.realize_eqF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (u w : γ) : (eqF u w).Realize v ↔ v u = v w

@[simp]

theorem DescriptiveComplexity.UnreachD.realize_detEdgeF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (u w : γ) : (detEdgeF u w).Realize v ↔ DetEdge (v u) (v w)

@[simp]

theorem DescriptiveComplexity.UnreachD.realize_stuckF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (u : γ) : (stuckF u).Realize v ↔ Stuck (v u)

The specification

@[reducible, inline]

abbrev DescriptiveComplexity.UnreachD.vS : Fin 3 ⊕ Fin 3

The current source candidate.

Equations

• DescriptiveComplexity.UnreachD.vS = Sum.inl 0

@[reducible, inline]

abbrev DescriptiveComplexity.UnreachD.vX : Fin 3 ⊕ Fin 3

The current position of the walk.

Equations

• DescriptiveComplexity.UnreachD.vX = Sum.inl 1

@[reducible, inline]

abbrev DescriptiveComplexity.UnreachD.vC : Fin 3 ⊕ Fin 3

The current budget.

Equations

• DescriptiveComplexity.UnreachD.vC = Sum.inl 2

@[reducible, inline]

abbrev DescriptiveComplexity.UnreachD.vS' : Fin 3 ⊕ Fin 3

The next source candidate.

Equations

• DescriptiveComplexity.UnreachD.vS' = Sum.inr 0

@[reducible, inline]

abbrev DescriptiveComplexity.UnreachD.vX' : Fin 3 ⊕ Fin 3

The next position.

Equations

• DescriptiveComplexity.UnreachD.vX' = Sum.inr 1

@[reducible, inline]

abbrev DescriptiveComplexity.UnreachD.vC' : Fin 3 ⊕ Fin 3

The next budget.

Equations

• DescriptiveComplexity.UnreachD.vC' = Sum.inr 2

noncomputable def DescriptiveComplexity.UnreachD.stepFF : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula (Fin 3 ⊕ Fin 3)

The transition of the scanning mode to itself: either follow the forced arc and spend one unit of budget, or – when the walk is stuck or the budget is exhausted – move on to the next source candidate. Both are guarded by the absence of a marked target ahead of a marked source, which is where the walk stops for good.

Equations

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

noncomputable def DescriptiveComplexity.UnreachD.stepFT : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula (Fin 3 ⊕ Fin 3)

The transition to the accepting mode: the last candidate has been scanned through.

Equations

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

noncomputable def DescriptiveComplexity.UnreachD.srcFml : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula (Fin 3)

The starting nodes: the least candidate, the walk at that candidate, the full budget.

Equations

• DescriptiveComplexity.UnreachD.srcFml = DescriptiveComplexity.minF 0 ⊓ DescriptiveComplexity.UnreachD.eqF 1 0 ⊓ DescriptiveComplexity.minF 2

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.UnreachD.unreachdSpec : TCSpec FirstOrder.Language.stGraph

The specification whose deterministic walk scans for a forced path from a marked source to a marked target, accepting when it finds none.

Equations

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

Semantics of the walk

def DescriptiveComplexity.UnreachD.IsMinA {A : Type} [LinearOrder A] (a : A) : Prop

a is a least element of the order.

Equations

• DescriptiveComplexity.UnreachD.IsMinA a = ∀ (b : A), a ≤ b

Order arithmetic for the budget

theorem DescriptiveComplexity.UnreachD.orank_of_isMinA {A : Type} [LinearOrder A] {a : A} (h : IsMinA a) : orank a = 0

Determinism of the scanning walk

theorem DescriptiveComplexity.UnreachD.node_ext {A : Type} {b c : Bool × (Fin 3 → A)} (h0 : b.1 = c.1) (h1 : b.2 0 = c.2 0) (h2 : b.2 1 = c.2 1) (h3 : b.2 2 = c.2 2) : b = c

Correctness of the scan

def DescriptiveComplexity.UnreachD.Bad {A : Type} [FirstOrder.Language.stGraph.Structure A] (s : A) : Prop

A marked source with a marked target ahead of it: what the scan looks for, and what its acceptance denies.

Equations

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

theorem DescriptiveComplexity.UnreachD.detReachable_iff_exists_bad {A : Type} [FirstOrder.Language.stGraph.Structure A] : DetReachable A ↔ ∃ (s : A), Bad s

theorem DescriptiveComplexity.UnreachD.iterate_of_stuck {A : Type} [FirstOrder.Language.stGraph.Structure A] {x : A} (h : Stuck x) (n : ℕ) : detNext^[n] x = x

Completeness of the scan

Nothing to find means nothing stops the walk, so it runs the inner loop to its end for every candidate and finishes.

UNREACHd, and the closure of LOGSPACE under complement

theorem DescriptiveComplexity.unreachd_dtcDefinable : DTCDefinable REACHdᶜ

The complement of REACHd is FO(DTC) definable: the scan is deterministic (DescriptiveComplexity.UnreachD.functional_unreachdSpec), so its determinization is itself, and it accepts exactly the marked graphs in which no marked target lies ahead of a marked source.

theorem DescriptiveComplexity.mem_LOGSPACE_compl_iff {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : LOGSPACE.Mem Pᶜ ↔ LOGSPACE.Mem P

Membership in LOGSPACE is closed under complement.

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.coLOGSPACE : ComplexityClass

coLOGSPACE, the complement class of LOGSPACE. That it is LOGSPACE is DescriptiveComplexity.LOGSPACE_eq_coLOGSPACE.

Equations

• DescriptiveComplexity.coLOGSPACE = DescriptiveComplexity.LOGSPACE.compl

theorem DescriptiveComplexity.LOGSPACE_eq_coLOGSPACE : LOGSPACE = coLOGSPACE

L = coL: deterministic logarithmic space is closed under complement. Unlike NL = coNL (DescriptiveComplexity.NL_eq_coNL, Immerman–Szelepcsényi) this needs no inductive counting: a deterministic walk has only one thing to do at each node, so not arriving is witnessed by walking until the budget runs out. Registered in the Lax archive as Lax485149.LEqCoL.LOGSPACE_eq_coLOGSPACE.

def DescriptiveComplexity.UNREACHd : DecisionProblem FirstOrder.Language.stGraph

UNREACHd, the complement of REACHd: no marked target is reachable from a marked source along forced arcs.

Equations

• DescriptiveComplexity.UNREACHd = DescriptiveComplexity.REACHdᶜ

theorem DescriptiveComplexity.unreachd_mem_LOGSPACE : LOGSPACE.Mem UNREACHd

UNREACHd is in LOGSPACE, by the scan.

theorem DescriptiveComplexity.unreachd_LOGSPACE_hard : LOGSPACE.Hard UNREACHd

UNREACHd is LOGSPACE-hard, by complementing the discharge: the complement of a problem of the class is again in the class, it reduces to REACHd, and the very same interpretation reduces the problem itself to UNREACHd.

theorem DescriptiveComplexity.UNREACHd_LOGSPACE_complete : LOGSPACE.Complete UNREACHd

UNREACHd is LOGSPACE-complete. Both halves come from the same side here, unlike the REACH/UNREACH pair one level up: an operator-based logic defines a problem and its complement alike, so no analogue of Immerman–Szelepcsényi is needed to complete the picture. Registered in the Lax archive as Lax485149.UnreachdLComplete.unreachd_LOGSPACE_complete.