Documentation

Complexitylib.Models.TuringMachine.SingleTape.Internal.Pad

Padding a 0-work-tape NTM with a dummy work tape #

NTM.pad0 turns an NTM 0 into an NTM 1 deciding the same language in the same time bound: the added work tape is never used. The dummy head steps right off ▷ on its first move (respecting the δ_right_of_start discipline) and then parks at cell 1, writing □ over the □ already there, so the dummy tape's cells never change.

This closes the k = 0 case of the single-tape reduction (NTM.exists_singleTape_decidesInTime): the simulation machinery requires at least one work tape, while a padded machine is already single-work-tape.

source
def Complexity.NTM.pad0 (N : NTM 0) :
NTM 1

Pad a 0-work-tape machine with one never-used work tape. The dummy tape's action: step right off ▷, otherwise stay put and write □ (over the □ already under the head).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.NTM.pad0_trace (N : NTM 0) (T : ℕ) (choices : Fin T → Bool) (c : Cfg 0 N.Q) (c1 : Cfg 1 N.Q) :
    c1.state = c.state → c1.input = c.input → c1.output = c.output → (c1.work 0).cells = (Tape.init []).cells → (c1.work 0).head ≤ 1 → (N.pad0.trace T choices c1).state = (N.trace T choices c).state ∧ (N.pad0.trace T choices c1).input = (N.trace T choices c).input ∧ (N.pad0.trace T choices c1).output = (N.trace T choices c).output

    Trace correspondence. The padded machine's run tracks the original's component-wise; the dummy work tape keeps its initial cells with the head parked at cell 0 or 1.

    source
    theorem Complexity.NTM.pad0_trace_init (N : NTM 0) (x : List Bool) (T : ℕ) (choices : Fin T → Bool) :
    (N.pad0.trace T choices (N.pad0.initCfg x)).state = (N.trace T choices (N.initCfg x)).state ∧ (N.pad0.trace T choices (N.pad0.initCfg x)).input = (N.trace T choices (N.initCfg x)).input ∧ (N.pad0.trace T choices (N.pad0.initCfg x)).output = (N.trace T choices (N.initCfg x)).output

    The trace correspondence at the initial configurations.

    source
    theorem Complexity.NTM.pad0_allPathsHaltIn {N : NTM 0} {T : ℕ → ℕ} (h : N.AllPathsHaltIn T) :
    N.pad0.AllPathsHaltIn T

    Padding preserves the all-paths halting bound.

    source
    theorem Complexity.NTM.pad0_acceptsInTime_iff (N : NTM 0) (x : List Bool) (Tn : ℕ) :
    N.pad0.AcceptsInTime x Tn ↔ N.AcceptsInTime x Tn

    Padding preserves timed acceptance, in both directions.

    source
    theorem Complexity.NTM.pad0_decidesInTime {L : Language} {N : NTM 0} {T : ℕ → ℕ} (hdec : N.DecidesInTime L T) :
    N.pad0.DecidesInTime L T

    Padding preserves deciding. A 0-work-tape decider yields a 1-work-tape decider for the same language in the same time bound.