Documentation

CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.ConfigurationGraph.Bounds

Radices accommodating a space bound #

A source machine that visits at most S work cells along every computation prefix has only views whose registers fit any radix B with n + 2 ≤ B, room for the finite control and 3 ^ (4 * S + 1) ≤ B (Turing.MultiTapeNTM.ConfigurationGraph.fits_of_runsInSpace_of_le). For logarithmic space a fixed exponent, depending only on the source machine and its space constant, gives such a radix (n + 2) ^ D. Thus the exact compact graph then has polynomially many vertices, and its local routines take only logarithmically many stored bits.

Main results #

source
theorem Turing.MultiTapeNTM.ConfigurationGraph.fits_of_runsInSpace_of_le {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} {S B : ℕ} (hs : ntm.RunsInSpace w S) (hn : w.length + 2 ≤ B) (hc : Fintype.card (Option State) < B) (h3 : 3 < B) (hstack : 3 ^ (4 * S + 1) ≤ B) {v : FiniteCfg k Bool State} (hv : Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v) :
Fits B (registers v)

Every reachable view fits a large enough radix: one above the input positions, the finite tags, and the ternary stack codes of 4 * S + 1 cells, for a source that visits at most S work cells along every computation prefix.

source
def Turing.MultiTapeNTM.ConfigurationGraph.radixExponent (State : Type) [Fintype State] (c : ℕ) :
ℕ

A generous fixed radix exponent for a machine using c * (log2 n + 1) work cells.

Instances For
    source
    theorem Turing.MultiTapeNTM.ConfigurationGraph.vertexBound_eq_pow {k : ℕ} (D n : ℕ) :
    vertexBound (radix D n) = (n + 2) ^ (D * Fintype.card (Register k))

    The ambient vertex count is exactly a fixed natural power of n+2.

    source
    theorem Turing.MultiTapeNTM.ConfigurationGraph.fits_of_runsInSpace {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} (c : ℕ) (hs : ntm.RunsInSpace w (c * (w.length.log2 + 1))) {v : FiniteCfg k Bool State} (hv : Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v) :
    Fits (radix (radixExponent State c) w.length) (registers v)

    Every view reachable under the native logarithmic space bound fits the fixed radix.

    source
    theorem Turing.MultiTapeNTM.ConfigurationGraph.vertexID_lt_pow_of_runsInSpace {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} (c : ℕ) (hs : ntm.RunsInSpace w (c * (w.length.log2 + 1))) {v : FiniteCfg k Bool State} (hv : Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v) :
    vertexID (radix (radixExponent State c) w.length) v < (w.length + 2) ^ (radixExponent State c * Fintype.card (Register k))

    Every reachable ID is strictly below a natural polynomial in input length.

    source
    theorem Turing.MultiTapeNTM.ConfigurationGraph.length_vertexID_le_of_runsInSpace {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} (c : ℕ) (hs : ntm.RunsInSpace w (c * (w.length.log2 + 1))) {v : FiniteCfg k Bool State} (hv : Relation.ReflTransGen ntm.ViewStep (ntm.initView w) v) :
    (MultiTapeTM.encNat (vertexID (radix (radixExponent State c) w.length) v)).length ≤ (radixExponent State c * Fintype.card (Register k) + 1) * ((w.length + 1).log2 + 1)

    Binary vertex IDs need only logarithmically many bits.

    source
    theorem Turing.MultiTapeNTM.ConfigurationGraph.reachable_lt_pow_of_runsInSpace {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} (c : ℕ) (hs : ntm.RunsInSpace w (c * (w.length.log2 + 1))) {u : ℕ} (hu : Relation.ReflTransGen (Edge ntm (radix (radixExponent State c) w.length) w) (startID ntm (radix (radixExponent State c) w.length)) u) :
    u < (w.length + 2) ^ (radixExponent State c * Fintype.card (Register k))

    Every vertex reachable in the compact graph satisfies the polynomial ambient bound.

    source
    theorem Turing.MultiTapeNTM.ConfigurationGraph.accepts_iff_reachable_bad_of_runsInSpace {k : ℕ} {State : Type} [Fintype State] {ntm : MultiTapeNTM k Bool State} {w : List Bool} (c : ℕ) (hs : ntm.RunsInSpace w (c * (w.length.log2 + 1))) :
    ntm.Accepts w ↔ ∃ (u : ℕ), Relation.ReflTransGen (Edge ntm (radix (radixExponent State c) w.length) w) (startID ntm (radix (radixExponent State c) w.length)) u ∧ bad (radix (radixExponent State c) w.length) w.length u = true

    A logarithmic native space bound supplies the exact polynomial compact graph.