Computability theory is the branch of theoretical computer science that asks which tasks can be performed by mechanical procedures and which cannot. It is a formal study that grew out of questions in logic and mathematics and is now a foundation for modern computer science. Researchers and scientists use formal models and rigorous proofs to classify problems as solvable (computable) or unsolvable (undecidable).

Basic concepts and formal models

At the heart of computability theory is the notion of an abstract machine that captures the intuitive idea of an algorithm. One standard formalism is a mathematical description of a model of computation known as the Turing machine. A Turing machine is often described informally as a simple typewriter-like device with a read/write head that moves along an infinite tape, changing symbols according to a finite set of rules. This idealized machine was introduced to make precise what it means to compute a function or decide a language.

The machine is named after the British mathematician Alan Turing, commonly referenced as Alan Turing in historical accounts of the field. Using this and equivalent formalisms (lambda calculus, recursive functions, register machines), theorists define classes of computable functions and prove results about their limits.

Decidability, the Halting problem, and examples

A decision problem is called decidable if there exists an algorithm that always halts and correctly answers yes or no for every input. Some problems are undecidable: no algorithm can solve every instance. The most famous example is the Halting problem, which asks whether a given program will eventually stop on a given input. In the 1930s it was shown that no single algorithm can decide halting for all programs. From that basic negative result follow many other undecidability proofs by reduction.

  • Decidable problems: arithmetic on fixed-size integers, regular language membership, many graph algorithms.
  • Undecidable problems: general program equivalence, first-order logic validity in some settings, certain problems about Diophantine equations.

Proof techniques in computability rely on diagonalization, reductions, and constructive encodings of programs as data. Reductions are used to transfer undecidability from one problem to another: if A reduces to B and A is undecidable, then B is also undecidable.

History and the Church–Turing perspective

Computability theory emerged in the 1930s from independent work by Alonzo Church, Alan Turing, and others. The Church–Turing thesis informally asserts that the intuitive notion of algorithmic computability corresponds to the functions computable by these formal models. While the thesis is not a theorem (it relates a formal notion to an informal one), it has guided theoretical and practical thinking about what machines can compute.

Over the decades the field expanded to study relative computability (oracle machines), degrees of unsolvability, and connections with logic and set theory. It also set the stage for computational complexity theory, which refines questions about how efficiently problems can be solved rather than whether they can be solved at all.

Applications and notable implications

Although computability results are often negative, they have many practical consequences. Knowing that a problem is undecidable prevents wasted effort seeking a universal algorithm and motivates restricted models, heuristics, approximate methods, or semi-decision procedures that work in many cases. Computability concepts underpin compiler design, program analysis, formal verification, and the limits of automated reasoning.

Important distinctions include computability versus complexity (can it be done at all vs. how much resource is required) and decidability versus semi-decidability (where an algorithm may halt with yes for positive instances but run forever on negatives). The subject remains central to theoretical computer science, mathematics, and the philosophy of computation.