Quantitative streaming folds

Ordinary List.foldl expressions over raw bit strings use Christian Reitwiessner's streaming backend. A round holds the accumulator and one bit, and does not copy the input list. Time, work space and encoded accumulator size remain separate in the contract. Space counts visited work-tape cells, excluding the read-only input and write-only output; retained accumulators are charged. The invariant wrappers use the same pure prefix-fold rule, keeping their distinct resource contracts separate from invariant propagation.

Main results

• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl_bits_stream_sum: cumulative computation and copying costs, with peak workspace bounds.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl_bits_stream_sum_spec: an invariant supplies the cumulative cost and postcondition.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl_bits_pair_stream_sum: stream a paired initial accumulator and bit list (s₀, l) on encPair enc encBits with cumulative round costs and workspace independent of l.length.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl_bits_pair_stream_sum_spec: invariant wrapper for paired bit-list streaming folds.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.iterate_unary_stream_sum: stream k rounds of a state map from (s, k), emitting per round, with cumulative round costs and workspace independent of k.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl_bits_stream: the uniform-round specialization.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl_bits_stream_spec: an invariant supplies the bounds and a postcondition.
• Turing.MultiTapeTM.ComputableTidilyInO.foldl_bits_finite: a fixed finite-state fold takes linear time and constant work space, including a bound on its encoded final state.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.map_bits: a bitwise map emits its output as it scans, in linear time and zero work space.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.reverse_bits, Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.length_bits, Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.dropLast_bits, Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.getLast?_toList_bits, Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.getLast?_bits: linear-time zero-workspace bit-list reversal, unary length, prefix (List.dropLast), and last-bit (List.getLast?.toList, List.getLast?) primitives.

References

Uses Christian Reitwiessner's ComputableTidilyInTimeAndSpace.streamFold from the crei/tidy-universal branch; see the source marker in CslibFrontier/Computability/Machines/Turing/MultiTape/Encodings/StreamFold.lean.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl_bits_stream_sum {σ : Type} {enc : σ ↪ List Bool} {step : σ → Bool → σ} (init : σ) {t s : σ × Bool → ℕ} (hstep : ComputableTidilyInTimeAndSpace (fun (p : σ × Bool) => step p.1 p.2) (encPair enc encBool) enc t s) {R : List Bool → ℕ → ℕ} {Q B : List Bool → ℕ} (hcost : ∀ (l : List Bool) (i : ℕ) (hi : i < l.length), t (List.foldl step init (List.take i l), l[i]) + (enc (List.foldl step init (List.take i l))).length + (enc (List.foldl step init (List.take (i + 1) l))).length + 1 ≤ R l i) (hspace : ∀ (l : List Bool) (i : ℕ) (hi : i < l.length), s (List.foldl step init (List.take i l), l[i]) ≤ Q l) (hstate : ∀ (l : List Bool), ∀ i ≤ l.length, (enc (List.foldl step init (List.take i l))).length ≤ B l) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace (fun (l : List Bool) => List.foldl step init l) encBits enc (fun (l : List Bool) => c * (∑ i ∈ Finset.range l.length, R l i + B l + 1)) fun (l : List Bool) => c * (Q l + B l + 1)

Stream a bit list with cumulative round costs. R l i includes the step, the current and next encoded state lengths, and control. Q and B bound peak step workspace and encoded state size. The input is scanned without copying; final output and tape restoration are charged too. The constant is independent of the input, and the bounds need not be computable.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl_bits_stream {σ : Type} {enc : σ ↪ List Bool} {step : σ → Bool → σ} (init : σ) {t s : σ × Bool → ℕ} (hstep : ComputableTidilyInTimeAndSpace (fun (p : σ × Bool) => step p.1 p.2) (encPair enc encBool) enc t s) {R Q B : List Bool → ℕ} (htime : ∀ (l : List Bool) (i : ℕ) (hi : i < l.length), t (List.foldl step init (List.take i l), l[i]) ≤ R l) (hspace : ∀ (l : List Bool) (i : ℕ) (hi : i < l.length), s (List.foldl step init (List.take i l), l[i]) ≤ Q l) (hstate : ∀ (l : List Bool), ∀ i ≤ l.length, (enc (List.foldl step init (List.take i l))).length ≤ B l) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace (fun (l : List Bool) => List.foldl step init l) encBits enc (fun (l : List Bool) => c * (l.length * (R l + B l + 1) + B l + 1)) fun (l : List Bool) => c * (Q l + B l + 1)

Stream a bit list through a tidy step computation. Each round charges the step and the stored state, without copying the input list. R, Q and B bound the time of a round, its work space and the encoded state size, respectively. The final output and tape restoration are charged too. The constant is independent of the input; the three bounds need not be computable.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl_bits_stream_sum_spec {σ : Type} {enc : σ ↪ List Bool} {step : σ → Bool → σ} (init : σ) {t s : σ × Bool → ℕ} (hstep : ComputableTidilyInTimeAndSpace (fun (p : σ × Bool) => step p.1 p.2) (encPair enc encBool) enc t s) (invariant : List Bool → ℕ → σ → Prop) (hbase : ∀ (l : List Bool), invariant l 0 init) (hpreserve : ∀ (l : List Bool) (i : ℕ) (hi : i < l.length) (state : σ), invariant l i state → invariant l (i + 1) (step state l[i])) {R : List Bool → ℕ → ℕ} {Q B : List Bool → ℕ} (hcost : ∀ (l : List Bool) (i : ℕ) (hi : i < l.length) (state : σ), invariant l i state → t (state, l[i]) + (enc state).length + (enc (step state l[i])).length + 1 ≤ R l i ∧ s (state, l[i]) ≤ Q l) (hsize : ∀ (l : List Bool), ∀ i ≤ l.length, ∀ (state : σ), invariant l i state → (enc state).length ≤ B l) : (∃ (c : ℕ), ComputableTidilyInTimeAndSpace (fun (l : List Bool) => List.foldl step init l) encBits enc (fun (l : List Bool) => c * (∑ i ∈ Finset.range l.length, R l i + B l + 1)) fun (l : List Bool) => c * (Q l + B l + 1)) ∧ ∀ (l : List Bool), invariant l l.length (List.foldl step init l)

An invariant supplies cumulative computation and copying costs, peak workspace and a postcondition. Each round's bound includes both the old and the new encoded state.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl_bits_stream_spec {σ : Type} {enc : σ ↪ List Bool} {step : σ → Bool → σ} (init : σ) {t s : σ × Bool → ℕ} (hstep : ComputableTidilyInTimeAndSpace (fun (p : σ × Bool) => step p.1 p.2) (encPair enc encBool) enc t s) (invariant : List Bool → ℕ → σ → Prop) (hbase : ∀ (l : List Bool), invariant l 0 init) (hpreserve : ∀ (l : List Bool) (i : ℕ) (hi : i < l.length) (state : σ), invariant l i state → invariant l (i + 1) (step state l[i])) {R Q B : List Bool → ℕ} (hcost : ∀ (l : List Bool) (i : ℕ) (hi : i < l.length) (state : σ), invariant l i state → t (state, l[i]) ≤ R l ∧ s (state, l[i]) ≤ Q l) (hsize : ∀ (l : List Bool), ∀ i ≤ l.length, ∀ (state : σ), invariant l i state → (enc state).length ≤ B l) : (∃ (c : ℕ), ComputableTidilyInTimeAndSpace (fun (l : List Bool) => List.foldl step init l) encBits enc (fun (l : List Bool) => c * (l.length * (R l + B l + 1) + B l + 1)) fun (l : List Bool) => c * (Q l + B l + 1)) ∧ ∀ (l : List Bool), invariant l l.length (List.foldl step init l)

An invariant supplies the streaming fold's resource bounds and postcondition.

theorem Turing.MultiTapeTM.ComputableTidilyInO.foldl_bits_finite {σ : Type} [Finite σ] (enc : σ ↪ List Bool) (step : σ → Bool → σ) (init : σ) : ComputableTidilyInO (fun (l : List Bool) => List.foldl step init l) encBits enc List.length fun (x : List Bool) => 0

A fold with a fixed finite state type takes linear time and constant work space. The constant may depend on the state type, its encoding and the transition function; this is not a uniform bound for a family of growing state types. The encoded final state is bounded as well.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.map_bits (f : Bool → Bool) : ComputableTidilyInTimeAndSpace (List.map f) encBits encBits (fun (l : List Bool) => 4 * l.length + 8) fun (x : List Bool) => 0

Emit a bitwise map directly, without a growing accumulator on a work tape. Unlike InO, this numerical certificate does not include the emitted output in its space bound.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl_bits_pair_stream_sum {σ : Type} {enc : σ ↪ List Bool} {step : σ → Bool → σ} {t s : σ × Bool → ℕ} (hstep : ComputableTidilyInTimeAndSpace (fun (p : σ × Bool) => step p.1 p.2) (encPair enc encBool) enc t s) {R : σ × List Bool → ℕ → ℕ} {Q B : σ × List Bool → ℕ} (hcost : ∀ (p : σ × List Bool) (i : ℕ) (hi : i < p.2.length), t (List.foldl step p.1 (List.take i p.2), p.2[i]) + (enc (List.foldl step p.1 (List.take i p.2))).length + (enc (List.foldl step p.1 (List.take (i + 1) p.2))).length + 1 ≤ R p i) (hspace : ∀ (p : σ × List Bool) (i : ℕ) (hi : i < p.2.length), s (List.foldl step p.1 (List.take i p.2), p.2[i]) ≤ Q p) (hstate : ∀ (p : σ × List Bool), ∀ i ≤ p.2.length, (enc (List.foldl step p.1 (List.take i p.2))).length ≤ B p) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace (fun (p : σ × List Bool) => List.foldl step p.1 p.2) (encPair enc encBits) enc (fun (p : σ × List Bool) => c * (∑ i ∈ Finset.range p.2.length, R p i + B p + 1)) fun (p : σ × List Bool) => c * (Q p + B p + 1)

Stream a paired initial accumulator and bit list (s₀, l) on encPair enc encBits with cumulative round costs. The framed initial accumulator frame (enc s₀) is copied once to the state tape by rawFrameReader, and the remaining bits l are streamed directly from the input tape without copying l onto work tapes, so workspace depends only on peak step workspace Q and peak encoded accumulator length B.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl_bits_pair_stream_sum_spec {σ : Type} {enc : σ ↪ List Bool} {step : σ → Bool → σ} {t s : σ × Bool → ℕ} (hstep : ComputableTidilyInTimeAndSpace (fun (p : σ × Bool) => step p.1 p.2) (encPair enc encBool) enc t s) (invariant : σ × List Bool → ℕ → σ → Prop) (hbase : ∀ (p : σ × List Bool), invariant p 0 p.1) (hpreserve : ∀ (p : σ × List Bool) (i : ℕ) (hi : i < p.2.length) (state : σ), invariant p i state → invariant p (i + 1) (step state p.2[i])) {R : σ × List Bool → ℕ → ℕ} {Q B : σ × List Bool → ℕ} (hcost : ∀ (p : σ × List Bool) (i : ℕ) (hi : i < p.2.length) (state : σ), invariant p i state → t (state, p.2[i]) + (enc state).length + (enc (step state p.2[i])).length + 1 ≤ R p i ∧ s (state, p.2[i]) ≤ Q p) (hsize : ∀ (p : σ × List Bool), ∀ i ≤ p.2.length, ∀ (state : σ), invariant p i state → (enc state).length ≤ B p) : (∃ (c : ℕ), ComputableTidilyInTimeAndSpace (fun (p : σ × List Bool) => List.foldl step p.1 p.2) (encPair enc encBits) enc (fun (p : σ × List Bool) => c * (∑ i ∈ Finset.range p.2.length, R p i + B p + 1)) fun (p : σ × List Bool) => c * (Q p + B p + 1)) ∧ ∀ (p : σ × List Bool), invariant p p.2.length (List.foldl step p.1 p.2)

An invariant supplies cumulative computation and copying costs, peak workspace, and a postcondition for a paired streaming fold over (s₀, l) : σ × List Bool.

theorem Turing.MultiTapeTM.streamState_replicate {σ : Type u_1} {α : Type u_2} (f : σ → σ) (s : σ) (a : α) {k j : ℕ} (hj : j ≤ k) : streamState s (fun (p : σ × α) => f p.1) (List.replicate k a) j = f^[j] s

A fold whose step ignores its token iterates the state map, j times after j tokens.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.iterate_unary_stream_sum {σ : Type} {enc : σ ↪ List Bool} {f : σ → σ} {emit finish : σ → List Bool} {tN sN tE sE tF sF : σ → ℕ} (hnext : ComputableTidilyInTimeAndSpace f enc enc tN sN) (hemit : ComputableTidilyInTimeAndSpace emit enc encBits tE sE) (hfinish : ComputableTidilyInTimeAndSpace finish enc encBits tF sF) {R : σ × ℕ → ℕ → ℕ} {Q B : σ × ℕ → ℕ} (hcost : ∀ (x : σ × ℕ), ∀ i < x.2, tN (f^[i] x.1) + tE (f^[i] x.1) + (enc (f^[i] x.1)).length + (enc (f^[i + 1] x.1)).length + 1 ≤ R x i) (hspace : ∀ (x : σ × ℕ), ∀ i < x.2, sN (f^[i] x.1) + sE (f^[i] x.1) ≤ Q x) (hstate : ∀ (x : σ × ℕ), ∀ i ≤ x.2, (enc (f^[i] x.1)).length ≤ B x) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace (fun (x : σ × ℕ) => (List.map (fun (i : ℕ) => emit (f^[i] x.1)) (List.range x.2)).flatten ++ finish (f^[x.2] x.1)) (encPair enc encUnary) encBits (fun (x : σ × ℕ) => c * (tF (f^[x.2] x.1) + ∑ i ∈ Finset.range x.2, R x i + B x + 1)) fun (x : σ × ℕ) => c * (sF (f^[x.2] x.1) + Q x + B x + 1)

Stream k rounds of a state map f from (s, k) on encPair enc encUnary. Round i emits emit (f^[i] s) directly to the output, and the final state is finished by finish. The unary count is read from the input tape one bit per round and never copied, so workspace holds only the current state and the callbacks. R x i charges round i: the step, the emission, and the current and next encoded states; Q and B bound peak callback workspace and encoded state size.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.reverse_bits : ComputableTidilyInTimeAndSpace List.reverse encBits encBits (fun (l : List Bool) => 2 * l.length + 2) fun (x : List Bool) => 0

Reverse a bit list tidily in 2 * l.length + 2 steps and zero work-tape space, using the two-state zero-work-tape primitive Turing.MultiTapeTM.reverseInput.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.length_bits : ComputableTidilyInTimeAndSpace List.length encBits encUnary (fun (l : List Bool) => 4 * l.length + 8) fun (x : List Bool) => 0

The length of a bit list, emitted in unary while scanning, in 4 * l.length + 8 steps and zero work-tape space.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.dropLast_bits : ComputableTidilyInTimeAndSpace List.dropLast encBits encBits (fun (l : List Bool) => 4 * l.length + 8) fun (x : List Bool) => 0

Drop the last bit of a bit list (List.dropLast) tidily in 4 * l.length + 8 steps and zero work-tape space, using a three-state (Option Bool) finite-state transducer that buffers one lookahead symbol.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.getLast?_toList_bits : ComputableTidilyInTimeAndSpace (fun (l : List Bool) => l.getLast?.toList) encBits encBits (fun (l : List Bool) => 4 * l.length + 8) fun (x : List Bool) => 0

Extract the last bit of a bit list as a 0-or-1-element list (l.getLast?.toList) tidily in 4 * l.length + 8 steps and zero work-tape space.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.getLast?_bits : ComputableTidilyInTimeAndSpace List.getLast? encBits (encOption encBool) (fun (l : List Bool) => 4 * l.length + 8) fun (x : List Bool) => 0

Extract the last bit of a bit list as an Option Bool (l.getLast?) tidily in 4 * l.length + 8 steps and zero work-tape space.