Directed connectivity by a nondeterministic search in logarithmic space

A nondeterministic counter program (Cslib.Complexity.STCON.searchProgram) decides directed s–t connectivity on the adjacency-matrix encoding Cslib.Complexity.encSTCON in logarithmic space Sipser, Example 8.19. It counts the unary header to learn n, s and t, then walks from s: at each step it accepts if the current vertex is t, rejects once it has taken n steps, and otherwise guesses the next vertex v by incrementing a counter from 0 as long as its choices say so, rejecting when the counter reaches n, and moves to v when the matrix has an arc from the current vertex to v. It stores only the header values, the current vertex, the number of steps taken and the counter, all at most the length of the input, and every branch halts.

The proof uses an invariant of every branch (Cslib.Complexity.STCON.Search.Inv): it records the values of the registers at every label, and in particular that the current vertex is reachable from s, which gives soundness at the accepting label. Every step decreases a rank (Cslib.Complexity.STCON.Search.rank), which bounds the length of every branch. Conversely, a shortest path from s to t, which has fewer than n arcs, is followed by an accepting branch.

Main definitions

• Cslib.Complexity.STCON.searchProgram: the nondeterministic search.

Main results

• Cslib.Complexity.STCON.accepts_searchProgram_iff: the search accepts exactly the instances in STCON.
• Cslib.Complexity.STCON.exists_decidesInLogSpace: one nondeterministic machine decides STCON in logarithmic space, every branch halting.

References

• M. Sipser, Introduction to the Theory of Computation, Example 8.19

def Cslib.Complexity.STCON.searchProgram : Turing.CounterProgram

The nondeterministic search for a path. Register 0 holds the choice, registers 1, 2 and 3 the header values n, s and t, register 4 the current vertex, register 5 the number of steps taken and register 6 the guessed vertex. Label 17 accepts and label 18 rejects.

def Cslib.Complexity.STCON.Search.Reach (I : STCONInstance) (cur : ℕ) : Prop

The vertex cur is reachable from the source.

def Cslib.Complexity.STCON.Search.Loop (I : STCONInstance) (cur steps v : ℕ) : Prop

The registers of the main loop: the current vertex is reachable, at most n steps were taken and the guessed vertex is a vertex.

def Cslib.Complexity.STCON.Search.Phase (I : STCONInstance) : ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → Prop

The values of the registers 1 to 6 at each label.

def Cslib.Complexity.STCON.Search.Bounded (I : STCONInstance) (n s t cur steps v : ℕ) : Prop

The registers 1 to 6 stay below the header values.

def Cslib.Complexity.STCON.Search.Inv (I : STCONInstance) (cfg : Turing.CounterProgram.Config) : Prop

The invariant of every branch.

def Cslib.Complexity.STCON.Search.budget (I : STCONInstance) : ℕ

The total budget of the rank.

def Cslib.Complexity.STCON.Search.progress (I : STCONInstance) (cfg : Turing.CounterProgram.Config) : ℕ

The progress made by a configuration: it increases with every step.

def Cslib.Complexity.STCON.Search.rank (I : STCONInstance) (cfg : Turing.CounterProgram.Config) : ℕ

The rank: the budget left.

Every branch

theorem Cslib.Complexity.STCON.Search.inv_run (I : STCONInstance) (choices : List Bool) : Inv I (searchProgram.toNondeterministicQueryMachine.run I.encode choices)

The invariant holds on every branch.

theorem Cslib.Complexity.STCON.Search.haltsWithin (I : STCONInstance) : searchProgram.toNondeterministicQueryMachine.HaltsWithin I.encode (rank I searchProgram.init)

Every branch halts.

theorem Cslib.Complexity.STCON.Search.mem_of_accepts (I : STCONInstance) (h : searchProgram.toNondeterministicQueryMachine.Accepts I.encode) : I ∈ STCON

An accepting branch is sound: the invariant at the accepting label says that t is reachable from s.

An accepting branch

theorem Cslib.Complexity.STCON.Search.accepts_of_mem (I : STCONInstance) (h : I ∈ STCON) : searchProgram.toNondeterministicQueryMachine.Accepts I.encode

An accepting branch exists when t is reachable from s: a shortest path has fewer than n arcs.

theorem Cslib.Complexity.STCON.accepts_searchProgram_iff (I : STCONInstance) : searchProgram.toNondeterministicQueryMachine.Accepts I.encode ↔ I ∈ STCON

The search accepts exactly the instances in STCON.

theorem Cslib.Complexity.STCON.exists_decidesInLogSpace : ∃ (k : ℕ) (State : Type) (_ : Finite State) (ntm : Turing.MultiTapeNTM k Bool State) (c : ℕ), ntm.DecidesInSpace encSTCON STCON fun (I : STCONInstance) => c * ((encSTCON I).length.log2 + 1)

Directed s–t connectivity in nondeterministic logarithmic space Sipser, Example 8.19: one finite-state nondeterministic machine decides STCON on the encoding encSTCON within space c * (Nat.log2 n + 1) on encodings of length n, every branch halting.