215 Complexity — Counter Prog
215.1 Overview
This module introduces counter programs, the programming model used for the polynomial-time emitters of [AB09, §6.2, Remark 6.7]. A counter program is a goto program over finitely many registers holding natural numbers. It can increment, decrement (saturating at \(0\)) and zero-test a register, print a bit or print a register’s value in unary, and read its binary input once from left to right. The module gives the step semantics of such programs and compiles every counter program into a binary multi-tape Turing machine with one work tape per register, holding that register’s value in unary. The main result is that one abstract step, taken while every register is at most \(B\), is simulated in at most \(2B + 3\) machine steps.
215.2 Declarations
Fix a number \(R\) of registers, indexed by \(\{ 0, \dots , R-1\} \), and a set \(\Lambda \) of labels. An instruction of a counter program over \(R\) registers with labels in \(\Lambda \) is one of the following, where \(r\) ranges over registers, \(b\) over bits and \(\ell ', \ell _0, \ell _+, \ell _\bot , \ell _1\) over labels: \(\mathsf{halt}\) (stop); \(\mathsf{goto}(\ell ')\) (jump to \(\ell '\)); \(\mathsf{out}(b, \ell ')\) (print the bit \(b\), then go to \(\ell '\)); \(\mathsf{inc}(r, \ell ')\) (increment register \(r\)); \(\mathsf{dec}(r, \ell ')\) (decrement register \(r\), with \(0\) staying \(0\)); \(\mathsf{jz}(r, \ell _0, \ell _+)\) (go to \(\ell _0\) if register \(r\) is \(0\), and to \(\ell _+\) otherwise); \(\mathsf{pr}(r, \ell ')\) (print \(1^v\), where \(v\) is the value of register \(r\)); and \(\mathsf{rd}(\ell _\bot , \ell _0, \ell _1)\) (read the next input symbol: go to \(\ell _\bot \) if the input is exhausted, and otherwise consume the symbol and go to \(\ell _0\) or \(\ell _1\) according as it is \(0\) or \(1\)).
For \(R\) registers and a set \(\Lambda \) of labels, an abstract state of a counter program consists of four components: the current label, which is either an element of \(\Lambda \) or a special value marking that the program has halted; a register assignment \(\rho : \{ 0, \dots , R-1\} \to \mathbb {N}\); the read position \(p \in \mathbb {N}\), the number of input symbols consumed so far; and the output printed so far, a finite bit string.
Let \(P : \Lambda \to \mathrm{Instr}\) be a counter program over \(R\) registers (an instruction at every label) and \(x\) an input bit string. One step of \(P\) on \(x\) leaves a halted state unchanged. A state with label \(\ell \), registers \(\rho \), read position \(p\) and output \(w\) is updated according to \(P(\ell )\), every component not mentioned staying the same: \(\mathsf{halt}\) makes the state halted; \(\mathsf{goto}(\ell ')\) moves to label \(\ell '\); \(\mathsf{out}(b, \ell ')\) moves to \(\ell '\) and replaces the output by \(w b\); \(\mathsf{inc}(r, \ell ')\) and \(\mathsf{dec}(r, \ell ')\) move to \(\ell '\) and replace \(\rho (r)\) by \(\rho (r) + 1\), respectively by the truncated difference \(\max (\rho (r) - 1, 0)\); \(\mathsf{jz}(r, \ell _0, \ell _+)\) moves to \(\ell _0\) if \(\rho (r) = 0\) and to \(\ell _+\) otherwise; \(\mathsf{pr}(r, \ell ')\) moves to \(\ell '\) and replaces the output by \(w\, 1^{\rho (r)}\); and \(\mathsf{rd}(\ell _\bot , \ell _0, \ell _1)\) moves to \(\ell _\bot \) if \(p \ge |x|\), and otherwise moves to \(\ell _0\) or \(\ell _1\) according as the symbol \(x_p\) (indexing from \(0\)) is \(0\) or \(1\), and increases the read position to \(p + 1\).
Given a counter program \(P\) over \(R\) registers with labels in \(\Lambda \), an input bit string \(x\), an abstract state \(s\) and \(t \in \mathbb {N}\), the \(t\)-step run \(\mathrm{run}_{P,x}(s, t)\) is the state obtained by applying the one-step map of \(P\) on \(x\) to \(s\) exactly \(t\) times.
For a label \(\ell _0\), the initial abstract state at \(\ell _0\) (for \(R\) registers) has current label \(\ell _0\), every register equal to \(0\), read position \(0\), and empty output.
For every counter program \(P\) over \(R\) registers with labels in \(\Lambda \), every input bit string \(x\) and every abstract state \(s\), running \(P\) on \(x\) from \(s\) for zero steps returns \(s\): \(\mathrm{run}_{P,x}(s, 0) = s\).
Let \(P\) be a counter program over \(R\) registers with labels in \(\Lambda \), \(x\) an input bit string and \(s\) an abstract state. For all \(a, b \in \mathbb {N}\), running \(a + b\) steps from \(s\) is the same as running \(a\) steps and then \(b\) further steps: \(\mathrm{run}_{P,x}(s, a + b) = \mathrm{run}_{P,x}(\mathrm{run}_{P,x}(s, a), b)\).
Let \(P\) be a counter program over \(R\) registers with labels in \(\Lambda \), \(x\) an input bit string, \(s\) an abstract state and \(t \in \mathbb {N}\). Running \(t + 1\) steps from \(s\) equals running \(t\) steps from the state obtained by one step of \(P\) on \(x\) from \(s\): \(\mathrm{run}_{P,x}(s, t + 1) = \mathrm{run}_{P,x}(\mathrm{step}_{P,x}(s), t)\).
Let \(P\) be a counter program over \(R\) registers with labels in \(\Lambda \), \(x\) an input bit string, and \(s\) an abstract state whose label component marks it as halted. Then for every \(t \in \mathbb {N}\), running \(P\) on \(x\) from \(s\) for \(t\) steps returns \(s\) unchanged.
Let \(P\) be a counter program over \(R\) registers with labels in \(\Lambda \), \(x\) an input bit string, \(s\) an abstract state with registers \(\rho \), and \(r\) a register. If \(\rho '\) denotes the registers of the state reached from \(s\) by one step of \(P\) on \(x\), then \(\rho '(r) \le \rho (r) + 1\).
Let \(P\) be a counter program over \(R\) registers with labels in \(\Lambda \), \(x\) an input bit string, and \(s\) an abstract state whose read position \(p\) satisfies \(p \le |x|\). Then the read position of the state reached from \(s\) by one step of \(P\) on \(x\) is again at most \(|x|\).
Let \(P\) be a counter program over \(R\) registers with labels in \(\Lambda \), \(x\) an input bit string, \(s\) an abstract state with registers \(\rho \), \(r\) a register and \(t \in \mathbb {N}\). If \(\rho '\) denotes the registers of the state reached from \(s\) after \(t\) steps of \(P\) on \(x\), then \(\rho '(r) \le \rho (r) + t\).
For \(R\) registers and a set \(\Lambda \) of labels, the control states of the Turing machine compiled from a counter program are of five kinds, where \(r\) is a register and \(\ell , \ell _0, \ell _+\) are labels: \(\mathsf{main}(\ell )\), about to execute the instruction at label \(\ell \); \(\mathsf{dec}_2(r, \ell )\), the second phase of a decrement of register \(r\); \(\mathsf{jz}_2(r, \ell _0, \ell _+)\), the second phase of a zero test of register \(r\); \(\mathsf{print}_{\leftarrow }(r, \ell )\), printing register \(r\) while walking left over its cells; and \(\mathsf{print}_{\rightarrow }(r, \ell )\), walking back right after such a print. When \(\Lambda \) is finite, so is the set of control states.
Consider machines with \(R\) work tapes over the bit alphabet whose control states are the compiled control states for \(R\) registers and labels \(\Lambda \). Given a work tape index \(t\), an input-head move \(i \in \{ -1, 0, 1\} \), a write instruction (write nothing, write a blank, or write a bit), a head move \(m \in \{ -1, 0, 1\} \), an optional output bit \(o\) and an optional next control state \(q\), this is the single-step action that moves the input head by \(i\), performs the write instruction on tape \(t\) and moves its head by \(m\), leaves every other work tape untouched (no write, no movement), emits \(o\) if present, and passes to \(q\) (halting if \(q\) is absent).
Consider machines with \(R\) work tapes over the bit alphabet whose control states are the compiled control states for \(R\) registers and labels \(\Lambda \). Given an input-head move \(i \in \{ -1, 0, 1\} \), an optional output bit \(o\) and an optional next control state \(q\), this is the single-step action that moves the input head by \(i\), neither writes on nor moves any work tape, emits \(o\) if present, and passes to \(q\) (halting if \(q\) is absent).
Let \(P\) be a counter program over \(R\) registers with labels in \(\Lambda \). Its compiled transition table maps a control state, the symbol under the input head and the symbols under the \(R\) work heads to an action; unless stated otherwise the action writes nothing, moves no head, emits nothing, and touches only the work tape of the register \(r\) involved. In \(\mathsf{main}(\ell )\) it acts according to \(P(\ell )\): \(\mathsf{halt}\) halts; \(\mathsf{goto}(\ell ')\) passes to \(\mathsf{main}(\ell ')\); \(\mathsf{out}(b, \ell ')\) emits \(b\) and passes to \(\mathsf{main}(\ell ')\); \(\mathsf{inc}(r, \ell ')\) writes \(1\) on tape \(r\), moves its head right and passes to \(\mathsf{main}(\ell ')\); \(\mathsf{dec}(r, \ell ')\), \(\mathsf{jz}(r, \ell _0, \ell _+)\) and \(\mathsf{pr}(r, \ell ')\) move the head of tape \(r\) left and pass to \(\mathsf{dec}_2(r, \ell ')\), \(\mathsf{jz}_2(r, \ell _0, \ell _+)\) and \(\mathsf{print}_{\leftarrow }(r, \ell ')\) respectively; and \(\mathsf{rd}(\ell _\bot , \ell _0, \ell _1)\) passes to \(\mathsf{main}(\ell _\bot )\) if the input head reads a blank, and otherwise moves the input head right and passes to \(\mathsf{main}(\ell _0)\) or \(\mathsf{main}(\ell _1)\) according as it reads \(0\) or \(1\). In the auxiliary states, with \(c\) the cell scanned on tape \(r\): \(\mathsf{dec}_2(r, \ell )\) erases \(c\) if it is nonblank and otherwise moves right, then passes to \(\mathsf{main}(\ell )\); \(\mathsf{jz}_2(r, \ell _0, \ell _+)\) moves right and passes to \(\mathsf{main}(\ell _+)\) if \(c\) is nonblank and to \(\mathsf{main}(\ell _0)\) otherwise; \(\mathsf{print}_{\leftarrow }(r, \ell )\) emits \(1\), moves left and stays put in its state if \(c\) is nonblank, and otherwise moves right and passes to \(\mathsf{print}_{\rightarrow }(r, \ell )\); and \(\mathsf{print}_{\rightarrow }(r, \ell )\) moves right and stays in its state if \(c\) is nonblank, and otherwise passes to \(\mathsf{main}(\ell )\) without moving.
Let \(\Lambda \) be a finite set of labels, \(P\) a counter program over \(R\) registers with labels in \(\Lambda \), and \(\ell _0 \in \Lambda \) a start label. The machine of \(P\) started at \(\ell _0\) is the finite-state multi-tape Turing machine over the bit alphabet with \(R\) work tapes (one per register), whose states are the compiled control states for \(R\) and \(\Lambda \), whose initial state is \(\mathsf{main}(\ell _0)\), and whose transition function is the compiled transition table of \(P\).
For a natural number \(v\) write \(1^v\) for the unary tape whose cells \(0, \dots , v-1\) hold \(1\) and whose other cells (indexed by \(\mathbb {Z}\)) are blank. Let \(x\) be an input bit string of length \(n\) and \(s\) an abstract state with registers \(\rho \), read position \(p\) and output \(w\). Its encoding is the configuration, on input \(x\), of a machine with \(R\) work tapes and the compiled control states, whose state is \(\mathsf{main}(\ell )\) if \(s\) has label \(\ell \) and is halted if \(s\) is halted, whose input head is at position \(\min (p + 1, n + 1)\), whose work tape \(r\) holds \(1^{\rho (r)}\) with its head on cell \(\rho (r)\), and whose output tape holds \(w\).
Let \(\Lambda \) be a finite set of labels, \(P\) a counter program over \(R\) registers with labels in \(\Lambda \), \(\ell _0 \in \Lambda \), and \(x\) an input bit string. Let \(C\) be a configuration on input \(x\) of the machine of \(P\) started at \(\ell _0\) which is in some control state \(q\) (not halted), with work tapes \((T_i)\) and work heads \((h_i)\). Then one step of that machine maps \(C\) to the result of applying to \(C\) the action that the compiled transition table of \(P\) assigns to \(q\), the symbol under the input head of \(C\), and the work-tape symbols \((T_i(h_i))_i\).
Let \(x\) be an input bit string and consider a configuration on \(x\), with \(R\) work tapes and the compiled control states, having an arbitrary state, input-head position \(p\), work tapes \((T_i)\), work heads \((h_i)\) and output \(w\). Applying to it the action on the single work tape \(t\) with input-head move \(i\), write instruction \(\omega \), head move \(m\), optional output bit \(o\) and optional next state \(q\) yields the configuration with state \(q\), input-head position the clamped move of \(p\) by \(i\), tape \(t\) replaced by \(T_t\) with cell \(h_t\) overwritten as prescribed by \(\omega \) (and unchanged if \(\omega \) writes nothing), head \(t\) moved to \(h_t + m\), all other tapes and heads unchanged, and output \(w\) followed by \(o\) if \(o\) is present.
Let \(x\) be an input bit string and consider a configuration on \(x\), with \(R\) work tapes and the compiled control states, having an arbitrary state, input-head position \(p\), work tapes \((T_i)\), work heads \((h_i)\) and output \(w\). Applying to it the action that touches no work tape, with input-head move \(i\), optional output bit \(o\) and optional next state \(q\), yields the configuration with state \(q\), input-head position the clamped move of \(p\) by \(i\), the same work tapes \((T_i)\) and heads \((h_i)\), and output \(w\) followed by \(o\) if \(o\) is present.
Let \(\Lambda \) be a finite set of labels, \(P\) a counter program over \(R\) registers with labels in \(\Lambda \), \(\ell _0 \in \Lambda \), \(x\) an input bit string, \(r\) a register, \(\ell \) a label, \(p\) an input-head position, \((T_i)\) work tapes and \((h_i)\) work heads, and \(m \in \mathbb {N}\) such that tape \(r\) is the unary tape \(T_r = 1^m\) (cells \(0, \dots , m-1\) hold \(1\), all others blank). Then for every \(j \le m\) and every output string \(w\), running the machine of \(P\) started at \(\ell _0\) for \(j + 1\) steps from the configuration in state \(\mathsf{print}_{\leftarrow }(r, \ell )\) with input head \(p\), tapes \((T_i)\), heads \((h_i)\) except that head \(r\) is on cell \(j - 1\), and output \(w\), reaches the configuration in state \(\mathsf{print}_{\rightarrow }(r, \ell )\) with input head \(p\), tapes \((T_i)\), heads \((h_i)\) except that head \(r\) is on cell \(0\), and output \(w\, 1^j\).
Let \(\Lambda \) be a finite set of labels, \(P\) a counter program over \(R\) registers with labels in \(\Lambda \), \(\ell _0 \in \Lambda \), \(x\) an input bit string, \(r\) a register, \(\ell \) a label, \(p\) an input-head position, \((T_i)\) work tapes, \((h_i)\) work heads, \(w\) an output string, and \(m \in \mathbb {N}\) such that tape \(r\) is the unary tape \(T_r = 1^m\) (cells \(0, \dots , m-1\) hold \(1\), all others blank). Then for every \(d \le m\), running the machine of \(P\) started at \(\ell _0\) for \(d + 1\) steps from the configuration in state \(\mathsf{print}_{\rightarrow }(r, \ell )\) with input head \(p\), tapes \((T_i)\), heads \((h_i)\) except that head \(r\) is on cell \(m - d\), and output \(w\), reaches the configuration in state \(\mathsf{main}(\ell )\) with input head \(p\), tapes \((T_i)\), heads \((h_i)\) except that head \(r\) is on cell \(m\), and output \(w\).
For \(v \in \mathbb {N}\) let \(1^v\) be the unary tape whose cells \(0, \dots , v-1\) hold \(1\) and whose other cells are blank. Let \(\rho : \{ 0, \dots , R-1\} \to \mathbb {N}\), let \(t\) be an index and \(m \in \mathbb {N}\), and let \(\rho '\) agree with \(\rho \) except that \(\rho '(t) = m\). Then replacing the \(t\)-th entry of the tape vector \((1^{\rho (r)})_r\) by \(1^m\) gives the tape vector \((1^{\rho '(r)})_r\).
Let \(\rho : \{ 0, \dots , R-1\} \to \mathbb {N}\), let \(t\) be an index and \(m \in \mathbb {N}\), and let \(\rho '\) agree with \(\rho \) except that \(\rho '(t) = m\). Then replacing the \(t\)-th entry of the integer vector \((\rho (r))_r\) by \(m\) gives the integer vector \((\rho '(r))_r\).
Let \(x\) be an input bit string of length \(n\) and \(s\) an abstract state of a counter program over \(R\) registers whose read position \(p\) satisfies \(p \le n\). Then in the machine configuration encoding \(s\) on input \(x\), the input head is at position \(p + 1\).
Let \(x\) be an input bit string of length \(n\) and \(s\) an abstract state of a counter program over \(R\) registers whose read position \(p\) satisfies \(p \le n\). Then the symbol under the input head in the machine configuration encoding \(s\) on input \(x\) is the bit \(x_p\) (indexing from \(0\)) when \(p \lt n\), and no symbol (a blank) when \(p = n\).
Let \(\Lambda \) be a finite set of labels, \(P\) a counter program over \(R\) registers with labels in \(\Lambda \), \(\ell _0 \in \Lambda \), \(x\) an input bit string, and \(B \in \mathbb {N}\). Let \(s\) be an abstract state that is running at some label \(\ell \in \Lambda \), whose read position is at most \(|x|\), and all of whose registers are at most \(B\). Then there is \(t \le 2B + 3\) such that running the Turing machine of \(P\) started at \(\ell _0\) for \(t\) steps from the configuration encoding \(s\) on input \(x\) yields the configuration encoding the state reached from \(s\) by one step of \(P\) on \(x\). Here a state with registers \(\rho \), read position \(p\) and output \(w\) is encoded by the configuration in control state \(\mathsf{main}(\ell )\) (or halted if the state is halted) whose input head is at position \(\min (p + 1, |x| + 1)\), whose work tape \(r\) holds \(1\) exactly on cells \(0, \dots , \rho (r) - 1\) with its head on cell \(\rho (r)\), and whose output is \(w\).