Computation Theory · Cluster
Decidability
Turing machines, reductions, and undecidable problems.
- 01 Encoding Turing Machines and the Undecidability of Acceptance How a machine becomes a finite string, what a configuration record contains, and why diagonalization over that encoding rules out any decider for acceptance.
- 02 Recognizers, Dovetailing, and Complement Asymmetry Why a machine that halts on every yes-instance but may loop on no-instances cannot be closed under complement, and how interleaved simulation converts a recognizer into one for a different set.
- 03 Mapping Reductions and the Halting Problem How a computable function that maps one language into another transfers undecidability, why the halting problem follows from acceptance by a reduction in the opposite direction, and where the construction breaks.
- 04 Rice’s Theorem and the Collapse of Semantic Properties Why every nontrivial property of the language a program computes is undecidable, how the proof smuggles a halting question into an arbitrary property, and which program properties escape the theorem.
- 05 Presburger Arithmetic and the Decidable Side of Number Theory Why the first-order theory of addition alone admits quantifier elimination and always terminates, and how the single operation of multiplication moves the same language across the undecidability line.
- 06 Trakhtenbrot’s Theorem and the Finite Model Boundary Why first-order validity over all structures and over finite structures are both undecidable but for opposite reasons, and how a sentence can encode an entire halting computation in one finite domain.
- 07 Decision Procedures for Word Equations and Unification How Makanin’s algorithm decides whether two words with variables can be made equal, why the bound on solution length is enormous, and what unification gains from restricting to free function symbols.
- 08 The Arithmetical Hierarchy and the Turing Jump How undecidable problems are graded by the number of quantifiers needed to express them, why the halting set generates every level, and what Post’s theorem says about the resulting ladder.
- 09 The Post Correspondence Problem as a Reduction Source How a set of domino pairs encodes a computation through matched strings, why no algorithm can decide whether a match exists, and why this formulation is the convenient origin for other undecidability proofs.
- 10 Combining Decision Procedures with the Nelson–Oppen Method How separate decision procedures for arithmetic, arrays, and uninterpreted functions are made to agree on shared variables, why stable infiniteness is required, and where non-convex theories force case splits.