Radix rounds

A simulation that cannot compute the space of its source can still find a compact configuration graph that represents every reachable view: it tries the radices startRadix State n, 4 * startRadix State n, 16 * startRadix State n, … in turn and keeps the first one in whose graph no reachable vertex overflows (Turing.MultiTapeNTM.ConfigurationGraph.fits_of_not_overflow). The space of the source then only bounds the number of rounds: a source visiting at most S work cells fits every radix from round 4 * S + 1 on (Turing.MultiTapeNTM.ConfigurationGraph.fits_roundRadix_of_runsInSpace), and the vertices of round j have O(j + log₂ n) bits (Turing.MultiTapeNTM.ConfigurationGraph.vertexWidth_roundRadix_le). Inductive counting grows its radix this way, so that its space bound need not be constructible [Imm88].

Main definitions

• Turing.MultiTapeNTM.ConfigurationGraph.startRadix: the first radix, above every input position and finite tag.
• Turing.MultiTapeNTM.ConfigurationGraph.roundRadix: the radix of round j, 4 ^ j times the first.

Main results

• Turing.MultiTapeNTM.ConfigurationGraph.fits_init, Turing.MultiTapeNTM.ConfigurationGraph.startID_lt: the start view fits every radix above the finite tags, so in particular every round.
• Turing.MultiTapeNTM.ConfigurationGraph.fits_roundRadix_of_runsInSpace: a source visiting at most S work cells fits every round from 4 * S + 1 on.
• Turing.MultiTapeNTM.ConfigurationGraph.roundRadix_le_two_pow, Turing.MultiTapeNTM.ConfigurationGraph.vertexWidth_roundRadix_le: round j has a radix below 2 ^ (2 * j + log₂ n + O(1)) and vertices of O(j + log₂ n) bits.

References

• N. Immerman, Nondeterministic Space Is Closed under Complementation
• M. Sipser, Introduction to the Theory of Computation, Section 8.6

The radices

def Turing.MultiTapeNTM.ConfigurationGraph.startRadix (State : Type) [Fintype State] (n : ℕ) : ℕ

The first radix tried: above every input position and every finite tag.

theorem Turing.MultiTapeNTM.ConfigurationGraph.le_startRadix {State : Type} [Fintype State] (n : ℕ) : n + 2 ≤ startRadix State n

theorem Turing.MultiTapeNTM.ConfigurationGraph.card_lt_startRadix {State : Type} [Fintype State] (n : ℕ) : Fintype.card (Option State) + 3 < startRadix State n

def Turing.MultiTapeNTM.ConfigurationGraph.roundRadix (State : Type) [Fintype State] (n j : ℕ) : ℕ

The radix of round j: the first radix times 4 ^ j.

theorem Turing.MultiTapeNTM.ConfigurationGraph.roundRadix_zero {State : Type} [Fintype State] (n : ℕ) : roundRadix State n 0 = startRadix State n

theorem Turing.MultiTapeNTM.ConfigurationGraph.roundRadix_succ {State : Type} [Fintype State] (n j : ℕ) : roundRadix State n (j + 1) = 4 * roundRadix State n j

theorem Turing.MultiTapeNTM.ConfigurationGraph.startRadix_le_roundRadix {State : Type} [Fintype State] (n j : ℕ) : startRadix State n ≤ roundRadix State n j

theorem Turing.MultiTapeNTM.ConfigurationGraph.card_lt_roundRadix {State : Type} [Fintype State] (n j : ℕ) : Fintype.card (Option State) + 1 < roundRadix State n j

theorem Turing.MultiTapeNTM.ConfigurationGraph.roundRadix_mono {State : Type} [Fintype State] (n : ℕ) {j j' : ℕ} (h : j ≤ j') : roundRadix State n j ≤ roundRadix State n j'

theorem Turing.MultiTapeNTM.ConfigurationGraph.vertexBound_mono {k B B' : ℕ} (h : B ≤ B') : vertexBound B ≤ vertexBound B'

Larger radices have larger ambient graphs.

theorem Turing.MultiTapeNTM.ConfigurationGraph.roundRadix_le_two_pow {State : Type} [Fintype State] (n j : ℕ) : roundRadix State n j ≤ 2 ^ (2 * j + n.log2 + Fintype.card (Option State) + 4)

Round j has a radix below 2 ^ (2 * j + log₂ n + O(1)).

theorem Turing.MultiTapeNTM.ConfigurationGraph.vertexWidth_roundRadix_le (k : ℕ) (State : Type) [Fintype State] (n j : ℕ) : vertexWidth k (roundRadix State n j) ≤ Fintype.card (Register k) * (2 * j + n.log2 + Fintype.card (Option State) + 4) + 1

The vertices of round j have O(j + log₂ n) bits.

Fitting the rounds

theorem Turing.MultiTapeNTM.ConfigurationGraph.fits_init {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B : ℕ} {w : List Bool} (hB : Fintype.card (Option State) + 1 < B) : Fits B (registers (ntm.initView w))

The initial view fits every radix above the finite tags.

theorem Turing.MultiTapeNTM.ConfigurationGraph.startID_lt {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {B : ℕ} (hB : Fintype.card (Option State) + 1 < B) : startID ntm B < vertexBound B

The start vertex lies below the ambient bound of every radix above the finite tags.

theorem Turing.MultiTapeNTM.ConfigurationGraph.fits_roundRadix_of_runsInSpace {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} {S j : ℕ} (hs : ntm.RunsInSpace w S) (hj : 4 * S + 1 ≤ j) {v : FiniteCfg k Bool State} (hv : Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v) : Fits (roundRadix State w.length j) (registers v)

A space bound fits the late rounds: every view reachable by a source that visits at most S work cells fits the radix of every round from 4 * S + 1 on.