Documentation

Complexity.Computability.Complexity.Classes.LogSpace.USTCON

Undirected connectivity, symmetric logarithmic space, and SL = L #

Reingold's theorem Reingold, Theorem 4.1 Arora and Barak, Section 21.4: undirected s–t connectivity, on simple graphs given by their adjacency matrices (Cslib.Complexity.encUSTCON), is in L (Cslib.Complexity.USTCON_mem_L).

The decider is the read machine Cslib.USTCON.Reader.machine, which walks in Reingold's graph of the input along all label sequences of length O(log n) and evaluates its rotation map in place with a constant number of labels per level; its simulation on multi-tape machines runs in space O(log m) on encodings of length m (Cslib.USTCON.computableInLogSpace_decide). As for every problem in L enc, the decider is only required to be correct on the encodings of instances; recognising which bit strings are encodings is not part of the statement.

Symmetric logarithmic space (Cslib.Complexity.SL) is defined here by its logspace many-one reduction characterization as the class of problems logspace many-one reducible to USTCON Lewis and Papadimitriou Reingold, Section 1 and Theorem 4.2 (the symmetric Turing machine model and its equivalence with logspace reducibility to USTCON are not separately formalized). Combining USTCON_mem_L with the logspace reduction of any problem in L to USTCON via the canonical two-vertex witness Cslib.Complexity.USTCONInstance.ofBool yields completeness of USTCON for L (Cslib.Complexity.USTCON_logSpaceComplete_L) and Reingold's corollary SL = L (Cslib.Complexity.SL_eq_L) Reingold, Theorem 4.2.

Main definitions #

Main results #

References #

source
theorem Cslib.Complexity.USTCON_mem_L :
USTCON ∈ L encUSTCON

Reingold's theorem: undirected s–t connectivity is in deterministic logarithmic space.

source
def Cslib.Complexity.SL {α : Type} (enc : α ↪ List Bool) :
Set (Set α)

Symmetric logarithmic space SL, defined by its logspace many-one reduction characterization as the class of problems logspace many-one reducible to undirected s–t connectivity USTCON Lewis and Papadimitriou Reingold, Section 1 and Theorem 4.2. The symmetric Turing machine model and its equivalence with logspace reducibility to USTCON are not separately formalized.

Instances For
    source
    @[simp]
    theorem Cslib.Complexity.mem_SL_iff {α : Type} {enc : α ↪ List Bool} {A : Set α} :
    A ∈ SL enc ↔ LogSpaceReducible enc encUSTCON A USTCON

    Membership in SL is logspace many-one reducibility to USTCON.

    source
    theorem Cslib.Complexity.USTCON_mem_SL :
    USTCON ∈ SL encUSTCON

    Undirected s–t connectivity belongs to SL.

    source
    theorem Cslib.Complexity.LogSpaceReducible.mem_SL {α β : Type} {enc : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (hAB : LogSpaceReducible enc encB A B) (hB : B ∈ SL encB) :
    A ∈ SL enc

    SL is closed under logspace many-one reductions.

    source
    theorem Cslib.Complexity.USTCON_logSpaceHard_SL :
    LogSpaceHard (fun {α : Type} => SL) encUSTCON USTCON

    USTCON is logspace-hard for SL. This holds by the definition of SL; the theorem of Lewis and Papadimitriou about symmetric machines is not formalized.

    source
    theorem Cslib.Complexity.USTCON_logSpaceComplete_SL :
    LogSpaceComplete (fun {α : Type} => SL) encUSTCON USTCON

    USTCON is logspace-complete for SL, by the definition of SL. For symmetric machines this is the theorem of Lewis and Papadimitriou [LP82], which is not formalized.

    source
    theorem Cslib.Complexity.USTCON_logSpaceHard_L :
    LogSpaceHard (fun {α : Type} => L) encUSTCON USTCON

    USTCON is logspace-hard for L: compose a logspace decider with the finite map USTCONInstance.ofBool.

    source
    theorem Cslib.Complexity.USTCON_logSpaceComplete_L :
    LogSpaceComplete (fun {α : Type} => L) encUSTCON USTCON

    USTCON is logspace-complete for L Reingold, Theorem 4.1.

    source
    theorem Cslib.Complexity.SL_subset_L {α : Type} {enc : α ↪ List Bool} :
    SL enc ⊆ L enc

    Symmetric logarithmic space is contained in deterministic logarithmic space: every problem logspace-reducible to USTCON is in L by USTCON_mem_L Reingold, Theorem 4.2.

    source
    theorem Cslib.Complexity.L_subset_SL {α : Type} {enc : α ↪ List Bool} :
    L enc ⊆ SL enc

    Deterministic logarithmic space is contained in symmetric logarithmic space: every problem in L reduces in logarithmic space to USTCON via a two-vertex witness.

    source
    theorem Cslib.Complexity.SL_eq_L {α : Type} {enc : α ↪ List Bool} :
    SL enc = L enc

    Reingold's corollary (SL = L) Reingold, Theorem 4.2: symmetric logarithmic space, characterized by logspace many-one reducibility to USTCON, coincides with deterministic logarithmic space.

    source
    theorem Cslib.Complexity.compl_mem_SL {α : Type} {enc : α ↪ List Bool} {A : Set α} (h : A ∈ SL enc) :
    Aᶜ ∈ SL enc

    SL is closed under complement, as a consequence of SL = L and compl_mem_L.