Polynomial time on single-tape machines

10 fully proved

Rev Tail

InductiveStacks of the reversal component#✓fully proved

The two stack indices of the reversal component: the input stack \(X\) and the output stack \(O\).

inductive K | X | O
  deriving DecidableEq

Used by 4

Used byThe reversal component · Reversing and dropping the first bit is polynomial-time · Program of the reversal component · Running the reversal component

InductiveLabels of the reversal component#✓fully proved

The three labels of the reversal component: mv (move the input onto the output), drop (drop one symbol) and done.

inductive L | mv | drop | done
  deriving DecidableEq

Used by 4

Used byThe reversal component · Reversing and dropping the first bit is polynomial-time · Program of the reversal component · Running the reversal component

DefinitionProgram of the reversal component#✓fully proved

The multi-stack program over the stacks \(X\) and \(O\), both with alphabet \(\mathrm{Bool}\), with a Boolean internal state: at label mv it moves the bits of \(X\) one at a time onto \(O\) (reversing them) and then goes to drop; at drop it pops \(O\) once and goes to done; at done it halts.

def prog : L → TM2.Stmt (fun _ : K ↦ Bool) L Bool
  | .mv => moveB .X .O some id .mv .drop
  | .drop => .pop .O (fun s _ ↦ s) (.goto fun _ ↦ .done)
  | .done => .halt

Uses 4 · Used by 2

Statement usesStacks of the reversal component · Labels of the reversal component · Flag bit of a machine state · Bit-moving loop

Used byThe reversal component · Reversing and dropping the first bit is polynomial-time

AbbreviationThe reversal component#✓fully proved

The component machine with two stacks, the input stack \(X\) and the output stack \(O\), both over the alphabet \(\mathrm{Bool}\); the three labels mv, drop and done; the program that moves the bits of \(X\) onto \(O\) (reversing them), pops \(O\) once and halts; and the stack list \([X, O]\).

noncomputable abbrev comp : Cslib.Complexity.Host.Comp where
  K := K
  Γ := fun _ ↦ Bool
  L := L
  prog := prog
  ks := [.X, .O]
  ks_nodup := by decide
  mem_ks k := by cases k <;> decide

Uses 4 · Used by 2

Statement usesComponent machine · Stacks of the reversal component · Labels of the reversal component · Program of the reversal component

Used byReversing and dropping the first bit is polynomial-time · Running the reversal component

TheoremRunning the reversal component#✓fully proved

For every bit list \(x\), the program of the reversal component, started at label mv with internal state false, with the bits of \(x\) on the input stack \(X\) and every other stack empty, reaches label done within at most \(|x| + 2\) steps, with some internal state and some stacks whose output stack \(O\) holds the reversal of \(x\) with its first entry removed.

theorem run (x : List Bool) : ∃ v S', RunLe comp.prog (x.length + 2)
    ⟨some L.mv, false, Function.update (fun _ ↦ []) K.X (x.map id)⟩ ⟨some L.done, v, S'⟩ ∧
      S' K.O = x.reverse.tail.map (Equiv.refl Bool).symm

Uses 9 · Used by 1

Statement usesComponent machine · Stacks of the reversal component · Labels of the reversal component · The reversal component · Runs within a step budget

Proof usesFlag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Running the bit-moving loop

Used byReversing and dropping the first bit is polynomial-time

DefinitionReversing and dropping the first bit is polynomial-time#✓fully proved

A finite multi-stack Turing machine whose input and output alphabets are both identified with the bits, together with a polynomial \(p\) with natural-number coefficients, such that for every bit list \(x\), given bit by bit as its own encoding, the machine outputs the reversal of \(x\) with its first entry removed (that is, \(x\) without its last bit, in reverse order) within \(p(|x|)\) steps.

noncomputable def computable :
    TM2ComputableInPolyTime (fun l : List Bool ↦ l) (fun l : List Bool ↦ l)
      (fun x : List Bool ↦ x.reverse.tail) :=
  Cslib.Complexity.Host.reduction (c := comp) (cX := K.X) (cO := K.O) (gX := id)
    (start := L.mv) (done := L.done) (Equiv.refl Bool) _ (Polynomial.X + Polynomial.C 2) rfl
    fun x ↦ by simpa using run x

Uses 8 · Used by 1

Statement usesComponent machine · Reduction host · Stacks of the reversal component · Labels of the reversal component · The reversal component · Program of the reversal component · Running the reversal component · Runs within a step budget

Used byProblems in P are decided in polynomial time by single-tape machines

Of TM2

TheoremThe answer machine runs in one step#✓fully proved

Let \(M\) be a finite multi-stack machine with finite stack alphabets, whose input alphabet is identified with the bits by \(e\) and whose output alphabet by \(e_1\). For every non-blank cell \(x\) of the single-tape emulation alphabet of \(M\), the answer machine of \(M\), started on the one-cell tape \(x\), halts within at most one step on the one-cell tape holding the input-bit cell of the answer of \(x\) (the bit telling whether \(x\) holds \(e_1^{-1}(\mathrm{true})\) on the output stack).

theorem answerTM_outputsWithinTime (x : NonBlank (TM2to1.Γ' tm.K tm.Γ)) :
    (answerTM tm e e₁).OutputsWithinTime [x] [inCell tm e (cellAnswer tm e₁ x)] 1

Uses 4 · Used by 1

Statement usesNon-blank symbols · The answer machine · The answer bit of a cell · Input cell of a bit

Used byThe decider within time

TheoremThe decider within time#✓fully proved

Let \(M\) be a finite multi-stack machine with finite stack alphabets, whose input alphabet is identified with the bits by \(e\) and whose output alphabet by \(e_1\), and let \(C\) be the emulation constant of \(M\). Let \(w\) be a bit list, \(b\) a bit and \(t\) a natural number. Suppose \(M\), started with its input stack holding the bits of \(w\) in reverse order followed by \(\mathrm{true}\) (read through \(e^{-1}\)), is after exactly \(t\) steps in the halting configuration whose output stack holds just \(e_1^{-1}(b)\), whose other stacks are empty and whose internal state is the initial one. Then the single-tape decider of \(M\), started on the tape of input-bit cells of \(w\), halts on the one-cell tape holding the input-bit cell of \(b\) within \(C t (|w| + 1 + C t + 1) + 4\) steps.

theorem deciderTM_outputsWithinTime {w : List Bool} (b : Bool) {t : ℕ}
    (h : (flip bind tm.step)^[t] (some (initList tm ((w.reverse ++ [true]).map e.symm))) =
      some (haltList tm [e₁.symm b])) :
    (deciderTM tm e e₁).OutputsWithinTime (w.map (inCell tm e)) [inCell tm e b]
      (emulationConstant tm * t * (w.length + 1 + emulationConstant tm * t + 1) + 4)

Uses 20 · Used by 1

Statement usesNon-blank symbols · The decider of a multi-stack machine · Input cell of a bit · Emulation constant

Proof usesStacks of height at most one give a one-cell tape · The answer machine · The answer machine runs in one step · The bottom cell of the start tape · The answer bit of a cell · States of the single-tape emulation · Finite single-tape emulation of a multi-stack machine · The bottom cell followed by the input word is the emulation's start tape · Timed outputs compose · The machine that prepends a symbol · Prepending a symbol takes at most two steps · The single-tape simulation outputs within one extra step · Single-tape emulation of halting multi-stack runs · A multi-stack machine is supported by all its labels · Two-step single-tape translation of a multi-stack machine · The emulation visits finitely many states

Used byProblems in P are decided in polynomial time by single-tape machines

Complexity

DefinitionPolynomial time on single-tape machines#✓fully proved

The class of decision problems \(L\) for which there are a finite alphabet \(\Sigma\) with a designated default element, an injective map \(\iota\) from the bits to \(\Sigma\), a single-tape Turing machine \(M\) over \(\Sigma\) and a polynomial \(p\) with natural-number coefficients such that, for every bit list \(w\), the machine \(M\) started on the word \(\iota(w)\) (the bits of \(w\) mapped by \(\iota\)) halts on the one-cell tape \(\iota(L(w))\) within \(p(|w|)\) steps.

def SingleTapeP : DecisionComplexityClass :=
  {L | ∃ (Symbol : Type) (_ : Inhabited Symbol) (_ : Fintype Symbol) (ι : Bool → Symbol),
    Function.Injective ι ∧ ∃ (tm : SingleTapeTM Symbol) (p : Polynomial ℕ),
      ∀ w : List Bool, tm.OutputsWithinTime (w.map ι) [ι (L w)] (p.eval w.length)}

Uses 2 · Used by 1

Statement usesComplexity classes · Decision problems

Used byProblems in P are decided in polynomial time by single-tape machines

TheoremProblems in P are decided in polynomial time by single-tape machines#✓fully proved

Every decision problem in the class \(\mathrm{P}\) (defined with multi-stack machines) belongs to the class of decision problems decided in polynomial time by single-tape machines.

The proof reverses the input, restricts the multi-stack machine to finite alphabets and emulates it on a single tape within quadratic overhead.

theorem P_subset_singleTapeP : P ⊆ SingleTapeP

Uses 22

Statement usesPolynomial time on single-tape machines · Complexity classes · Decision problems · The complexity class P

Proof usesPolynomial-time encoder to the canonical bit-list encoding · Reversing and dropping the first bit is polynomial-time · Non-blank symbols · The decider of a multi-stack machine · The decider within time · Input cell of a bit · Emulation constant · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · The composite polynomial-time TM2 computation · Symbols a statement may push · Relevant symbols of a stack

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.