Computing an output one bit at a time

A polynomial-time function is usually easiest to describe not as a string transformation but as a rule for each output bit: "the i-th bit of f x is whatever this decision procedure says". This module turns such a description into f ∈ FP.

The two inputs are a unary length function — how long the output is, given in unary so that it is itself a plausible FP output — and a bit oracle, a polynomial-time function reading pair x (unary i) and returning the single bit. The construction is an iteration of an append-one-bit step, run once per output position, and iterate_mem_FP supplies the closure of FP under such iterations.

This is the bridge that lets a decision procedure written on the RAM surface (where RAM_P_eq_P transfers it to P) be used to build a function in FP, for which no direct RAM bridge exists.

Main definitions

• Complexity.bitStep — the append-one-bit step

Main results

• Complexity.bitwise_mem_FP — a bitwise description puts the function in FP
• Complexity.bitwise_mem_FP_of_mem_P — the same with the bit rule given as a language in P, which is the form the RAM surface produces

def Complexity.bitStep (G : List Bool → List Bool) (z : List Bool) : List Bool

One step of the construction: consult the oracle at the current output length and append the bit it returns. The state is pair (output so far) input.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.bitStep_mem_FP {G : List Bool → List Bool} (hG : G ∈ FP) : bitStep G ∈ FP

theorem Complexity.bitStep_iterate {G : List Bool → List Bool} {b : List Bool → ℕ → Bool} (hGspec : ∀ (x : List Bool) (i : ℕ), G (pair x (List.replicate i true)) = [b x i]) (x : List Bool) (n : ℕ) : (bitStep G)^[n] (pair [] x) = pair (List.map (b x) (List.range n)) x

Running the step from the empty output builds the first n bits.

theorem Complexity.bitwise_mem_FP {len : List Bool → ℕ} {b : List Bool → ℕ → Bool} (hlen : (fun (x : List Bool) => List.replicate (len x) true) ∈ FP) {G : List Bool → List Bool} (hG : G ∈ FP) (hGspec : ∀ (x : List Bool) (i : ℕ), G (pair x (List.replicate i true)) = [b x i]) : (fun (x : List Bool) => List.map (b x) (List.range (len x))) ∈ FP

A function described bit by bit is polynomial time. If the output length is computable in unary and each output bit is computable from the input and the position in unary, the function itself is in FP.

theorem Complexity.bitwise_mem_FP_of_mem_P {len : List Bool → ℕ} {b : List Bool → ℕ → Bool} (hlen : (fun (x : List Bool) => List.replicate (len x) true) ∈ FP) {L : Language} (hL : L ∈ P) (hLspec : ∀ (x : List Bool) (i : ℕ), pair x (List.replicate i true) ∈ L ↔ b x i = true) : (fun (x : List Bool) => List.map (b x) (List.range (len x))) ∈ FP

The same, from a language in P. The bit rule is usually established as a decision problem — "does position i of the output carry a one?" — and this is the form in which RAM_P_eq_P delivers it.