Undecidability emerges from rewriting in semi-thue systems
Diagonalization and Undecidability in Semi-Thue Systems
Computational Complexity
Summary
Deciding certain outcomes in systems that rewrite strings according to rules is surprisingly tricky. This paper shows that fundamental limits on decision-making—called undecidability—arise naturally when viewing computations as rewriting steps, instead of as traditional machine instructions. The authors prove that for some key questions in these rewriting systems, no algorithm can list all the negative cases, and they achieve this entirely within the rewriting framework itself. Their work clarifies old ideas about how self-reference and universality cause undecidability but in a new setting of rewriting rules.
What this means in practice
- •For formal methods engineers: Understand which rewriting-based system properties cannot be automatically verified due to inherent undecidability in nondeterministic rewriting.
- •For program analysis tool developers: Design better static analyzers by recognizing limits of decidability when analyzing programs modeled via rewriting systems.
A theory result. No direct application yet.
Authors
Vesa Halava, Reino Niskanen
Abstract
We revisit classical diagonalization argument in the setting of semi-Thue systems, viewing computation as nondeterministic rewriting rather than sequential machine execution. Semi-Thue systems naturally generate derivation trees, making existential acceptance, reachability, and infinite derivations fundamental computational notions. We formulate acceptance and decision directly in terms of derivation trees and study the associated assertion, word, and infiniteness problems. We prove that the complements of the assertion and word problems are not recursively enumerable by direct Post-style diagonal arguments. For the infiniteness problem, we give a constructive diagonalization based on a fixed universal semi-Thue system. Unlike the classical approach, the diagonal construction is carried out entirely within the rewriting formalism: the universal system remains an ordinary nondeterministic semi-Thue system while simulating encoded semi-Thue computations, including self-reference. These results show that undecidability in semi-Thue systems arises naturally from universality and self-reference in nondeterministic rewriting, rather than from machine states or control mechanisms. This perspective clarifies the relationship between rewriting systems, recursive enumerability, and classical diagonal arguments originating in the work of Post and Turing.