structure TuringMachine.PTM (Q Γ : Type) : Type

A Probabilistic Turing Machine (PTM): a deterministic 1-tape TM augmented with two transition functions δ₀ and δ₁. At each step the machine flips a fair coin and uses δ₀ on outcome 0 and δ₁ on outcome 1.

• blank : Γ
• inputAlpha : Set Γ
• blank_not_in_inputAlpha : self.blank ∉ self.inputAlpha
• δ₀ : Q → Γ → Q × Γ × Direction
• δ₁ : Q → Γ → Q × Γ × Direction
• q₀ : Q
• qAccept : Q
• qReject : Q
• qReject_ne_qAccept : self.qReject ≠ self.qAccept

def TuringMachine.PTM.stepWithCoin {Q Γ : Type} [DecidableEq Q] (M : PTM Q Γ) (c : Config Q Γ) (coin : Bool) : Config Q Γ

Advance the PTM M by one step from configuration c using the given coin flip: chooses δ₁ when coin = true and δ₀ otherwise. Halting configurations (accept/reject) are fixed points.

def TuringMachine.PTM.initConfig {Q Γ : Type} (M : PTM Q Γ) (w : List Γ) : Config Q Γ

The starting configuration of M on input w: the head is at position 0, the state is q₀, and the tape holds the symbols of w with blanks elsewhere.

def TuringMachine.PTM.runWithCoins {Q Γ : Type} [DecidableEq Q] (M : PTM Q Γ) (w : List Γ) (n : ℕ) : (Fin n → Bool) → Config Q Γ

Run the PTM M on input w for n steps, consuming the sequence coins of n coin flips and returning the resulting configuration.

def TuringMachine.PTM.isAcceptConfig {Q Γ : Type} (M : PTM Q Γ) (c : Config Q Γ) : Prop

A configuration c is accepting for M iff its state is M.qAccept.

def TuringMachine.PTM.isRejectConfig {Q Γ : Type} (M : PTM Q Γ) (c : Config Q Γ) : Prop

A configuration c is rejecting for M iff its state is M.qReject.

def TuringMachine.PTM.acceptsWithCoins {Q Γ : Type} [DecidableEq Q] (M : PTM Q Γ) (w : List Γ) (n : ℕ) (coins : Fin n → Bool) : Prop

M accepts input w along the coin-flip branch coins of length n.

def TuringMachine.PTM.rejectsWithCoins {Q Γ : Type} [DecidableEq Q] (M : PTM Q Γ) (w : List Γ) (n : ℕ) (coins : Fin n → Bool) : Prop

M rejects input w along the coin-flip branch coins of length n.

@[implicit_reducible]

instance TuringMachine.instDecidableAcceptsWithCoins {Q Γ : Type} [DecidableEq Q] (M : PTM Q Γ) (w : List Γ) (n : ℕ) (coins : Fin n → Bool) : Decidable (M.acceptsWithCoins w n coins)

Decidability of acceptance along a fixed coin-flip branch, used to count accepting branches via Finset.filter.

@[implicit_reducible]

instance TuringMachine.instDecidableRejectsWithCoins {Q Γ : Type} [DecidableEq Q] (M : PTM Q Γ) (w : List Γ) (n : ℕ) (coins : Fin n → Bool) : Decidable (M.rejectsWithCoins w n coins)

Decidability of rejection along a fixed coin-flip branch.

def TuringMachine.PTM.numAccepting {Q Γ : Type} [DecidableEq Q] (M : PTM Q Γ) (w : List Γ) (n : ℕ) : ℕ

The number of length-n coin-flip sequences on which M accepts w.

def TuringMachine.PTM.numRejecting {Q Γ : Type} [DecidableEq Q] (M : PTM Q Γ) (w : List Γ) (n : ℕ) : ℕ

The number of length-n coin-flip sequences on which M rejects w.

def TuringMachine.PTM.acceptProb {Q Γ : Type} [DecidableEq Q] (M : PTM Q Γ) (w : List Γ) (n : ℕ) : ℚ

The probability that M accepts w when run for n steps with uniform random coins: numAccepting / 2^n.

def TuringMachine.PTM.rejectProb {Q Γ : Type} [DecidableEq Q] (M : PTM Q Γ) (w : List Γ) (n : ℕ) : ℚ

The probability that M rejects w when run for n steps with uniform random coins: numRejecting / 2^n.

def TuringMachine.PTM.decidesWithError {Q Γ : Type} [DecidableEq Q] (M : PTM Q Γ) (A : Set (List Γ)) (ε : ℚ) (t : ℕ → ℕ) : Prop

M decides the language A with error at most ε using t (|w|) coin flips on input w: if w ∈ A then M rejects w with probability ≤ ε, and if w ∉ A then M accepts w with probability ≤ ε.

def TuringMachine.PTM.runsInTime {Q Γ : Type} [DecidableEq Q] (M : PTM Q Γ) (t : ℕ → ℕ) : Prop

M runs in time t: on every input w and every coin sequence of length t (|w|), the resulting configuration is either accepting or rejecting (i.e. M has halted on every branch within t (|w|) steps).

def TuringMachine.PTM.isPolyTime {Q Γ : Type} [DecidableEq Q] (M : PTM Q Γ) : Prop

M is polynomial-time: there exist k and a runtime bound t' with t'(n) = O(n^k) such that M halts on every coin-flip branch within t'(|w|) steps.

def TuringMachine.InBPP {Γ : Type} [DecidableEq Γ] (A : Set (List Γ)) : Prop

The complexity class BPP: A ∈ BPP iff some polynomial-time PTM decides A with two-sided error ε = 1/3.

structure TuringMachine.RandomDecider (Γ : Type) [DecidableEq Γ] : Type

An abstract "random decider" over alphabet Γ: given input w and a sequence of numBits w.length random bits it returns a Boolean answer. Used as an extensional model of a randomized algorithm.

• numBits : ℕ → ℕ
• decide (w : List Γ) : (Fin (self.numBits w.length) → Bool) → Bool

def TuringMachine.RandomDecider.decidesWithBoundedError {Γ : Type} [DecidableEq Γ] (rd : RandomDecider Γ) (A : Set (List Γ)) : Prop

A RandomDecider decides A with two-sided error ≤ 1/3: for w ∈ A the fraction of random strings on which it answers false is at most 1/3, and symmetrically for w ∉ A.

def TuringMachine.RandomDecider.isPolyTime {Γ : Type} [DecidableEq Γ] (rd : RandomDecider Γ) : Prop

A RandomDecider is polynomial-time if its number of random bits is polynomially bounded in the input length.

theorem TuringMachine.InBPP_of_random_decider {Γ : Type} [DecidableEq Γ] (A : Set (List Γ)) (rd : RandomDecider Γ) (hPoly : rd.isPolyTime) (hCorrect : rd.decidesWithBoundedError A) : InBPP A

If A is decided by a polynomial-time RandomDecider with bounded error 1/3, then A ∈ BPP. This packages the abstract random-decider model into the class BPP.