Undirected connectivity in logarithmic space

Reingold's theorem: deciding undirected s–t connectivity on the encodings Cslib.Complexity.encUSTCON is computable in logarithmic space (Cslib.USTCON.computableInLogSpace_decide) Reingold, Theorem 4.1 Arora and Barak, Section 21.4.

The step machine simulating the read machine Cslib.USTCON.Reader.machine is tidy within the space of its states and the position of its head (Cslib.USTCON.Reader.tidy_machine). It computes the output of the read machine (Turing.ReadMachine.computes_toStepMachine), which halts on an encoded instance with the answer (Cslib.USTCON.Reader.exists_run_eq), and its states along the run are states of the read machine together with a head position at most m + 1 (Turing.ReadMachine.exists_state_run), which have O(log m) bits on encodings of length m (Cslib.USTCON.Reader.length_encState_run_le). Correctness is claimed only on encodings of instances; recognising which bit strings are encodings is not formalised.

Main results

• Cslib.USTCON.computableTidilyInBigO_decide: the decision in space O(log n).
• Cslib.USTCON.computableInLogSpace_decide: the decision is computable in logarithmic space.

References

• O. Reingold, Undirected connectivity in log-space
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

theorem Cslib.USTCON.computableTidilyInBigO_decide : ∃ (t : Complexity.USTCONInstance → ℕ), Turing.MultiTapeTM.ComputableTidilyInBigO (fun (I : Complexity.USTCONInstance) => decide (I ∈ Complexity.USTCON)) Complexity.encUSTCON Turing.MultiTapeTM.encBool t fun (I : Complexity.USTCONInstance) => (Complexity.encUSTCON I).length.log2 + 1

Undirected connectivity in space O(log n): the decision of undirected s–t connectivity is tidily computable from the encoded instance in space linear in the logarithm of its length.

theorem Cslib.USTCON.computableInLogSpace_decide : Turing.MultiTapeTM.ComputableInLogSpace (fun (I : Complexity.USTCONInstance) => decide (I ∈ Complexity.USTCON)) Complexity.encUSTCON Turing.MultiTapeTM.encBool

Reingold's theorem: deciding undirected s–t connectivity is computable in logarithmic space, on encodings of instances by their adjacency matrices.