Computable

In particular, if the system of Principia Mathematica be ω-consistent, its Entscheidungsproblem is unsolvable. ~ Alonzo Church, 1936, An Unsolvable Problem of Elementary Number Theory

A problem is computable, or equivalently its solution is computable, when it can be solved using a stylus and tablet of some sort. More generally, a problem is computable within a system when the rules of that system can be arranged to mechanically produce a solution to the problem.

The most common type of computability involves whatever problems can be solved by Turing machines. By the Church-Turing thesis, this type of computability is the hardest that can be done in our universe; if a problem is computable then there exists a Turing machine which solves an equivalent definition of the problem. There are many computable problems, examples including various popular problems.

Uncomputable problems cannot be solved by a given system. In the typical context of Turing machines, uncomputable problems cannot be solved by Turing machines. An example of an uncomputable problem is whether a given Turing machine will halt on a given input: the Halting problem.

The terms also apply to other models of computation, like finite state automata and push-down automata, but Turing machine computability is the most common use.

History

In 1928, Hilbert & Ackermann asked whether there was a way to use mathematics to decide questions about mathematics. In particular, they wondered whether mechanical calculators could be used to automatically solve high-level questions about mathematical structures. They formulated the Entscheidungsproblem: the problem of deciding a yes/no question. It turns out that we will be interested in answering questions about mathematical theories that are sufficiently strong enough to phrase most of number theory; this will be enough to show that Hilbert's programme cannot succeed.

Here, sufficient strength is a side condition that arises in any Gödelian reasoning. As defined by one reference text,

Definition. A formal theory of arithmetic is sufficiently strong if and only if it captures all effectively-decidable numerical properties.

Effectiveness is also defined in that same text; a property or relation is effectively decidable when there is an algorithm that mechanically computes it in some finite number of steps on some given inputs. This is something of a retrospective framing, since we necessarily recount this history from a society where computing is ubiquitous.

Via lambda calculus

Main article: Lambda calculus

This path was laid out by Church. We first define lambda calculus and start from the fact that it is strongly normalizing.

Theorem (Church—Rosser for lambda calculus). A lambda term has at most one normal form. (Church & Rosser, 1936)

Church then defines a certain flavor of recursive function as a set of arithmetic equations over natural numbers, where some numbers are unknown variables. He points out that some of these equations are hard and some are easy. For example, consider these two equations that differ only in exponent:

x² + y² = z² (2)
x³ + y³ = z³ (3)

Theorem (wikipedia:Pythagorean triples). There are infinitely many solutions to equation (2) where 2 < x < y < z.

Theorem (wikipedia:Fermat's Last Theorem when p=3). There are no solutions to equation (3) where 2 < x < y < z. (Euler, 1770; Kausler, 1802)

Church shows that recursive functions can express a search for a least solution. For example, the least Pythagorean triple is (3, 4, 5). The process of examining all candidate solutions — the process of performing the search — defines a recursively enumerable set, the set which contains all of the solutions. Recursive enumeration can be used to examine mathematical objects like numbers and formulae. There is a grand bridge between lambda calculus and recursive functions, although Church will always phrase top-level results in terms of recursive functions first in order to stay relevant to Hilbert's programme.

Theorem. A function of natural numbers is recursive if and only if it is definable by a lambda term. (Church, Kleene & Rosser, 1936)

Definition. A recursive function decides an assignment to all-but-one of its variables when it has exactly two possible solutions over all possible assignments.

The two solutions can be any two distinct values. Kleene uses 0 and 1. Church uses 1 and 2. The intuition is that we may query a recursive function to see whether a particular assignment satisfies some property; in that sense, the recursive function represents that property. Church uses this bridge to set up Gödelian number theory and instantiate Gödel's first incompleteness.

Theorem. For any Gödel encoding, there is a recursive function indicating whether a natural number encodes a well-formed formula. (Kleene, 1936)

Theorem. The set of well-formed formulae in normal form is recursively enumerable. (Church, 1936)

Theorem. The set of well-formed formulae which have a normal form is recursively enumerable. (Church & Kleene, 1936)

Lemma (Gödel's diagonal lemma). A recursive function over two lambda-terms A and B that decides whether A reduces to B is equivalent to a recursive function over one lambda-term C that decides whether C has a normal form. (Church, 1936)

And this leads to an example of what is not computable for lambda calculus and the first refutation of Hilbert's programme.

Theorem (Undecidability of Normalization for lambda calculus). There is no recursive function that decides whether some well-formed formula has a normal form. (Church, 1936)

Corollary. The set of well-formed formulae with no normal form is not recursively enumerable. (Church, 1936)

Theorem (Undecidability of Equivalence for lambda calculus). There is no recursive function that decides whether one well-formed formula reduces to another. (Church, 1936)

Theorem (Rice's theorem for lambda calculus). There is no recursive function that decides whether a well-formed formula is a provable statement in some sufficiently-strong language of arithmetic. (Church, 1936)

Via Turing machines

Main article: Turing machine

This path was laid out by Turing. First, we note that pencil and paper is not infinitely capable.

Lemma (Turing's compact argument). Only finitely many recognizable symbols can be written on paper with ink. (Turing, 1937)

Turing proved this in a footnote! Imagine a square of paper. A symbol on the paper is a region where ink is applied. Let the distance between symbols be the area of ink that must be moved to transform one symbol into another, assuming that there is an infinite inkwell beside the paper which can serve as a source and sink. Then Turing notes that the space of symbols is compact and must have finite cover. Informally, an inkblot only has finitely many connected regions of ink. We will compute with this cover rather than the inkblot itself.

By this reasoning, recognition of symbols is a necessarily fuzzy process. Turing assumes that we are willing to define a Hilbert deductive system upon those symbols. From there, he defines Turing machines in terms of what they can compute:

Definition. A real number is computable when its digits can be enumerated by a finite sequence of reductions in some formal system.

Theorem (Computability). Any computable real number can be represented by a Turing machine. (Turing, 1937)

Turing notes that a Turing machine is a concrete object in set theory and can be represented by a natural number using Gödel encoding. This allows us to diagonalize Turing machines:

Theorem (Undecidability of Halting for Turing machines). There is no Turing machine which accepts two inputs if and only if the first input, interpreted as representing a Turing machine, will accept the second input. (Turing, 1937)

This also gives us the first version of producing an arbitrary effect at an arbitrary point, a flavor of Rice's theorem, as well as the second refutation of Hilbert's programme:

Theorem. There is no Turing machine which accepts an input if and only if that input, interpreted as a Turing machine, will print a given symbol for some input. (Turing, 1937)

Theorem (Rice's theorem for Turing machines). There is no Turing machine which accepts an input if and only if that input is interpretable as a provable statement in some sufficiently-strong language of arithmetic. (Turing, 1937)

Via category theory

This path was laid by Lawvere and explained by Yanofsky. The foundation is the following observation:

Definition. In a category with terminal object, an arrow g : X → [A, Y] is weakly point-surjective if and only if for every arrow f : A → Y there exists x in X such that for every a in A, f(a) = g(x)(a).

Definition. In a category with terminal object, an object Y has the fixed-point property if and only if for all t : Y → Y there exists y in Y such that t(y) = y.

Theorem (Lawvere's fixed point, diagonal version). In any Cartesian closed category, if there is an weakly point-surjective arrow g : A → [A, Y] then Y has the fixed-point property. (Lawvere, 1969)

Corollary (Lawvere's fixed point, Cantor's version). In any Cartesian closed category, if there is an arrow t : Y → Y such that t(y) ≠ y for all y in Y, then for no A is there a weakly point-surjective arrow A → [A, Y]. (Lawvere, 1969)

We start with Cantor's version. To see how Cantor's version works, note that sets and functions are Cartesian closed; and let Y = 2, t be negation, and lack of weak point-surjectivity be weakened to lack of surjectivity. Then its namesake emerges:

Corollary (Cantor's theorem). For no set A is there a surjection A → [A, 2] onto its power set. (Cantor, 1891)

So, let a computable universe be a category with a subobject classifier 2, a natural numbers object N, and a total isomorphism N → C for all objects C, called the coding of C, which enumerates the elements of C. For c in C, the inverse of the coding is a natural number called the code of c. Without loss of generality, we'll assume that our category is Cartesian closed and that therefore there are enumerations for all exponential objects, although the entire argument can be made with finite products. For example, the effective topos is a computable universe. Arrows in a computable universe can be partial; not all arrows are total.

In a computable universe, a program that decides halting would be a total arrow Halt : N → [N, 2] such that the code of any arrow f : X → Y is the curry of another total arrow Halt(f) : N → 2 which is defined for any x in X for which f(x) is also defined. Intuitively, whenever f(x) has a value, Halt should be defined at that value as true, and false otherwise. But there is an arrow α : 2 → 2 defined as α(0) = 1 and undefined at α(1) which has no fixed points, so:

Corollary (Undecidability of Halting for computable universes). In no computable universe is there a total arrow N → [N, 2] which decides whether a coded arrow is defined at a coded point. (Yanofsky, 2003)

We return to the diagonal theorem now. In a computable universe, there is a total isomorphism N → [N, N]. Isomorphisms are surjections, so:

Corollary (Kleene's second recursion, Rogers' fixed point). In any computable universe, N has the fixed-point property. (Kleene, 1938; Rogers, 1967)

This version of Kleene's recursion theorem is strong enough to prove both an external and internal version of Rice's theorem.

Corollary (Rice's theorem for computable universes, external version). In no computable universe is there a total arrow N → 2 which decides whether a number is the code of a provable statement in some sufficiently-strong language of arithmetic. (Yanofsky, 2003)

Corollary (Rice's theorem for computable universes, internal version). In no computable universe is there any total non-constant arrow N → 2 which decides a subset of [N, N]. (Rice, 1951)

The difference between the two statements is that the external version is always evaluated with respect to some external Gödel encoding and its associated language of arithmetic, while the internal version is always evaluated with respect to the fixed Gödel encoding used to define the computational universe. This is why the internal version appears to be an invariant, deeper statement about numbers; the Gödel encoding is still present, merely hidden.

Via topos theory

Fix some partial combinatory algebra (PCA). An algorithm is realizable if it corresponds to a proof in the PCA. Construct the realizability topos over the PCA; this is not easy, but is always possible. Any arrow in the topos is computable by decomposition into its constituent realizers.

Given any realizability topos, a language L is an collection of sentences over some alphabet of symbols S in the topos. A computable language is an arrow S* → 2 in the topos; that is, it is a subset of the sentences over S for which every element of the set has a corresponding realizer witnessing its membership.

Generalizing this particular example, consider arbitrary objects L and arrows L → 2 which express their subobjects as computations. Such arrows are known as computable subsets of L, computable properties of L, or computable decision problems, and are contained in the complexity class R.

Examples of uncomputable languages

• Languages which can solve the Turing machine or greater halting problems are uncomputable, like Oracle and various other oracle machines
• Contradictory languages like ^
• Joke languages that have commands with unknowable effects on execution, like Ifthen and User talk:/w/wiki/index.php/Talk:index.php/Main page

Non-examples

• Ambiguous languages like Brain:D which have non-deterministic parsing phases are computable; the computation ranges over all possible parses.
• Similarly, non-deterministic languages can also be computable, since a computable universal search can be proceeded over all possibilities

See also

• List of complexity classes
• Category:Uncomputable