Accepting choice strings of a fair-coin table

A closed fair-coin table Turing.MultiTapePTM k Bool State is the binary-choice normal form of a machine: a run is a deterministic replay of a list of choice bits, one bit per live step. When both branches of an instruction agree, its bit is ignored, and a halted configuration ignores all further bits (Turing.MultiTapePTM.stepCoins). So every run on τ bits is padded to exactly τ steps. A nondeterministic machine with finitely many states and a binary alphabet is put in this form by its choice table Turing.MultiTapeNTM.choiceTable, which encodes each choice in binary and rejects at a stuck configuration.

The accepting count Turing.MultiTapePTM.acceptCount machine input τ is the number of bit strings y ∈ {0,1}^τ on which the table emits [true] on input: the count A_M(x) of the counting simulations of nondeterministic and probabilistic time. It is the generic count Cslib.Complexity.acceptCount of the replay predicate, so the elementary lemmas about that count (Cslib.Complexity.acceptCount_le_two_pow, Cslib.Complexity.acceptCount_pos_iff, …) apply to it directly. Its fraction of all 2 ^ τ strings is exactly the probability that the closed fair-coin run outputs [true] (Turing.MultiTapePTM.eval_runClosed_apply_eq_acceptCount). The membership characterizations for nondeterministic and bounded-error deciders are in CslibFrontier.Computability.Complexity.Classes.Time.AcceptCount.

Main definitions

• Turing.MultiTapePTM.acceptCount: the number of accepting choice strings of a given length.

Main results

• Turing.MultiTapePTM.eval_runClosed_apply_eq_acceptCount: the probability of output [true] is the accepting count divided by 2 ^ τ.
• Turing.MultiTapePTM.half_lt_eval_runClosed_apply_iff: strict majority acceptance, as an integer comparison 2 ^ τ < 2 * acceptCount.
• Turing.MultiTapePTM.runClosedCoins_eq_output_stepCoins: the replay on upstream configurations.

@[reducible, inline]

abbrev Turing.MultiTapePTM.acceptCount {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) (input : List Bool) (τ : ℕ) : ℕ

The accepting count A_M(x): the number of choice strings y ∈ {0,1}^τ replaying which the closed fair-coin table emits [true] on input.

theorem Turing.MultiTapePTM.eval_runClosed_apply_eq_acceptCount {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) (input : List Bool) (τ : ℕ) : (machine.runClosed τ input).eval [true] = ↑(machine.acceptCount input τ) / 2 ^ τ

Acceptance probability is the accepting fraction. The closed fair-coin run with clock τ outputs [true] with probability acceptCount / 2 ^ τ.

theorem Turing.MultiTapePTM.half_lt_eval_runClosed_apply_iff {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) (input : List Bool) (τ : ℕ) : 2⁻¹ < (machine.runClosed τ input).eval [true] ↔ 2 ^ τ < 2 * machine.acceptCount input τ

Strict majority acceptance is the integer comparison 2 ^ τ < 2 * acceptCount.

theorem Turing.MultiTapePTM.runClosedCoins_eq_output_stepCoins {k : ℕ} {State : Type} (machine : MultiTapePTM k Bool State) (input coins : List Bool) : machine.runClosedCoins coins input = (machine.stepCoins coins (Cfg.init machine.initial input)).output

The replay on the configurations of the shared interpreter is the replay on upstream configurations, by deterministic steps under each coin.