lemmaroutine
Elementary digit scans run in linear time
Four digit-level array rearrangements each run in time
linear-time tape toolbox for rearranging arrays
Lemma·
lem:elementary-streams·§2.1 Array order and elementary scansStatement (paper)
Fix a radix . Each of the following operations on an array of
volume takes steps on a fixed number of one-dimensional tapes:
\begin{enumerate}
\item any fixed permutation of the pair of digit values at two specified
radix- positions, whether or not the positions are adjacent;
\item moving one specified radix- digit to another position, preserving
the order of the intervening positions;
\item splitting on a specified radix- digit, applying a fixed
pointwise map to aligned streams, and merging them back;
\item for positive integers , within each prefix of an array on
, splitting
whole rows cyclically into a fixed number of streams, and, when
divides , merging those streams in any fixed order of the row classes.
\end{enumerate}
The bounds include shape preparation, counter initialization and resets,
and returning or clearing the visited portions of work tapes. Their
constants may depend on the fixed radix, the fixed pointwise map, and the
fixed number of row classes.
In plain English
For a fixed radix and an array of volume , four digit-level operations each take steps on a fixed number of one-dimensional tapes. They are permuting the digit values at two positions, moving one digit to another position, splitting on a digit with a pointwise map and merging, and cyclically splitting and merging whole rows in a array.
Why it's here
This lemma is the toolbox of linear-time tape primitives that later lemmas and claims cite for rearranging arrays without paying extra overhead. Because the bounds include shape preparation, counters and tape cleanup, later arguments can use these operations as plain steps.
Classified routine:
Standard multitape Turing machine techniques: a fixed-radix digit permutation, split or merge can be done with a constant number of linear streaming passes using counters. This follows the usual tape-model data rearrangement arguments, as in the Schönhage–Strassen and Harvey–van der Hoeven tape implementations.
Uses
Nothing else in the paper
Used by
lemAffine updates on digit fields cost linear timepropPower-width chunk interchange in O(Ve^τ)lemSwapping binary address chunks in O(Vu^τ)lemPacked XOR of selected address bitslemTensor resampling across d dimensionsclaimSplit rows cyclically into role streamsclaimExchange high digits to form row fieldclaimTop selected position by two-bit XORclaimLayout permutation by moves and chunk exchangesclaimAxis exposure costs via chunk swaps
Sources
PaperOpen
- Section
- §2.1 Array order and elementary scans
- Page
- —
- Label
lem:elementary-streams- Line
sections/02-streams.tex:60
Leannot aligned
Phase 2 aligns this node to a Lean declaration.