A polynomial-space controller for an ordered bitstring fold

A fixed-width binary counter and an accumulator suffice. The existing initialized controller preserves the input, and SpaceIter supplies the machine and its space account. No list of all candidates is stored.

def Complexity.SpaceIter.BitstringFold.pack (done answer cursor acc : List Bool) : List Bool

Four fields: completion flag, answer flag, cursor, accumulator.

Equations

• Complexity.SpaceIter.BitstringFold.pack done answer cursor acc = Complexity.pair done (Complexity.pair answer (Complexity.pair cursor acc))

def Complexity.SpaceIter.BitstringFold.answer (s : List Bool) : List Bool

The saved verdict, read by a total pair projection.

Equations

• Complexity.SpaceIter.BitstringFold.answer s = Complexity.pairFst (Complexity.pairSnd s)

def Complexity.SpaceIter.BitstringFold.cursor (s : List Bool) : List Bool

The fixed-width candidate counter.

Equations

• Complexity.SpaceIter.BitstringFold.cursor s = Complexity.pairFst (Complexity.pairSnd (Complexity.pairSnd s))

def Complexity.SpaceIter.BitstringFold.acc (s : List Bool) : List Bool

The accumulator, which may be empty without emptying the encoded state.

Equations

• Complexity.SpaceIter.BitstringFold.acc s = Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd s))

theorem Complexity.SpaceIter.BitstringFold.pack_length (d a c v : List Bool) : (pack d a c v).length = 2 * d.length + 2 * a.length + 2 * c.length + v.length + 6

theorem Complexity.SpaceIter.BitstringFold.pack_ne_nil (d a c v : List Bool) : pack d a c v ≠ []

theorem Complexity.SpaceIter.BitstringFold.pack_head (d a : Bool) (c v x : List Bool) : (pair (pack [d] [a] c v) x).headD false = d

def Complexity.SpaceIter.BitstringFold.step (update : List Bool → List Bool → List Bool → List Bool) (accept : List Bool → List Bool → Bool) (x s : List Bool) : List Bool

Process the current candidate, or publish the saved verdict after completion.

Equations

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

theorem Complexity.SpaceIter.BitstringFold.step_running (update : List Bool → List Bool → List Bool → List Bool) (accept : List Bool → List Bool → Bool) (x c v : List Bool) (a : Bool) : step update accept x (pack [false] [a] c v) = pack [bumpOver c] [accept x (update x c v)] (bumpBits c) (update x c v)

theorem Complexity.SpaceIter.BitstringFold.step_done (update : List Bool → List Bool → List Bool → List Bool) (accept : List Bool → List Bool → Bool) (x c v : List Bool) (a : Bool) : step update accept x (pack [true] [a] c v) = pack [a] [a] c v

theorem Complexity.SpaceIter.BitstringFold.step_ne_nil (update : List Bool → List Bool → List Bool → List Bool) (accept : List Bool → List Bool → Bool) (x s : List Bool) : step update accept x s ≠ []

def Complexity.SpaceIter.BitstringFold.initial (seed : List Bool → List Bool) (accept : List Bool → List Bool → Bool) (w : Polynomial ℕ) (x : List Bool) : List Bool

Begin with the zero candidate and the supplied seed.

Equations

• Complexity.SpaceIter.BitstringFold.initial seed accept w x = Complexity.SpaceIter.BitstringFold.pack [false] [accept x (seed x)] (Complexity.polyRuler w x) (seed x)

def Complexity.SpaceIter.BitstringFold.controller (seed : List Bool → List Bool) (update : List Bool → List Bool → List Bool → List Bool) (accept : List Bool → List Bool → Bool) (w : Polynomial ℕ) : List Bool → List Bool

Preserve the original input while initializing once and then folding.

Equations

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

theorem Complexity.SpaceIter.BitstringFold.initial_ne_nil (seed : List Bool → List Bool) (accept : List Bool → List Bool → Bool) (w : Polynomial ℕ) (x : List Bool) : initial seed accept w x ≠ []

theorem Complexity.SpaceIter.BitstringFold.orbit_ne_nil (seed : List Bool → List Bool) (update : List Bool → List Bool → List Bool → List Bool) (accept : List Bool → List Bool → Bool) (w : Polynomial ℕ) (x : List Bool) (i : ℕ) : (step update accept x)^[i] (initial seed accept w x) ≠ []

theorem Complexity.SpaceIter.BitstringFold.controller_iterate (seed : List Bool → List Bool) (update : List Bool → List Bool → List Bool → List Bool) (accept : List Bool → List Bool → Bool) (w : Polynomial ℕ) (x : List Bool) (i : ℕ) : (controller seed update accept w)^[i + 1] (pair [] x) = pair ((step update accept x)^[i] (initial seed accept w x)) x

theorem Complexity.SpaceIter.BitstringFold.zero_bits (width : ℕ) : bitsOfLenLE width 0 = List.replicate width false

theorem Complexity.SpaceIter.BitstringFold.cursor_length (width i : ℕ) : (bumpBits^[i] (List.replicate width false)).length = width

theorem Complexity.SpaceIter.BitstringFold.cursor_value (width i : ℕ) (hi : i < 2 ^ width) : bumpBits^[i] (List.replicate width false) = width.toBitsLE i

theorem Complexity.SpaceIter.BitstringFold.cursor_over (width i : ℕ) (hi : i < 2 ^ width) : bumpOver (bumpBits^[i] (List.replicate width false)) = decide (i + 1 = 2 ^ width)

theorem Complexity.SpaceIter.BitstringFold.orbit (seed : List Bool → List Bool) (update : List Bool → List Bool → List Bool → List Bool) (accept : List Bool → List Bool → Bool) (w : Polynomial ℕ) (x : List Bool) (i : ℕ) : i ≤ 2 ^ Polynomial.eval x.length w → (step update accept x)^[i] (initial seed accept w x) = pack [decide (i = 2 ^ Polynomial.eval x.length w)] [accept x (bitstringFoldPrefix (update x) (seed x) (Polynomial.eval x.length w) i)] (bumpBits^[i] (polyRuler w x)) (bitstringFoldPrefix (update x) (seed x) (Polynomial.eval x.length w) i)

The ordinary orbit computes each prefix, raising its flag exactly at the endpoint.

theorem Complexity.SpaceIter.BitstringFold.orbit_final (seed : List Bool → List Bool) (update : List Bool → List Bool → List Bool → List Bool) (accept : List Bool → List Bool → Bool) (w : Polynomial ℕ) (x : List Bool) : (step update accept x)^[2 ^ Polynomial.eval x.length w + 1] (initial seed accept w x) = pack [accept x (bitstringFold (update x) (seed x) (Polynomial.eval x.length w))] [accept x (bitstringFold (update x) (seed x) (Polynomial.eval x.length w))] (bumpBits^[2 ^ Polynomial.eval x.length w] (polyRuler w x)) (bitstringFold (update x) (seed x) (Polynomial.eval x.length w))

theorem Complexity.SpaceIter.BitstringFold.pack_mem_FP {d a c v : List Bool → List Bool} (hd : d ∈ FP) (ha : a ∈ FP) (hc : c ∈ FP) (hv : v ∈ FP) : (fun (z : List Bool) => pack (d z) (a z) (c z) (v z)) ∈ FP

theorem Complexity.SpaceIter.BitstringFold.update_mem_FP {update : List Bool → List Bool → List Bool → List Bool} (hu : (fun (z : List Bool) => update (pairFst z) (pairFst (pairSnd z)) (pairSnd (pairSnd z))) ∈ FP) {x c v : List Bool → List Bool} (hx : x ∈ FP) (hc : c ∈ FP) (hv : v ∈ FP) : (fun (z : List Bool) => update (x z) (c z) (v z)) ∈ FP

theorem Complexity.SpaceIter.BitstringFold.accept_mem_FP {accept : List Bool → List Bool → Bool} (ha : (fun (z : List Bool) => [accept (pairFst z) (pairSnd z)]) ∈ FP) {x v : List Bool → List Bool} (hx : x ∈ FP) (hv : v ∈ FP) : (fun (z : List Bool) => [accept (x z) (v z)]) ∈ FP

theorem Complexity.SpaceIter.BitstringFold.step_mem_FP {update : List Bool → List Bool → List Bool → List Bool} {accept : List Bool → List Bool → Bool} (hu : (fun (z : List Bool) => update (pairFst z) (pairFst (pairSnd z)) (pairSnd (pairSnd z))) ∈ FP) (ha : (fun (z : List Bool) => [accept (pairFst z) (pairSnd z)]) ∈ FP) {x s : List Bool → List Bool} (hx : x ∈ FP) (hs : s ∈ FP) : (fun (z : List Bool) => step update accept (x z) (s z)) ∈ FP

theorem Complexity.SpaceIter.BitstringFold.controller_mem_FP {seed : List Bool → List Bool} {update : List Bool → List Bool → List Bool → List Bool} {accept : List Bool → List Bool → Bool} (w : Polynomial ℕ) (hs : seed ∈ FP) (hu : (fun (z : List Bool) => update (pairFst z) (pairFst (pairSnd z)) (pairSnd (pairSnd z))) ∈ FP) (ha : (fun (z : List Bool) => [accept (pairFst z) (pairSnd z)]) ∈ FP) : controller seed update accept w ∈ FP

theorem Complexity.SpaceIter.BitstringFold.packed_length (d a : Bool) (c v x : List Bool) : (pair (pack [d] [a] c v) x).length = 4 * c.length + 2 * v.length + x.length + 22

theorem Complexity.SpaceIter.BitstringFold.mem_PSPACE_internal {seed : List Bool → List Bool} {update : List Bool → List Bool → List Bool → List Bool} {accept : List Bool → List Bool → Bool} (w v : Polynomial ℕ) (hs : seed ∈ FP) (hu : (fun (z : List Bool) => update (pairFst z) (pairFst (pairSnd z)) (pairSnd (pairSnd z))) ∈ FP) (ha : (fun (z : List Bool) => [accept (pairFst z) (pairSnd z)]) ∈ FP) (hbound : ∀ (x : List Bool), ∀ i ≤ 2 ^ Polynomial.eval x.length w, (bitstringFoldPrefix (update x) (seed x) (Polynomial.eval x.length w) i).length ≤ Polynomial.eval x.length v) : {x : List Bool | accept x (bitstringFold (update x) (seed x) (Polynomial.eval x.length w)) = true} ∈ PSPACE

theorem Complexity.SpaceIter.BitstringFold.or_prefix_length (p : List Bool → Bool) (width i : ℕ) : (bitstringFoldPrefix (fun (c a : List Bool) => [a.headD false || p c]) [false] width i).length = 1

Boolean OR uses a one-bit accumulator, independently of the number of candidates.

theorem Complexity.SpaceIter.BitstringFold.or_prefix_iff (p : List Bool → Bool) (width i : ℕ) : (bitstringFoldPrefix (fun (c a : List Bool) => [a.headD false || p c]) [false] width i).headD false = true ↔ ∃ j < i, p (width.toBitsLE j) = true

theorem Complexity.SpaceIter.BitstringFold.or_fold_iff (p : List Bool → Bool) (width : ℕ) : (bitstringFold (fun (c a : List Bool) => [a.headD false || p c]) [false] width).headD false = true ↔ ∃ (c : List Bool), c.length = width ∧ p c = true

theorem Complexity.SpaceIter.BitstringFold.head_mem_FP {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (z : List Bool) => [(f z).headD false]) ∈ FP

theorem Complexity.SpaceIter.BitstringFold.or_eq (a : List Bool) (b : Bool) : orBit a [b] = [a.headD false || b]

theorem Complexity.SpaceIter.BitstringFold.exists_bitstring_mem_PSPACE_internal {p : List Bool → List Bool → Bool} (w : Polynomial ℕ) (hp : (fun (z : List Bool) => [p (pairFst z) (pairSnd z)]) ∈ FP) : {x : List Bool | ∃ (c : List Bool), c.length = Polynomial.eval x.length w ∧ p x c = true} ∈ PSPACE