211 Complexity — Convention
211.1 Overview
This module fixes the calling convention of the machine-construction library for multi-tape Turing machines over the Boolean alphabet: the canonical seam configuration (a designated anchor state, input head at its initial position, each work tape holding one word written from the origin with its head at the origin, and empty output) at which loop rounds and wrapped subroutines meet, together with the fact that a machine’s initial configuration is such a seam. It also introduces the pure list and arithmetic functions against which the primitive machine contracts are stated: splitting a word at its last \(\mathrm{true}\), least solutions of padding length equations, fixed-width binary increment with overflow, and the splitting off of a leading unary token.
211.2 Declarations
Let \(k \ge 0\), let \(x\) be a Boolean input word, let \(q\) be a state, and let \(w = (w_0, \dots , w_{k-1})\) be a family of Boolean words indexed by the \(k\) work tapes. The seam configuration \(\mathrm{seam}(q, w)\) of a \(k\)-work-tape machine over the Boolean alphabet on input \(x\) is the configuration whose control is in the (non-halted) state \(q\), whose input head sits on the first input cell (position \(1\)), whose work tape \(i\) holds the word \(w_i\) in cells \(0, \dots , \left\lvert w_i\right\rvert - 1\) and is blank at every other integer cell, whose work-tape heads are all at cell \(0\), and whose output tape is empty.
Let \(M\) be a deterministic Turing machine with \(k\) work tapes over the Boolean alphabet, with start state \(q_0\), and let \(x\) be a Boolean input word. Then the initial configuration of \(M\) on \(x\) equals the seam configuration \(\mathrm{seam}(q_0, w)\) with \(w_i = \varepsilon \) the empty word for every work tape \(i\); that is, the configuration in state \(q_0\) with the input head on the first input cell, every work tape entirely blank with its head at cell \(0\), and empty output.
Let \(k \ge 0\) be a number of work tapes, \(x\) a Boolean input word, \(q\) a state, \(w = (w_0, \dots , w_{k-1})\) a family of Boolean words, and \(i \lt k\) a work-tape index. In the seam configuration \(\mathrm{seam}(q, w)\) of a \(k\)-work-tape machine over the Boolean alphabet on input \(x\) (state \(q\), input head on the first input cell, work tape \(j\) holding \(w_j\) from cell \(0\), all work heads at cell \(0\), empty output), work tape \(i\) is exactly the buffer tape of \(w_i\): for every integer cell \(z\), its content is the \(z\)-th letter of \(w_i\) (counting from \(0\)) when \(0 \le z \lt \left\lvert w_i\right\rvert \), and blank otherwise.
For a Boolean word \(v\), \(\mathrm{cut}(v)\) is the prefix of \(v\) strictly before its last occurrence of \(\mathrm{true}\): if \(v = u \, \mathrm{true} \, \mathrm{false}^m\) for some word \(u\) and \(m \ge 0\), the result is \(u\), and if \(v\) contains no \(\mathrm{true}\) (in particular if \(v\) is empty), the result is undefined (none).
For natural numbers \(C\), \(e\) and \(n\), \(\mathrm{solve}_{C,e}(n)\) is the least \(i \in \{ 0, \dots , n\} \) satisfying \(i + C \cdot (i+1)^e = n\), or undefined (none) when no such \(i\) exists.
Fixed-width little-endian binary increment with overflow, defined recursively on Boolean words (least significant bit first): the empty word overflows (result none); a word \(\mathrm{false} \cdot r\) is sent to \(\mathrm{true} \cdot r\); and a word \(\mathrm{true} \cdot r\) is sent to \(\mathrm{false} \cdot r'\) where \(r'\) is the increment of \(r\), overflowing whenever the increment of \(r\) overflows. Thus a word of length \(\ell \) is mapped to the binary successor of the same length \(\ell \), and the result is none exactly when the word consists entirely of \(\mathrm{true}\).
For a function \(f : \mathbb {N} \to \mathbb {N}\) and a natural number \(n\), \(\mathrm{solve}_f(n)\) is the least \(i \in \{ 0, \dots , n\} \) satisfying \(i + f(i) = n\), or undefined (none) when no such \(i\) exists.
For a Boolean word \(v\), \(\mathrm{tok}(v)\) is the pair (token, remainder) obtained by splitting off the maximal leading block of \(\mathrm{true}\)’s together with the \(\mathrm{false}\) that terminates it: if \(v = \mathrm{true}^m \, \mathrm{false} \, r\) with \(m \ge 0\), the result is \((\mathrm{true}^m \, \mathrm{false}, \, r)\), and if \(v = \mathrm{true}^m\) contains no \(\mathrm{false}\) (including \(v\) empty), the result is \((\mathrm{true}^m, \varepsilon )\) with \(\varepsilon \) the empty word.