The configuration graph as an instance of directed connectivity

A nondeterministic machine ntm within space c * (Nat.log2 n + 1) accepts an input w exactly when an accepting halted vertex is reachable from the start vertex in its compact configuration graph (Turing.MultiTapeNTM.ConfigurationGraph.accepts_iff_reachable_bad_of_runsInSpace). Adding one sink vertex, with an arc from every accepting halted vertex, turns this into a question of directed s–t connectivity (Cslib.Complexity.STCON.configurationInstance): the vertices are the vertexBound identifiers of the compact graph and the sink, the source is the start vertex and the target is the sink Sipser, Theorem 8.25.

The instance is computed in logarithmic space from the framed input (Cslib.Complexity.STCON.computableInLogSpace_configurationInstance) by a counter program with output (Cslib.Complexity.STCON.writer). It counts the input length n, writes the unary header, and writes the adjacency matrix entry by entry, keeping only n, the two vertex identifiers and the code of one input symbol: each entry reads at most the one input bit that the arc of the configuration graph depends on, and evaluates the arithmetic edge test (Turing.MultiTapeNTM.ConfigurationGraph.edgeExpr). The identifiers are below a fixed polynomial in n, so the registers stay polynomially bounded. The framing of the input keeps them bounded by a polynomial in the length of the input even when the instance is encoded by the empty word.

Main definitions

• Cslib.Complexity.STCON.sinkAdj: the arcs of the configuration graph with a sink.
• Cslib.Complexity.STCON.configurationInstance: the instance of directed connectivity.
• Cslib.Complexity.STCON.writer: the counter program writing the encoded instance.

Main results

• Cslib.Complexity.STCON.configurationInstance_mem_iff: the instance is in STCON exactly when the machine accepts.
• Cslib.Complexity.STCON.computableInLogSpace_configurationInstance: the instance is computed in logarithmic space.

References

• M. Sipser, Introduction to the Theory of Computation, Theorem 8.25

theorem Cslib.Complexity.STCON.startID_lt_vertexBound {k : ℕ} {State : Type} [Fintype State] (ntm : Turing.MultiTapeNTM k Bool State) (c n : ℕ) : Turing.MultiTapeNTM.ConfigurationGraph.startID ntm (Turing.MultiTapeNTM.ConfigurationGraph.radix (Turing.MultiTapeNTM.ConfigurationGraph.radixExponent State c) n) < Turing.MultiTapeNTM.ConfigurationGraph.vertexBound (Turing.MultiTapeNTM.ConfigurationGraph.radix (Turing.MultiTapeNTM.ConfigurationGraph.radixExponent State c) n)

The start vertex is a vertex of the ambient graph.

noncomputable def Cslib.Complexity.STCON.sinkAdj {k : ℕ} {State : Type} [Fintype State] (ntm : Turing.MultiTapeNTM k Bool State) (D : ℕ) (w : List Bool) (u v : ℕ) : Bool

The arcs of the configuration graph on w, with a sink at vertexBound: an arc of the compact configuration graph between identifiers below vertexBound, and an arc from each accepting halted vertex to the sink.

noncomputable def Cslib.Complexity.STCON.configurationInstance {k : ℕ} {State : Type} [Fintype State] (ntm : Turing.MultiTapeNTM k Bool State) (c : ℕ) (w : List Bool) : STCONInstance

The configuration graph of ntm on w as an instance of directed connectivity: the vertexBound identifiers of the compact configuration graph and a sink, with source the start vertex and target the sink.

theorem Cslib.Complexity.STCON.configurationInstance_mem_iff {k : ℕ} {State : Type} [Fintype State] (ntm : Turing.MultiTapeNTM k Bool State) (c : ℕ) {w : List Bool} (hs : ntm.RunsInSpace w (c * (w.length.log2 + 1))) : configurationInstance ntm c w ∈ STCON ↔ ntm.Accepts w

The instance is in STCON exactly when the machine accepts, for a machine within space c * (Nat.log2 n + 1) on the input.

The writer

@[reducible, inline]

noncomputable abbrev Cslib.Complexity.STCON.numVerticesExpr {k : ℕ} (D : ℕ) : Turing.CounterProgram.Expr

The number of vertices, from the input length in register 0.

noncomputable def Cslib.Complexity.STCON.writer {k : ℕ} {State : Type} [Fintype State] (ntm : Turing.MultiTapeNTM k Bool State) (D : ℕ) : Turing.CounterProgram

The writer of the encoded instance, on the framed input. Register 0 holds the input length, register 1 a counter or the row, register 2 the column and register 3 the code of the input symbol of the row's arc. Labels 0 and 1 count the input; the three counting loops at labels 2, 7 and 12 write the unary header; the nested loops at labels 17 and 20 write the matrix, the entry at labels 23 to 32; label 33 halts.

theorem Cslib.Complexity.STCON.computableInLogSpace_configurationInstance {k : ℕ} {State : Type} [Fintype State] (ntm : Turing.MultiTapeNTM k Bool State) (c : ℕ) : Turing.MultiTapeTM.ComputableInLogSpace (configurationInstance ntm c) (Turing.MultiTapeTM.encFramed Turing.MultiTapeTM.encBits) encSTCON

The instance is computed in logarithmic space from the framed input.