Time classes through accepting choice strings

Problems in NTIME and BPTIME are decided by comparing the accepting count of a fixed binary-choice machine (Turing.MultiTapePTM.acceptCount) with a threshold, at every number τ of choice bits at least a linear function of the time bound. This is the normal form used by counting simulations of nondeterministic and probabilistic time, which compute the accepting count exactly.

• A nondeterministic decider is replayed by its choice table Turing.MultiTapeNTM.choiceTable, which encodes each choice in binary and rejects at a stuck configuration: an instance is a member exactly when the accepting count is positive (Turing.MultiTapeNTM.DecidesInTime.mem_iff_acceptCount_choiceTable_pos).
• A bounded-error fair-coin decider accepts a member with probability at least 2 / 3 and a nonmember with probability at most 1 / 3, so an instance is a member exactly when more than half of the choice strings accept (Turing.MultiTapePTM.DecidesWithBoundedErrorInTime.mem_iff_two_pow_lt_two_mul_acceptCount).

Both hold for every τ at least the clock: a halted table ignores further bits.

Main results

• Turing.MultiTapeNTM.DecidesInTime.mem_iff_acceptCount_choiceTable_pos: nondeterministic acceptance is a positive accepting count.
• Turing.MultiTapePTM.DecidesWithBoundedErrorInTime.mem_iff_two_pow_lt_two_mul_acceptCount: bounded-error acceptance is a strict-majority accepting count.
• Cslib.Complexity.exists_acceptCount_of_mem_NTIME, Cslib.Complexity.exists_acceptCount_of_mem_BPTIME: the class-level normal forms.

theorem Turing.MultiTapeNTM.DecidesInTime.mem_iff_acceptCount_choiceTable_pos {k : ℕ} {State : Type} [Finite State] {α : Type} {enc : α ↪ List Bool} {ntm : MultiTapeNTM k Bool State} {A : Set α} {t : α → ℕ} (h : ntm.DecidesInTime enc A t) {a : α} {τ : ℕ} (hτ : Nat.card (Action k Bool State) * t a ≤ τ) : a ∈ A ↔ 0 < ntm.choiceTable.acceptCount (enc a) τ

Nondeterministic acceptance is a positive accepting count. If ntm decides A within t, then a ∈ A exactly when some choice string of length τ makes the choice table accept, for every τ of at least M * t a, where M is the number of actions.

theorem Turing.MultiTapePTM.DecidesWithBoundedErrorInTime.mem_iff_two_pow_lt_two_mul_acceptCount {k : ℕ} {State α : Type} {enc : α ↪ List Bool} {machine : MultiTapePTM k Bool State} {A : Set α} {t : α → ℕ} (h : machine.DecidesWithBoundedErrorInTime enc A t) {a : α} {τ : ℕ} (hτ : t a ≤ τ) : a ∈ A ↔ 2 ^ τ < 2 * machine.acceptCount (enc a) τ

Bounded-error acceptance is a strict-majority accepting count. If machine decides A with bounded error within t, then a ∈ A exactly when more than half of the choice strings of length τ accept, for every τ of at least t a.

theorem Cslib.Complexity.exists_acceptCount_of_mem_NTIME {α : Type} {enc : α ↪ List Bool} {A : Set α} {t : ℕ → ℕ} (h : A ∈ NTIME enc t) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : Turing.MultiTapePTM k Bool State) (c₁ : ℕ) (c₂ : ℕ), ∀ (a : α) (τ : ℕ), c₁ * t (enc a).length + c₂ ≤ τ → (a ∈ A ↔ 0 < machine.acceptCount (enc a) τ)

Nondeterministic time as accepting counts. A problem in NTIME enc t is decided by a fixed binary-choice machine with a binary alphabet and finitely many states: for constants c₁ and c₂, an instance is a member exactly when its accepting count on τ choice bits is positive, for every τ ≥ c₁ * t n + c₂ on instances of encoded length n.

theorem Cslib.Complexity.exists_acceptCount_of_mem_BPTIME {α : Type} {enc : α ↪ List Bool} {A : Set α} {t : ℕ → ℕ} (h : A ∈ BPTIME enc t) : ∃ (k : ℕ) (State : Type) (_ : Finite State) (machine : Turing.MultiTapePTM k Bool State) (c₁ : ℕ) (c₂ : ℕ), ∀ (a : α) (τ : ℕ), c₁ * t (enc a).length + c₂ ≤ τ → (a ∈ A ↔ 2 ^ τ < 2 * machine.acceptCount (enc a) τ)

Bounded-error probabilistic time as accepting counts. A problem in BPTIME enc t is decided by a fixed fair-coin machine with a binary alphabet and finitely many states: for constants c₁ and c₂, an instance is a member exactly when more than half of its choice strings of length τ accept, for every τ ≥ c₁ * t n + c₂ on instances of encoded length n.