On Small Universal Reversible Turing Machines
T. Yokoyama
cs.FL
Oct 30, 2026 · v1
cs.LO
TL;DR
All definitions and theorems on small universal reversible Turing machines, both existence and nonexistence, are formalized in Lean 4 with Mathlib, with kernel-checked computations.
Abstract
A reversible Turing machine (RTM) is a Turing machine in which every instantaneous description has at most one predecessor. Writing URTM(m,n) for a universal RTM with m states and n symbols, we construct URTM(3,600), URTM(4,41), URTM(5,37), URTM(6,30), URTM(7,28), URTM(8,21), and URTM(85,2); each of them has fewer states or fewer symbols than each of the nine URTMs in Morita's book (2017). They come from improved versions of Morita's conversions to three states, to four states, and to two symbols; for example, the improved conversion to three states uses O(mn^2) symbols instead of O(m^2n^3). We also show that the halting problem of RTMs with at most two states is decidable for finite instantaneous descriptions, so that no RTM with at most two states is universal under any notion of universality that reduces the halting problem of Turing machines to it by a computable encoding into finite instantaneous descriptions; in particular, there is no URTM with at most two states in our formalization of Morita's definition. We also show that no three-state, two-symbol RTM is universal in that formalization.
Problem
How small can a universal reversible Turing machine (URTM) be in states and symbols? Morita's book lists nine URTMs and leaves open whether a two-state URTM exists.
Approach
The authors improve Morita's conversions to four states, three states, and two symbols, using disjoint ranges by direction, reverse counting, block decomposition, shared counters, and symbol merging. They give computable encodings that formalize Morita's universality definition. For nonexistence, they show halting is decidable for two-state RTMs and for all 359,829 normal-form keys of three-state, two-symbol RTMs. Everything is formalized in Lean 4 with Mathlib, using Mathlib's notion of computability, and the proofs depend only on the standard axioms.
Results
Seven new non-dominated URTMs are constructed: (3,600), (4,41), (5,37), (6,30), (7,28), (8,21), and (85,2). It is proved that no URTM has at most two states, and none has three states and two symbols, under the formalized definition. The formalization also found a step-count discrepancy in one of Morita's published test runs.
| Point | Blocks (b+,b-) | Symbols before | Symbols after |
|---|
| (4,41) | (2,2) | 50 | 41 |
| (5,37) | (3,2) | 49 | 37 |
| (6,30) | (3,3) | 54 | 30 |
| (7,28) | (4,3) | 50 | 28 |
| (8,21) | (4,4) | 40 | 21 |
Symbol merging results for machines derived from URTM(13,7)
