Streaming folds of tidily computable functions #
A list encoded as the concatenation of the tokens of its elements, each read by a finite-state
input reader, can be folded in one pass over the input. The fold keeps a state, starting with
init l; for each element a it moves from the state s to next (s, a) and emits emit (s, a);
at the end it emits finish of the final state. Only the state and one element are ever held on
the work tapes.
Main definitions #
Turing.MultiTapeTM.streamState: the state of the fold after the firstjelements.Turing.MultiTapeTM.streamEmit: the words the fold emits.Turing.MultiTapeTM.rawFrameReader: a two-state input reader that reads one framed word while preserving its framing.
Main results #
Turing.MultiTapeTM.transformsTapesAt_streamLoop_encoded: a typed streaming phase, shared by single-pass and multi-pass folds.Turing.MultiTapeTM.transformsTapesAt_streamLoop_encoded_after: a typed streaming phase starting after a prefix on the input tape.Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.streamFold_sum_after: streaming folds after an initialization phase that writes the framed initial state and may move the input head past a prefix, with cumulative round costs and peak workspace bounds.Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.streamFold_sum: streaming folds with cumulative computation and copying costs, and peak workspace bounds.Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.streamFold_pair_sum: streaming folds whose input begins with a framed initial state followed by encoded stream tokens.Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.streamFold: the uniform-round corollary.
The cumulative theorem generalizes Christian Reitwiessner's original encoding-layer proof.
The typed phase shares token decoding, callback adaptation and copying bounds with multi-pass
folds. streamFold_sum_after owns the machine and its resource proof once: streamFold_sum
computes the initial state from the whole input, streamFold_pair_sum reads it from a framed
input prefix, and the uniform-round corollary reuses the complete single-pass construction.
The emitted words, round by round.
An input reader that reads one framed word [true, b₁, …, true, bₖ, false] from the input
tape while keeping its framing, stopping immediately after the closing false (including on the
empty frame [false]).
Instances For
A typed streaming phase starting after an input prefix pre.
A typed streaming phase on selected tapes. The state is framed, each token is decoded once,
and the callbacks receive the ordinary pair encoding. roundCost charges callback time and
copying of the current state, next state and decoded element. The phase leaves its final state
on tape V and the input cursor just past the last token, so another phase can consume them.
Streaming folds after an initialization phase. The input encIn x is a prefix pre x
followed by the concatenated non-empty tokens tok a of the elements elems x, from each of which
the finite-state reader r reads encA a. On any selection e of tapes, the initializer I e
starts at the start of the input on blank tapes, writes the framed initial state
frame (encS (init x)) to the selected tape e (Fin.last kI), emits nothing and moves the input
head just past pre x, in time tI x and space sI x plus one cell for each unselected tape. If
next, emit and finish are tidily computable, and g x is encoded by the words emitted by the
fold over elems x followed by finish of its final state, then g is tidily computable. The
tokens are streamed directly from the input tape, which is never copied. The time bound sums the
initialization, the actual round costs roundCost (each round's computation, current and next
states, decoded element storage and control), finalization, input scanning and cleanup. Workspace
adds the initialization's to the peak callback workspace sMax and the stored-word bound lMax;
output is emitted directly and does not count as workspace.
Streaming folds with cumulative round costs. The input x is encoded by concatenating the
non-empty tokens tok a of the elements elems x, from each of which the finite-state reader r
reads encA a. If init, next, emit and finish are tidily computable, and g x is encoded
by the words emitted by the fold over elems x followed by finish of its final state, then g
is tidily computable. The time bound sums roundCost, including each round's computation, current
and next states, decoded element storage and control. Initialization, finalization, input scanning
and cleanup are charged separately. sMax and lMax bound peak callback workspace and stored
words; output is emitted directly and does not count as workspace.
Streaming folds are tidily computable. The input x is encoded by concatenating the non-
empty tokens tok a of the elements elems x, from each of which the finite-state reader r
reads encA a. If init, next, emit and finish are tidily computable, and g x is encoded
by the words emitted by the fold over elems x followed by finish of its final state, then g
is tidily computable. Its time is linear in the input plus the rounds. Workspace uses peak bounds
on states, elements and callbacks. The bounds tMax, sMax and lMax bound the time and space
of a round and the lengths of the states and elements.
Streaming folds from a framed initial state prefix. When encIn x consists of the framed
initial state frame (encS (init x)) followed directly by the concatenated tokens of elems x
(for example, on encPair encS encBits or encPair encS encUnary), appendRead rawFrameReader V
copies the framed initial state onto tape V and leaves the input cursor at the start of the
token stream, so the tokens are streamed directly from the input tape without copying the remainder
of the input onto work tapes.