Counting the accepting coins in polynomial space

This file computes, for a verifier machine, the number of coin values whose programs accept after a history (Cslib.Complexity.Interaction.accepted), within space polynomial in the input and the history, and in exponential time.

• A replay keeping only whether it is still live (Cslib.Complexity.Interaction.aliveStep) decides whether the program of given coins accepts after a history (Cslib.Complexity.Interaction.accepts_eq_true_iff), in polynomial time (Cslib.Complexity.Interaction.computableInPolyTime_accepts): it folds one instruction per coin over the configuration of the machine, whose storage grows by a bounded amount per instruction.
• The coin values are enumerated by the binary counter of the shared streaming count Cslib.Complexity.streamAcceptCount, and the accepting ones are counted with a binary accumulator (Cslib.Complexity.Interaction.countAccepts, Cslib.Complexity.Interaction.countAccepts_eq_accepted), within polynomial space (Turing.MultiTapeTM.ComputableInPolySpace, Cslib.Complexity.Interaction.computableInPolySpace_countAccepts).

Main definitions

• Cslib.Complexity.Interaction.accepts: whether the program of given coins accepts.
• Cslib.Complexity.Interaction.countAccepts: the number of accepting coin values.

Main results

• Cslib.Complexity.Interaction.computableInPolyTime_accepts: acceptance in polynomial time.
• Cslib.Complexity.Interaction.countAccepts_eq_accepted: the count of accepting coin values.
• Cslib.Complexity.Interaction.computableInPolySpace_countAccepts: the count in polynomial space.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

A live replay

@[reducible, inline]

abbrev Cslib.Complexity.Interaction.encHistory : History ↪ List Bool

Histories, encoded as lists of pairs of words.

@[reducible, inline]

abbrev Cslib.Complexity.Interaction.AliveState (k : ℕ) (Control Operation Entry : Type) : Type

The state of a replay that only records whether it is still live: the configuration, the rest of the history and liveness.

def Cslib.Complexity.Interaction.instruction {k : ℕ} {Control Operation : Type} (M : Turing.MultiTapePTM k Bool Control Operation) (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control Operation) (b : Bool) : Option (Turing.MultiTapeMachine.Action k Bool Control Operation)

The instruction of M in the configuration cfg with the coin b, unless it has halted.

def Cslib.Complexity.Interaction.answerFromHistory {k : ℕ} {Control Operation Entry : Type} [DecidableEq Operation] [Inhabited Entry] (matchOp : Operation → Entry → Bool) (entryPair : Entry → List Bool × List Bool) (t : ℕ) (op : Operation) (next : Control) (s : AliveState k Control Operation Entry) : AliveState k Control Operation Entry

Answer a request on the channel op from the history, moving to the control state next, or stop when the history is exhausted or sends another message.

def Cslib.Complexity.Interaction.taggedStep {k : ℕ} {Control Operation Entry : Type} [DecidableEq Operation] [Inhabited Entry] (matchOp : Operation → Entry → Bool) (entryPair : Entry → List Bool × List Bool) (t : ℕ) : Bool × Option (Turing.MultiTapeMachine.Action k Bool Control Operation) → AliveState k Control Operation Entry → AliveState k Control Operation Entry

The live replay step by its liveness and instruction.

def Cslib.Complexity.Interaction.aliveStep {k : ℕ} {Control Operation Entry : Type} [DecidableEq Operation] [Inhabited Entry] (matchOp : Operation → Entry → Bool) (entryPair : Entry → List Bool × List Bool) (M : Turing.MultiTapePTM k Bool Control Operation) (t : ℕ) (s : AliveState k Control Operation Entry) (b : Bool) : AliveState k Control Operation Entry

One instruction of a live replay: taggedStep dispatched by liveness and instruction.

def Cslib.Complexity.Interaction.aliveRun {k : ℕ} {Control Operation Entry : Type} [DecidableEq Operation] [Inhabited Entry] (matchOp : Operation → Entry → Bool) (entryPair : Entry → List Bool × List Bool) (M : Turing.MultiTapePTM k Bool Control Operation) (x r : List Bool) (h : List Entry) : AliveState k Control Operation Entry

The live replay of M on the input x with the coins r against the history h, its replies truncated to the number of coins.

def Cslib.Complexity.Interaction.accepts {k : ℕ} {Control Operation Entry : Type} [DecidableEq Operation] [Inhabited Entry] (matchOp : Operation → Entry → Bool) (entryPair : Entry → List Bool × List Bool) (M : Turing.MultiTapePTM k Bool Control Operation) (x r : List Bool) (h : List Entry) : Bool

Whether the program of the coins r accepts after the history h: the replay is live, has consumed the whole history and has output [true].

theorem Cslib.Complexity.Interaction.aliveStep_of_false {k : ℕ} {Control Operation Entry : Type} [DecidableEq Operation] [Inhabited Entry] (matchOp : Operation → Entry → Bool) (entryPair : Entry → List Bool × List Bool) (M : Turing.MultiTapePTM k Bool Control Operation) (t : ℕ) (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control Operation) (h : List Entry) (b : Bool) : aliveStep matchOp entryPair M t (cfg, h, false) b = (cfg, h, false)

theorem Cslib.Complexity.Interaction.foldl_aliveStep_false {k : ℕ} {Control Operation Entry : Type} [DecidableEq Operation] [Inhabited Entry] (matchOp : Operation → Entry → Bool) (entryPair : Entry → List Bool × List Bool) (M : Turing.MultiTapePTM k Bool Control Operation) (t : ℕ) (l : List Bool) (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control Operation) (h : List Entry) : List.foldl (aliveStep matchOp entryPair M t) (cfg, h, false) l = (cfg, h, false)

theorem Cslib.Complexity.Interaction.aliveRun_of_simulate_ok {k : ℕ} {Control : Type} (MUnit : Turing.MultiTapePTM k Bool Control Unit) {x r : List Bool} {h : History} {p : Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit × History} (hsim : simulate MUnit r.length x r h = Except.ok p) : aliveRun (fun (x : Unit) (x_1 : List Bool × List Bool) => true) id MUnit x r h = (p.1, p.2, true)

When the replay succeeds on x, r, h, the live replay stops at the same state and stays live.

theorem Cslib.Complexity.Interaction.aliveRun_of_simulate_error_some {k : ℕ} {Control : Type} (MUnit : Turing.MultiTapePTM k Bool Control Unit) {x r : List Bool} {h : History} {m : List Bool} (hsim : simulate MUnit r.length x r h = Except.error (some m)) : ∃ (cfg : Turing.MultiTapeMachine.FiniteConfig k Bool Control Unit) (rem : List (List Bool × List Bool)), aliveRun (fun (x : Unit) (x_1 : List Bool × List Bool) => true) id MUnit x r h = (cfg, rem, false) ∧ (cfg.channels ()).1 = m

When the replay pauses waiting for a reply to m, the live replay stops inactive with m on channel ().

theorem Cslib.Complexity.Interaction.accepts_eq_true_iff {k : ℕ} {Control : Type} (MUnit : Turing.MultiTapePTM k Bool Control Unit) (x r : List Bool) (h : History) : accepts (fun (x : Unit) (x_1 : List Bool × List Bool) => true) id MUnit x r h = true ↔ outcome (coinProgram MUnit r.length x r) h = Outcome.done true

The live replay decides acceptance: accepts holds exactly when the program of the coins accepts after the history.

The live replay in polynomial time

@[reducible, inline]

noncomputable abbrev Cslib.Complexity.Interaction.encAliveState {k : ℕ} {Control Operation Entry : Type} [Finite Control] [Fintype Operation] (encEntry : Entry ↪ List Bool) : AliveState k Control Operation Entry ↪ List Bool

Live replay states, encoded by their fields.

theorem Cslib.Complexity.Interaction.computableInPolyTime_instruction {k : ℕ} {Control Operation : Type} (M : Turing.MultiTapePTM k Bool Control Operation) [Finite Control] [Fintype Operation] : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Turing.MultiTapeMachine.FiniteConfig k Bool Control Operation × Bool) => instruction M p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encFiniteConfig Turing.MultiTapeTM.encBool) (Turing.MultiTapeTM.encFinite (Option (Turing.MultiTapeMachine.Action k Bool Control Operation)))

The instruction is polynomial-time: it reads finitely many observations.

theorem Cslib.Complexity.Interaction.computableInPolyTime_aliveRun {k : ℕ} {Control Operation Entry : Type} [DecidableEq Operation] [Inhabited Entry] (matchOp : Operation → Entry → Bool) (entryPair : Entry → List Bool × List Bool) (M : Turing.MultiTapePTM k Bool Control Operation) [Finite Control] [Fintype Operation] {encEntry : Entry ↪ List Bool} (hmatch : ∀ (op : Operation), Turing.MultiTapeTM.ComputableInPolyTime (matchOp op) encEntry Turing.MultiTapeTM.encBool) (hpair : Turing.MultiTapeTM.ComputableInPolyTime entryPair encEntry (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool × List Entry) => aliveRun matchOp entryPair M p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList encEntry))) (encAliveState encEntry)

The live replay is polynomial-time in the input, the coins and the history.

theorem Cslib.Complexity.Interaction.computableInPolyTime_accepts {k : ℕ} {Control Operation Entry : Type} [DecidableEq Operation] [Inhabited Entry] (matchOp : Operation → Entry → Bool) (entryPair : Entry → List Bool × List Bool) (M : Turing.MultiTapePTM k Bool Control Operation) [Finite Control] {encEntry : Entry ↪ List Bool} (hmatch : ∀ (op : Operation), Turing.MultiTapeTM.ComputableInPolyTime (matchOp op) encEntry Turing.MultiTapeTM.encBool) (hpair : Turing.MultiTapeTM.ComputableInPolyTime entryPair encEntry (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) [Finite Operation] : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool × List Entry) => accepts matchOp entryPair M p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList encEntry))) Turing.MultiTapeTM.encBool

Acceptance is polynomial-time in the input, the coins and the history.

Counting the accepting coins

def Cslib.Complexity.Interaction.countAccepts {k : ℕ} {Control α : Type} (MUnit : Turing.MultiTapePTM k Bool Control Unit) (enc : α ↪ List Bool) (fuel : α → ℕ) (q : α × History) : ℕ

The number of accepting values of fuel a coins after the history h, counted by trying the coins one after another with a binary counter (Cslib.Complexity.streamAcceptCount).

theorem Cslib.Complexity.Interaction.countAccepts_eq_accepted {k : ℕ} {Control α : Type} (MUnit : Turing.MultiTapePTM k Bool Control Unit) (enc : α ↪ List Bool) (fuel : α → ℕ) (q : α × History) : countAccepts MUnit enc fuel q = accepted (coinFamily MUnit (fuel q.1) (enc q.1)) q.2

The count of accepting coins: countAccepts is the number of coin values of fuel a coins whose programs accept after the history.

theorem Cslib.Complexity.Interaction.computableInPolySpace_countAccepts {k : ℕ} {Control α : Type} (MUnit : Turing.MultiTapePTM k Bool Control Unit) (enc : α ↪ List Bool) (fuel : α → ℕ) [Finite Control] (hfuel : Turing.MultiTapeTM.ComputableInPolyTime fuel enc Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolySpace (countAccepts MUnit enc fuel) (Turing.MultiTapeTM.encPair enc encHistory) Turing.MultiTapeTM.encNat

The count of accepting coins within polynomial space, in the input and the history, for a number of coins computed in polynomial time.