174 Complexity — Sweep
174.1 Overview
This module provides the generic zipper/transduction layer behind sweep-based tape simulations (the infrastructure for Arora–Barak’s Claim 1.6): a finite window of a work tape represented as two stacks around a frontier, scanned in either direction; exact-cost lemmas showing that a local transition rule realizes a complete forward or backward sweep as a finite-state transduction; table-valued (indexed) transducers that update one entry per visited cell; and a bound confining an initialized run’s work heads and nonblank cells to the elapsed-time interval.
174.2 Declarations
Given an integer frontier coordinate \(z\) and two finite lists \(l\) and \(r\) of possibly-blank symbols over an alphabet \(A\), this defines the tape content \(\mathbb {Z} \to A \cup \{ \text{blank}\} \) that stores the cells strictly to the left of \(z\) in \(l\) (nearest cell first) and the cells at \(z\) and to its right in \(r\) (in order); every position beyond the extent of either list reads as blank.
Let \(z\) be an integer and let \(l\) and \(r\) be finite lists of possibly-blank symbols over an alphabet \(A\). The two-stack zipper tape with frontier \(z\), left stack \(l\), and right stack \(r\) reads, at position \(z\), exactly the first entry of \(r\) — or blank when \(r\) is empty.
Let \(z\) be an integer, let \(l\) and \(r\) be finite lists of possibly-blank symbols over an alphabet \(A\), and let \(a\), \(b\) be possibly-blank symbols. Overwriting position \(z\) with \(b\) in the two-stack zipper tape with frontier \(z\), left stack \(l\), and right stack \(a \mathbin {::} r\) yields exactly the zipper tape with frontier \(z + 1\), left stack \(b \mathbin {::} l\), and right stack \(r\): the written cell transfers from the right stack to the left stack.
Given an optional machine state \(q\), an input-head position \(p\), an integer frontier \(z\), two zipper stacks \(l\) and \(r\) of possibly-blank symbols, and an output word, this defines the configuration of a one-work-tape Turing machine whose work tape is the two-stack zipper with frontier \(z\), left stack \(l\), and right stack \(r\), whose work head sits at \(z\), and whose input-head position and output are the given ones.
For a machine state \(q\), a possibly-blank symbol \(a\), and a direction \(d\), this defines the one-work-tape machine action that overwrites the scanned work-tape cell with \(a\), moves the work head one step in direction \(d\), leaves the input head stationary, appends nothing to the output, and passes to state \(q\).
Consider the forward-sweep configuration of a one-work-tape machine with (optional) state \(q\), input-head position \(p\), frontier \(z\), left stack \(l\), right stack \(a \mathbin {::} r\), and output word \(\mathit{out}\). Applying to it the local sweep action that writes the possibly-blank symbol \(b\), moves the work head right, and enters state \(q'\) produces exactly the forward-sweep configuration with state \(q'\), the same input-head position \(p\) and output \(\mathit{out}\), frontier \(z + 1\), left stack \(b \mathbin {::} l\), and right stack \(r\).
Given a local rule \(\mathit{visit} \colon R \times C \to R \times C\) mapping a control state and a cell to a new state and a rewritten cell, and an initial state \(s\), this defines the left-to-right transduction of a word over \(C\): the word is processed cell by cell, each cell being rewritten by \(\mathit{visit}\) while the control state is threaded through, and the result records both the final control state and the fully rewritten word.
Let \(M\) be a one-work-tape Turing machine over alphabet \(A\) with states \(S\), and let controller states \(R\) and controller cells \(C\) be encoded into \(S\) and \(A\) by maps \(\mathit{state}\) and \(\mathit{symbol}\). Suppose a local rule \(\mathit{visit} \colon R \times C \to R \times C\) is implemented by \(M\)’s transition table: whenever \(M\) is in state \(\mathit{state}(s)\) and its work head reads \(\mathit{symbol}(a)\) (for any input symbol), its transition is the local sweep action that writes the encoding of the rewritten cell, moves right, and enters the encoding of the new controller state. Then, starting from the forward-sweep configuration with state \(\mathit{state}(s)\), frontier \(z\), left stack \(l\), and right stack consisting of the encoded word \(\mathit{as}\) followed by \(r\), running \(M\) for exactly \(|\mathit{as}|\) steps reaches the forward-sweep configuration whose state encodes the final controller state of the transduction of \(\mathit{as}\), whose frontier is \(z + |\mathit{as}|\), and whose left stack is the encoded rewritten word, reversed, prepended to \(l\), with right stack \(r\); the input-head position and the output word are unchanged.
Given an optional machine state \(q\), an input-head position \(p\), an integer frontier \(z\), two zipper stacks \(l\) and \(r\) of possibly-blank symbols, and an output word, this defines the configuration of a one-work-tape Turing machine whose work head sits at \(z\) and whose work tape is the coordinate reflection of the two-stack zipper: the cell at coordinate \(w\) is the zipper tape with frontier \(-z\), left stack \(l\), and right stack \(r\), read at \(-w\). Thus \(r\) stores the cells at the frontier and to its left (in scanning order toward decreasing coordinates) and \(l\) stores the cells strictly to the right.
Consider the backward-sweep configuration of a one-work-tape machine with (optional) state \(q\), input-head position \(p\), frontier \(z\), left stack \(l\), right stack \(a \mathbin {::} r\), and output word \(\mathit{out}\). Applying to it the local sweep action that writes the possibly-blank symbol \(b\), moves the work head left, and enters state \(q'\) produces exactly the backward-sweep configuration with state \(q'\), the same input-head position \(p\) and output \(\mathit{out}\), frontier \(z - 1\), left stack \(b \mathbin {::} l\), and right stack \(r\).
Let \(M\) be a one-work-tape Turing machine over alphabet \(A\) with states \(S\), and let controller states \(R\) and controller cells \(C\) be encoded into \(S\) and \(A\) by maps \(\mathit{state}\) and \(\mathit{symbol}\). Suppose a local rule \(\mathit{visit} \colon R \times C \to R \times C\) is implemented by \(M\)’s transition table: whenever \(M\) is in state \(\mathit{state}(s)\) and its work head reads \(\mathit{symbol}(a)\) (for any input symbol), its transition is the local sweep action that writes the encoding of the rewritten cell, moves left, and enters the encoding of the new controller state. Then, starting from the backward-sweep configuration with state \(\mathit{state}(s)\), frontier \(z\), left stack \(l\), and right stack consisting of the encoded word \(\mathit{as}\) followed by \(r\), running \(M\) for exactly \(|\mathit{as}|\) steps reaches the backward-sweep configuration whose state encodes the final controller state of the transduction of \(\mathit{as}\), whose frontier is \(z - |\mathit{as}|\), and whose left stack is the encoded rewritten word, reversed, prepended to \(l\), with right stack \(r\); the input-head position and the output word are unchanged.
Let \(z\) be an integer and let \(l\) and \(r\) be finite lists of possibly-blank symbols over an alphabet \(A\). The two-stack zipper tape with frontier \(z\), left stack \(l\), and right stack \(r\) coincides, as a function on \(\mathbb {Z}\), with the coordinate reflection \(w \mapsto \) (zipper tape with frontier \(-(z - 1)\), left stack \(r\), and right stack \(l\), read at \(-w\)): reversing the scanning direction exchanges the two stacks.
Let \(\mathit{visit} \colon R \times C \to R \times C\) be a local rule, \(s\) an initial control state, and \(\mathit{as}\), \(\mathit{bs}\) two words over \(C\). The finite-state transduction of the concatenation \(\mathit{as} \mathbin {+\! \! +} \mathit{bs}\) starting from \(s\) is obtained by transducing \(\mathit{as}\) from \(s\), then transducing \(\mathit{bs}\) from the resulting control state: the final state is that of the second transduction, and the rewritten word is the concatenation of the two rewritten words.
Given a family of local rules \(\mathit{visit}_i \colon V \times C \to V \times C\) indexed by a type \(I\) with decidable equality, this defines a transducer whose control state is a table \(s \colon I \to V\) and whose cells are index-tagged pairs \((i, c)\): on such a pair it applies \(\mathit{visit}_i\) to the table entry \(s(i)\) and the cell \(c\), updates the table at \(i\) to the new value, and outputs \(i\) tagged with the rewritten cell. Only the entry named by the visited cell changes.
Let \(\mathit{visit}_i \colon V \times C \to V \times C\) be a family of local rules indexed by a type \(I\) with decidable equality, let \(\mathit{cell} \colon I \to C\) assign a cell to each index, and let \(\mathit{is}\) be a list of indices with no duplicates. Transducing, with the table-valued indexed transducer started at table \(s\), the block that lists each \(i \in \mathit{is}\) tagged with \(\mathit{cell}(i)\), yields: the table that at every index \(i\) occurring in \(\mathit{is}\) holds the new value of \(\mathit{visit}_i\) applied to the original entry \(s(i)\) and \(\mathit{cell}(i)\), and elsewhere agrees with \(s\); together with the block in which each tagged cell is replaced by its rewritten value, likewise computed from the original table. Because no index repeats, each local rule sees the untouched table entry.
Let \(k \in \mathbb {N}\), let \(\mathit{visit}_i \colon V \times C \to V \times C\) be a family of local rules indexed by \(i \in \{ 0, \dots , k-1\} \), let \(\mathit{cell}\) assign a cell to each index, and let \(s\) be an initial table. Transducing, with the table-valued indexed transducer started at \(s\), the block listing every index \(i\) exactly once in increasing order tagged with \(\mathit{cell}(i)\), yields the table \(i \mapsto \) (new value of \(\mathit{visit}_i\) on \(s(i)\) and \(\mathit{cell}(i)\)) together with the block of rewritten tagged cells in the same order.
Let \(k \in \mathbb {N}\), let \(\mathit{visit}_i \colon V \times C \to V \times C\) be a family of local rules indexed by \(i \in \{ 0, \dots , k-1\} \), let \(\mathit{cell}\) assign a cell to each index, and let \(s\) be an initial table. Transducing, with the table-valued indexed transducer started at \(s\), the block listing every index exactly once in decreasing order tagged with its cell, yields the table \(i \mapsto \) (new value of \(\mathit{visit}_i\) on \(s(i)\) and \(\mathit{cell}(i)\)) together with the correspondingly reversed block of rewritten tagged cells.
Let \(z\) be an integer and \(l\) a finite list of possibly-blank symbols over an alphabet \(A\). The two-stack zipper tape with frontier \(z\), left stack \(l\), and empty right stack equals the zipper tape with the same frontier and left stack whose right stack is the single blank cell.
Consider the forward-sweep configuration of a one-work-tape machine with (optional) state \(q\), input-head position \(p\), frontier \(z\), left stack \(l\), an arbitrary (possibly empty) right stack \(r\), and output word \(\mathit{out}\). Applying the local sweep action that writes the possibly-blank symbol \(b\), moves the work head right, and enters state \(q'\) produces the forward-sweep configuration with state \(q'\), the same input-head position and output, frontier \(z + 1\), left stack \(b \mathbin {::} l\), and right stack the tail of \(r\); when \(r\) is empty, the cell consumed is a blank beyond the stored zone.
Consider the backward-sweep configuration of a one-work-tape machine with (optional) state \(q\), input-head position \(p\), frontier \(z\), left stack \(l\), an arbitrary (possibly empty) right stack \(r\), and output word \(\mathit{out}\). Applying the local sweep action that writes the possibly-blank symbol \(b\), moves the work head left, and enters state \(q'\) produces the backward-sweep configuration with state \(q'\), the same input-head position and output, frontier \(z - 1\), left stack \(b \mathbin {::} l\), and right stack the tail of \(r\); when \(r\) is empty, the cell consumed is a blank beyond the stored zone.
Let \(M\) be a one-work-tape Turing machine over alphabet \(A\), let \(w\) be a word over \(A\) to be written, let \(d\) be a fixed integer displacement, and let \(\mathit{cfg}\) be a family of configurations of \(M\) indexed by a step counter \(i \in \{ 0, \dots , |w|\} \), an integer coordinate \(z\), and two lists \(l\), \(r\) of possibly-blank symbols. Assume the local one-step rule: for every \(i \lt |w|\) and all \(z\), \(l\), \(r\), a single step of \(M\) from \(\mathit{cfg}(i, z, l, r)\) yields \(\mathit{cfg}(i+1,\, z + d,\, w_i \mathbin {::} l,\, \mathrm{tail}(r))\), where \(w_i\) is the \(i\)-th symbol of \(w\), pushed as a nonblank cell. Then for every \(n \le |w|\), running \(M\) for exactly \(n\) steps from \(\mathit{cfg}(0, z, l, r)\) yields \(\mathit{cfg}\) at counter \(n\), coordinate \(z + dn\), first list the first \(n\) symbols of \(w\), reversed, prepended to \(l\), and second list \(r\) with its first \(n\) entries removed. The hypothesis is purely local and carries no premise about the global run.
Let \(M\) be a finite Turing machine over an alphabet \(\Gamma \) (a deterministic multi-tape machine with finitely many states and some number of work tapes), let \(x\) be an input word, and let \(t \in \mathbb {N}\). In the configuration reached by running \(M\) for \(t\) steps from its initial configuration on \(x\): every work-tape head position lies in the interval \([-t, t]\), and on every work tape, every cell at a coordinate \(z\) with \(z \lt -t\) or \(z \gt t\) is blank.