Computing an output one bit at a time, from a language in P

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". bitwise_mem_FP in Complexitylib.Classes.P.Range turns such a description, with the bit rule given as a polynomial-time function, into f ∈ FP. This module takes the bit rule as a language in P instead.

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 results

• Complexity.bitwise_mem_FP_of_mem_P — a bitwise description with the bit rule given as a language in P, which is the form the RAM surface produces, puts the function 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

A function described bit by bit, from a language in P. This is bitwise_mem_FP with the bit rule established as a decision problem ("does position i of the output carry a one?"), which is the form in which RAM_P_eq_P delivers it.