Do we need to live with the uncertainty?

Introduction

In the previous post we have seen that the halting problem cannot be solved. But maybe the problem is just in our programming languages, so let’s see if we can improve them to disallow non-halting programs.

Bounded C

A program can fail to halt by two reasons (we are ignoring I/O, limited memory sizes and all that earthly issues 😀 ): it can get trapped in an infinite loop or we can enter an infinite recursion. So let’s take a language like C and remove these “troublesome” features from it by

  • only allowing iteration via the for (b = 0; b < a; b++) construct and
  • removing the possibility of doing either direct or indirect recursion.

At first sight we haven’t lost a lot. For example we can easily raise numbers to a power

int my_pow(int base, int exp)
{
    int p = 1, i;
    for (i = 0; i < exp; i++)
        p *= base;
    return p;
}

or compute the elements of the Fibonacci series.

int fib(int n)
{
    int a = 0, b = 1, i, t;
    for (i = 0; i < n; i++)
    {
        t = a + b;
        a = b;
        b = t;
    }
    return a;
}

But maybe we have lost something subtler…

Challenge

Can we make a function in “normal C” that cannot be implemented in our “bounded C”? The answer will be given in the following post… or in the comments 😀

A really impossible problem

The problem

Previously we have solved a puzzle that claimed to be impossible but was, in fact, just a bit hard 😀 But in this post we will see a problem that is really impossible to solve, the halting problem:

Given a description of an arbitrary computer program, decide whether the program finishes running or continues to run forever.

For some programs it’s easy to see if they halt or not:

def program_1():
    return 2 + 2

def program_2():
    while True: pass

def program_3():
    from itertools import count
    for i in count():
        if str(2**i)[0] == '7':
            break

def program_4():
    from itertools import count
    for i in count():
        if str(2**i)[-1] == '7':
            break

For others it’s not so simple:

def program_5():
    def z(m, n):
        if m == 0:
            return n + 1
        elif n == 0:
            return z(m - 1, 1)
        else:
            return z(m - 1, z(m, n - 1))
    z(4, 4)

And there are simple ones where it’s an open problem to know if they halt or not:

def program_6():
    from itertools import count
    for i in count(1):
        p = 2 ** i
        r = int(''.join(reversed(str(p))))
        for j in count(1):
            q = 5 ** j
            if q > r:
                break
            elif q == r:
                return
The proof

Let’s assume we have a procedure, represented by the function does_halt(), to determine if any given program will halt:

def does_halt(program):
    #
    # magic implementation
    #

We don’t care about the details of the does_halt() function. The only requirements are:

  • Its implementation should be finite.
  • It must accept any Python function that doesn’t take arguments as a program.
  • It must give an answer in an easily bounded time. For example, we should be able to say “if the input program has 1000 bytes, the function should return a boolean value indicating if it halts in no more than NNN seconds”.

The clever point of the proof, though it’s not a new kind of cleverness, is to build a program that “halts only if it doesn’t”:

def paradox():
    if does_halt(paradox):
        while True:
            pass

As the paradox() program is finite, including this small amount of code plus the code of does_halt(), does_halt() should return in a finite amount of time. If does_halt() returns False, indicating that paradox() does not halt, the program exits, finishing its execution in a finite time. On the other hand, if does_halt() returns True, indicating that paradox() does halt, it enters an infinite loop.

This proves that some of these propositions must be true:

  • does_halt() must not be finitely implementable.
  • does_halt() must reject some valid programs.
  • does_halt() execution time is unbounded.