Online witness machines

A WitnessTM k is a deterministic machine with k ordinary work tapes and a separate, read-only Boolean witness stream. Its GuessProtocol permits reading a witness bit only when consuming it; nonadvancing steps leave the stream alone. The stream starts at its first bit, with no setup cost and no observable end marker. This is an online witness model, not a two-way certificate-input model.

Time is uniform over all streams. Space excludes the witness tape but charges ordinary work, input-tail travel, and output travel exactly as for NTM. Acceptance means halting with output 1; every other halted output rejects.

def Complexity.NTM.DecidesInTimeSpace {k : ℕ} (N : NTM k) (L : Language) (T S : ℕ → ℕ) : Prop

One NTM simultaneously obeys the given time and space bounds. Every prefix of every full-length choice sequence satisfies the decision-space convention.

Equations

• One or more equations did not get rendered due to their size.

structure Complexity.WitnessTM (k : ℕ) : Type 1

A deterministic machine with a separate online witness stream. The last physical work tape implements the stream and is excluded from charged space.

• machine : TM (k + 1)

  The deterministic machine, including its last, distinguished witness tape.

• advancing : self.machine.Q → Bool

  States in which the next witness bit is read and consumed.

• protocol : self.machine.GuessProtocol self.advancing

  The witness is read-only and never consulted without being consumed.

def Complexity.WitnessTM.run {k : ℕ} (W : WitnessTM k) (x : List Bool) (g : ℕ → Bool) (t : ℕ) : Cfg (k + 1) W.machine.Q

Execute with input x and externally supplied witness stream g, standing still after halting. All ordinary heads start at cell zero; the witness starts at one.

Equations

• W.run x g t = W.machine.traceD t (Complexity.NTM.loadCfg W.machine x g)

def Complexity.WitnessTM.toNTM {k : ℕ} (W : WitnessTM k) : NTM k

Replace each consumed witness bit by a nondeterministic transition choice.

Equations

• W.toNTM = Complexity.NTM.ofGuess W.machine

def Complexity.WitnessTM.AllWitnessesHaltIn {k : ℕ} (W : WitnessTM k) (T : ℕ → ℕ) : Prop

A single time bound applies to every input and every witness stream.

Equations

• W.AllWitnessesHaltIn T = ∀ (x : List Bool) (g : ℕ → Bool), W.machine.halted (W.run x g (T x.length))

def Complexity.WitnessTM.AcceptsInTime {k : ℕ} (W : WitnessTM k) (x : List Bool) (t : ℕ) : Prop

Some witness stream causes acceptance within the given number of steps.

Equations

• W.AcceptsInTime x t = ∃ (g : ℕ → Bool), W.machine.halted (W.run x g t) ∧ (W.run x g t).output.cells 1 = Complexity.Γ.one

def Complexity.WitnessTM.DecidesInTime {k : ℕ} (W : WitnessTM k) (L : Language) (T : ℕ → ℕ) : Prop

All witness runs halt within T, and accepting witnesses characterize L.

Equations

• W.DecidesInTime L T = (W.AllWitnessesHaltIn T ∧ ∀ (x : List Bool), x ∈ L ↔ W.AcceptsInTime x (T x.length))

def Complexity.WitnessTM.DecidesInTimeSpace {k : ℕ} (W : WitnessTM k) (L : Language) (T S : ℕ → ℕ) : Prop

Time and space bounds hold simultaneously. The witness tape is uncharged; all visible prefixes obey the ordinary NTM decision-space convention.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.WitnessTM.DecidesInSpace {k : ℕ} (W : WitnessTM k) (L : Language) (S : ℕ → ℕ) : Prop

A uniformly halting online witness machine with the given space bound.

Equations

• W.DecidesInSpace L S = ∃ (T : ℕ → ℕ), W.DecidesInTimeSpace L T S

def Complexity.NTM.toWitnessTM {k : ℕ} (N : NTM k) : WitnessTM k

Run an NTM deterministically by consuming one external witness bit per step. The charged work tapes and finite control are unchanged.

Equations

• N.toWitnessTM = { machine := N.choiceTM, advancing := fun (x : N.choiceTM.Q) => true, protocol := ⋯ }