218 Complexity — Unary Tape
218.1 Overview
This module describes work tapes of a multi-tape Turing machine [AB09, §1.2] that hold a natural number in unary. A work tape is a map from the integer cell positions to the symbols \(\{ 0, 1, \sqcup \} \), where \(\sqcup \) is the blank. The unary tape of \(m\) holds \(1\) on cells \(0, \dots , m-1\) and is blank everywhere else. Machines that keep counters in unary increment a counter by writing \(1\) on its first blank cell and decrement it by erasing its last cell. The module proves that these two writes turn the unary tape of \(m\) into that of \(m+1\), and the unary tape of \(j+1\) into that of \(j\). It also defines the effect of an optional write at a head position.
218.2 Declarations
For a natural number \(m\), the unary tape of \(m\) is the tape \(\mathrm{ones}_m : \mathbb {Z} \to \{ 0, 1, \sqcup \} \), where \(\sqcup \) denotes the blank symbol, given by
Let \(m \in \mathbb {N}\), and let \(\mathrm{ones}_m : \mathbb {Z} \to \{ 0, 1, \sqcup \} \) be its unary tape, which holds \(1\) on cells \(0, \dots , m-1\) and the blank \(\sqcup \) elsewhere. If \(c \in \mathbb {Z}\) satisfies \(0 \le c\) and \(c \lt m\), then \(\mathrm{ones}_m(c) = 1\).
Let \(m \in \mathbb {N}\), and let \(\mathrm{ones}_m : \mathbb {Z} \to \{ 0, 1, \sqcup \} \) be its unary tape, which holds \(1\) on cells \(0, \dots , m-1\) and the blank \(\sqcup \) elsewhere. If \(c \in \mathbb {Z}\) satisfies \(m \le c\), then \(\mathrm{ones}_m(c) = \sqcup \).
Let \(m \in \mathbb {N}\), and let \(\mathrm{ones}_m : \mathbb {Z} \to \{ 0, 1, \sqcup \} \) be its unary tape, which holds \(1\) on cells \(0, \dots , m-1\) and the blank \(\sqcup \) elsewhere. If \(c \in \mathbb {Z}\) satisfies \(c \lt 0\), then \(\mathrm{ones}_m(c) = \sqcup \).
For \(m \in \mathbb {N}\), let \(\mathrm{ones}_m : \mathbb {Z} \to \{ 0, 1, \sqcup \} \) be the unary tape of \(m\), which holds \(1\) on cells \(0, \dots , m-1\) and the blank \(\sqcup \) elsewhere. The unary tape of \(0\) is the all-blank tape: \(\mathrm{ones}_0(c) = \sqcup \) for every \(c \in \mathbb {Z}\).
For \(m \in \mathbb {N}\), let \(\mathrm{ones}_m : \mathbb {Z} \to \{ 0, 1, \sqcup \} \) be the unary tape of \(m\), which holds \(1\) on cells \(0, \dots , m-1\) and the blank \(\sqcup \) elsewhere. For every \(m \in \mathbb {N}\), the tape obtained from \(\mathrm{ones}_m\) by setting cell \(m\) to \(1\) and leaving every other cell unchanged is \(\mathrm{ones}_{m+1}\).
For \(m \in \mathbb {N}\), let \(\mathrm{ones}_m : \mathbb {Z} \to \{ 0, 1, \sqcup \} \) be the unary tape of \(m\), which holds \(1\) on cells \(0, \dots , m-1\) and the blank \(\sqcup \) elsewhere. For every \(j \in \mathbb {N}\), the tape obtained from \(\mathrm{ones}_{j+1}\) by setting cell \(j\) to the blank \(\sqcup \) and leaving every other cell unchanged is \(\mathrm{ones}_j\).
Let \(T : \mathbb {Z} \to \{ 0, 1, \sqcup \} \) be a tape, where \(\sqcup \) denotes the blank symbol, let \(p \in \mathbb {Z}\) be a head position, and let \(w\) be an optional write, which is either “no write” or a symbol \(s \in \{ 0, 1, \sqcup \} \) to be written. The tape after the write is \(T\) itself if \(w\) is “no write”. If \(w\) writes \(s\), it is the tape that holds \(s\) at cell \(p\) and agrees with \(T\) at every other cell.