Search arXiv⌕ Search

arXiv · 2610.40105

Diagonalization and Undecidability in Semi-Thue Systems

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.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Vesa Halava, Reino Niskanen. 2026-10-29. Diagonalization and Undecidability in Semi-Thue Systems. https://arxiv.org/abs/2610.40105

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

KEEP EXPLORING

Related papers

Boolean PCSPs through the lens of Fourier Analysis

We develop an analytical framework for Boolean promise constraint satisfaction problems (PCSPs) that studies polymorphisms through the notion of influence from Fourier analysis of Boolean functions. Extending the work of Brakensiek, Guruswami, and Sandeep [ICALP'21] on Ordered PCSPs, we identify two general phenomena in Boolean minions indicative of hardness or tractability: (1) preservation of coordinate influence under random 2-to-1 minors and (2) the presence of sharp thresholds. We demonstrate that these phenomena occur in broader settings than previously established, yielding new hardness/tractability results for minions consisting of unate or polynomial threshold functions.

cs.CC↗

Self-Referential $K$-SAT and the Finite Analogue of Gödel's Incompleteness Theorem

We study self-reference and solution independence in Boolean $K$-SAT as a finite analogue of Gödel incompleteness. Independence is defined through factorial moments of the solution count. Constant-width random formulas fail this criterion due to correlations among overlapping assignments. At a covering threshold, logarithmic-width random CNFs have a Poisson solution count, with positive probabilities of unsatisfiability and unique satisfiability. Replacing a redundant clause by one falsified by the unique solution yields an unsatisfiable companion preserving the unsigned incidence graph. For every permitted local view of a good uniquely satisfiable formula, an unsatisfiable companion preserves that view. Irreducibility defeats deterministic and bounded-error evaluators using $N^c$ clause queries, for fixed $0 0$, transcripts of $N^{1-δ}$ queries leave $N-o(N)$ bits of witness entropy. On typical support graphs, expansion yields linear Resolution width, linear PC/PCR and SOS degree, and exponential proof size. Bounds hold for semantic Cutting Planes under a partition condition and for Positivstellensatz with bounded product width, uniformly over unsatisfiable support-preserving signings. Structural evidence and the limits of acceleration strategies motivate the self-referential $K$-SAT exhaustive-search hypothesis (SRK-ESH): no uniform deterministic algorithm deciding the promise family achieves a fixed proportional saving in the exponent. This dual-evidence criterion combines intrinsic hardness mechanisms with algorithmic evidence. We interpret this hypothesis as a quantitative projection of the Gödel-style local--global gap. The information obstruction constrains quantum local observation and statistical learning from bounded local information.

cs.CC↗

On the Complexity of Finding Fixed Points for Set-Valued Contractions

In this paper, we study the computational complexity of finding fixed points for set-valued contractions. We first formulate a computational problem for Nadler's fixed-point theorem: Projected-Nadler, and prove that it is $\mathsf{CLS}$-complete by showing its equivalence to Continuous-LocalOpt. We then establish a stronger converse for Nadler's fixed point theorem that can be applied as a tool to analyze the convergence rate of set-valued basic iteration procedure. Finally, we reduce large-margin triplet stationarity problem to Projected-Nadler. Together with its $\mathsf{CLS}$-hardness introduced in [arXiv:2509.16898], this yields $\mathsf{CLS}$-completeness of large-margin triplet stationarity.

cs.CC↗