Exact counting in polynomial space

Enumerate certificates with a fixed-width binary counter and keep the number accepted in a binary accumulator. The exponentially many iterations reuse their workspace: a certificate of length m needs m cells and its acceptance count has at most m + 1 bits. This is the usual polynomial-space simulation of counting [AB09]. The interactive-proof simulation counts its accepting coins with the same counter (Cslib.Complexity.Interaction.countAccepts).

Main definitions

• Cslib.Complexity.acceptCountStep: one round of the count: test, accumulate, advance the counter.
• Cslib.Complexity.streamAcceptCount: the count obtained by running every value of the counter.

Main results

• Cslib.Complexity.streamAcceptCount_eq_acceptCount: the streaming count is acceptCount.
• Cslib.Complexity.computableInPolySpace_acceptCount: count accepted certificates of a polynomial-time unary length, with binary output.
• Cslib.Complexity.SharpP.computableInPolySpace: every #P function is computable within polynomial space, with binary output.
• Cslib.Complexity.GapP.computableInPolySpace: evaluate integer gaps in binary.

References

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

def Cslib.Complexity.acceptCountStep {α : Type} (V : α × List Bool → Bool) (s : α × List Bool × ℕ) : α × List Bool × ℕ

One round of the streaming count of the certificates that V accepts: test the current certificate, add the verdict to the accumulator and advance the binary counter.

def Cslib.Complexity.streamAcceptCount {α : Type} (V : α × List Bool → Bool) (a : α) (t : ℕ) : ℕ

The number of certificates of length t that V accepts together with a, counted by running acceptCountStep over all 2 ^ t values of a t-bit binary counter. It equals acceptCount V a t (streamAcceptCount_eq_acceptCount) and needs only the counter and the accumulator as workspace.

theorem Cslib.Complexity.streamAcceptCount_eq_acceptCount {α : Type} (V : α × List Bool → Bool) (a : α) (t : ℕ) : streamAcceptCount V a t = acceptCount V a t

The streaming count of accepted certificates is acceptCount.

theorem Cslib.Complexity.computableInPolySpace_acceptCount {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} {r : α → ℕ} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hr : Turing.MultiTapeTM.ComputableInPolyTime r enc Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolySpace (fun (a : α) => acceptCount V a (r a)) enc Turing.MultiTapeTM.encNat

Count the accepted certificates of a polynomial-time unary length in polynomial space. The result uses binary natural-number output, including when the certificate length is zero.

theorem Cslib.Complexity.SharpP.computableInPolySpace {α : Type} {enc : α ↪ List Bool} {f : α → ℕ} (hf : f ∈ SharpP enc) : Turing.MultiTapeTM.ComputableInPolySpace f enc Turing.MultiTapeTM.encNat

Every #P function is computable in polynomial space when its output is written in binary.

theorem Cslib.Complexity.GapP.computableInPolySpace {α : Type} {enc : α ↪ List Bool} {g : α → ℤ} (hg : g ∈ GapP enc) : Turing.MultiTapeTM.ComputableInPolySpace g enc Turing.MultiTapeTM.encIntBin

Every GapP function is computable in polynomial space with binary sign-magnitude output.