Time is unpredictable

This post is inspired by the question Are runtime bounds in P decidable? asked by John Sidles on the CSTheory website, and the answer given by Emanuele Viola.

Is there an automatic procedure to determine whether a given Turing machine, known to be halting, operates within time bound O(f) (assuming f is a computable function)?

Predictably, the answer turns out to be negative.

Let’s start by formalising the problem. Assume M is the Turing machine whose runtime we’re interested in, and F is another TM computing the time bound f; then

L = {(M, F) : M halts within O(F) steps}.

Also let H be the halting problem:

H = {(M’, x) : M halts on input x}.

We can now define the function R(M’, x) = (M, F), where F computes n2 and M, on input y, behaves as follows:

  • Simulate M’ on x for n = |y| steps.
  • If M’ has already halted, then loop for n2 steps.
  • Otherwise, loop for n3 steps.

We’re finally ready to prove our undecidability result.

Theorem. R is a many-one reduction from H to L.

Proof. Clearly R is a computable function, so we just need to show that

(M’, x) ∈ H ⇔ (M, F) ∈ L.

If (M’, x) ∈ H, that is, if M’ halts on input x, then it does so in k steps (for some k ∈ ℕ). Hence M runs in O(n2) time (notice that it runs in n3 time for |y| < k, but it’s only the asymptotic behaviour that matters for us). Thus (M, F) ∈ L.

On the other hand, if M’ does not halt on x, then M never completes its simulation, and the runtime for M is O(n3). Thus (M, F) ∉ L. □

Remark. We’ve actually proved a stronger statement, i.e., that the set of Turing machines running in O(n2) time is undecidable, even if we restrict the domain to machines halting in polynomial time. Similar undecidability results hold for an infinite class of time bounds.


On the length of proofs (episode II)

Last week I wrote a post about arithmetical theorems having very long proofs, and linked to an article on the SEP for the details. Today, me and my colleague Luca Manzoni realised that there is a much simpler proof; it is essentially the same proof described by Scott Aaronson for the uncomputability of the busy beaver function, and it holds for any undecidable, recursively axiomatisable theory T (that is, if there exists a recursive set of axioms generating the sentences of the theory, but no decision procedure for checking whether a sentence is a theorem).

Let L(φ) be the length in symbols of the shortest proof of the sentence φ, using a standard set of inference rules together with any recursive set of axioms for T; set L(φ) = 0 if φ is not a theorem. Also, let L(n) be the maximum L(φ) among all sentences φ of length at most n.

Theorem. L grows faster than any computable function.

Proof. Otherwise, given a sentence φ, we can first compute an integer f (|φ|) ≥ L(|φ|), then enumerate all proofs of length at most f (|φ|) and check them. If at least one of these is a proof of φ, we answer “yes”, otherwise “no”. But this is a decision procedure for T, since we know that if φ is a theorem, then it has a proof of length at most f (|φ|); contradiction. □

In particular, the theorem holds for Peano arithmetic and friends.

How I learned to stop worrying about Turing completeness and love primitive recursion

The primitive recursive functions are a class of computable arithmetic functions with a reasonably natural definition. They do not exhaust all computable functions (e.g., Ackermann’s function grows faster than any PR function). Here is a list of reasons to like them anyway.

  • The PR functions are exactly the functions that can be computed by using only for loops (i.e., without unbounded kinds of loop such as while and repeat-until).
  • Each time you apply the primitive recursion schema, you get new functions. Meaning: with n + 1 nested for loops you can compute functions that you can’t compute using only n nested for loops.
  • Any computable function can be obtained by using PR functions plus a single application of the μ operator. In other words, you just need to use one while loop (together with the for loops) to obtain a Turing machine. This is called Kleene’s normal form theorem.
  • Every recursively enumerable set is also primitively recursively enumerable. See this question on MathOverflow, where I recently discovered this fact.
  • The PR functions are exactly the functions that can be computed by Turing machines operating within a PR time bound. Isn’t this amazing? See, e.g., this paper by A.R. Meyer and D.M. Ritchie (yes, that D.M. Ritchie).
  • Any function of practical use is primitive recursive. This is a consequence of the previous point: polynomials, but also exponentials (and much, much worse functions) are all PR. If a function is not PR, then you don’t have enough time to compute it.

I strongly urge you to like the primitive recursive functions too.

On the length of proofs

One of the most amazing facts about (un)computability is the existence of functions f : ℕ → ℕ that grow faster than any recursive function, that is, for all computable g : ℕ → ℕ we have

\displaystyle \lim_{n \to \infty} \frac{g(n)}{f(n)} = 0.

The most common function of this kind is the busy beaver function, described by Tibor Radó in his paper On non-computable functions; for an introduction to this topic, you can read the excellent paper Who can name the bigger number? by Scott Aaronson (that’s where I first read about it).

Radó’s paper was published in the Bell System Technical Journal in 1962 but, as often happens, related work was done before by Kurt Gödel; see, for instance, the paper bearing the same title as this post, whose translation can be found in the classic collection The Undecidable (edited by Martin Davis).

A cool result that can be proved is that the length of the proofs of arithmetical statements also grows faster than any recursive function. Quoting Juliette Kennedy’s article about Gödel on the Stanford Encyclopedia of Philosophy:

Theorem 5. Given any recursive function f there are provable sentences φ of arithmetic such that the shortest proof is greater than f(⌜φ⌝) in length.

In other words, some theorems just have really freaking long proofs. See the SEP article for the details.