Searcharxiv⌕ Search

arXiv · 2611.00153

On Small Universal Reversible Turing Machines

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.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

T. Yokoyama. 2026-10-30. On Small Universal Reversible Turing Machines. https://arxiv.org/abs/2611.00153

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

Regular Separability for Bidirected VASS

The regular separability problem asks, given two languages, whether there exists a regular language that contains one of them and is disjoint from the other. We study regular separability for bidirected VASS. We first show that the problem remains Ackermann-complete when the input consists of two languages recognised by bidrected VASS. To find a subclass of VASS in which the problem has lower complexity we define alphabetically bidirected VASS as ones where bidirectedness is also visible in the input letters. Our main result establishes that regular separability for alphabetically bidirected VASS is EXPSPACE-complete. The key to this result is that, in this setting, regular separability coincides with disjointness. As a first ingredient in this equivalence, we also show that for alphabetically bidirected Z-VASS, regular separability and disjointness are equivalent. Consequently, regular separability for these systems is in polynomial-time. In fact, it is log-space inter-reducible with non-solvability of integer linear Diophantine equation systems. Finally, we observe that the picture changes dramatically in the presence of a zero test, namely, we show that regular separability for alphabetically bidirected one-counter automata is undecidable.

cs.FL↗

Certified Splitting: Decidability and Anchor Supply for Maximal-Munch Tokenization

A certificate is a window of bytes with an origin inside it such that, wherever the window occurs in a completely tokenizable input, the token covering the window's final byte begins at that origin. Certification is decided from the token set alone, and a certificate's occurrences mark where work may soundly begin. This paper decides certification and applies it to cuts, edits and audits. It is decided two ways, online with a completeness cutoff for literal vocabularies and offline through an armed-run verifier for arbitrary regular token sets. Either route, under a declared window budget, yields the anchor inventory, with a counterexample on each refutation. Cutting a completely tokenizable input at certified anchors and scanning the chunks independently reproduces the sequential segmentation, with no speculation or fixup pass. A tokenizability-preserving byte substitution moves boundaries only strictly between the certified anchors witnessed in the unchanged bytes on either side of it. For tokens of length at most L, an edit at p moves no boundary at or below p - L + 1. Cutting at every occurrence of a delimiter is sound exactly when it occurs only at token starts, and cutting after every occurrence exactly when it occurs only at token ends. Two instruments follow. The anchor-free span of a finite certified inventory is decided bounded or not with its exact supremum, three for the UTF-8 shape; and a differential auditor decides whether two token sets place different boundaries on an input both tokenize, with a differing input. Every theorem carries an executable check. Every measurement is a named program's output or arithmetic on such outputs, and each program ships with the paper or is pinned by commit in the munch library. That library's threaded scanner splits the archived campaign corpus at certified anchors and reproduces the sequential boundary stream byte for byte.

cs.FL↗

Finitely Verifiable Segmentation: Decidability for Every Tokenizer with a Finite-State Verifier

A segmentation policy assigns to each byte string at most one segmentation into tokens. Call it finitely verifiable when a finite automaton over marked strings, bytes paired with boundary bits, accepts exactly the policy's own segmentations. The automaton judges a proposed segmentation and need not compute one. From a supplied verifier the paper gives constructive decisions for four questions, whether a window certifies a token boundary, whether the boundary gap is bounded, whether a mask can keep generation from dead-ending, and whether two policies are equivalent. The last three specialize limitedness, co-accessibility and the equivalence of single-valued transducers. The first refines the synchronizing cut of code theory, and two more ask whether a certified cut, or the cuts of an inventory, let each piece scan alone. The class sits strictly between the online-scannable policies and those with regular domains, and online scannability is decidable in polynomial time through Choffrut's theorem. Markings are length-preserving, so the class is exactly the rational segmentation policies, a normal form rather than a restriction. The class is closed under four pipeline operations, composition over a labeled stage, restriction to a regular schema, splitting at character-class changes, and byte-fallback union of literal policies. Each composite inherits the six decisions, and certificates transfer between stages under four laws. Under rational, unifilar, almost surely stopping finite-state sources, each mass of the weighted section is an exact rational, and so is each rate where expected length is positive. Maximal-munch lexing, canonical byte-pair encoding and two-mode WordPiece instantiate the interface, and the munch library implements all six decisions. Every theorem carries an executable check, and every reported statistic is a program's own output.

cs.FL↗