🚀 go-pugleaf

Here are two articles about the practical solution to the halting
problem. The first, from February this year, is short and should give
people an idea of the resources implied by ``practical solution.''
(Practical enough that it could reasonably be an option in Saber-C.)

The second, from January 1989, was my first posting of the solution, on
comp.theory. I remember having just finished reading an article in good
old Dr. Dobbs about the halting problem. It gave the usual presentation
of the theory, but went out on a limb and said that the halting problem
wasn't solvable in practice. As happens so often in computer `science,'
the limb wasn't connected to the tree's trunk. After seeing a similarly
unjustified statement in a discussion in comp.lang.c and comp.theory, I
was sufficiently annoyed to write the article.

Several months ago someone from England seemed interested in
implementing the method. I don't know what's come of it. Oh, well.

---Dan

>From: brnstnd@stealth.acf.nyu.edu
Newsgroups: comp.software-eng
Subject: Re: Have *YOU* ever written a program which COULDN'T be proven correct?
Message-ID: <3803:04:53:29@stealth.acf.nyu.edu>
Date: 14 Feb 90 04:53:30 GMT
Distribution: usa

In article <793@arc.UUCP> steve@arc.UUCP (Steve Savitzky) writes:
> I think you missed my point, which is that whether or not the halting
> problem can be solved *in theory* for real programs on real computers,
> it cannot be solved *in practice*.  

A year ago I posted a short note to comp.theory titled Finite Halting
Problem Considered Solvable. The gist of it is that you can solve the
halting problem for a program using just twice the memory and thrice
the time.

In practice, with language support, you designate certain variables
to be tested for looping. Those variables are stored twice, and the
program runs at a third of the speed. If those variables together enter
a loop, the loop will be detected during its first period. For some
programs this could be very useful.

---Dan

>From: bernsten@phoenix.UUCP (Dan Bernstein)
Newsgroups: comp.theory
Subject: Finite Halting Problem Considered Solvable
Message-ID: <8901162049.AA11027@jade.berkeley.edu>
Date: 16 Jan 89 16:32:35 GMT
Sender: daemon@ucbvax.BERKELEY.EDU
Reply-To: TheoryNet List <THEORYNT%NDSUVM1.bitnet@jade.berkeley.edu>,
        Dan Bernstein <phoenix!bernsten@PRINCETON.EDU>
Distribution: inet
Organization: The Internet
Lines: 52


The halting problem is to determine whether a given program loops forever.
This is an uncomputable function of a program, as we all know.

But if a program is restricted to a finite number of states then the
problem is computable. The practical solution is that we run the program
on two machines with that number of states, one machine exactly twice as
fast as the other; if the program loops in time t to t+u, then we will
see the machines in exactly the same state at time 3t to 3t+3u.

Now consider modern, real computers.

The space needed for this is practical. But the time is a trickier
consideration. How do we compare the states of two computers? The
solution is that in unit time a computer modifies a bounded-size
portion of its state as expressed in bits. So we merely watch what
registers, memory bytes, etc. are changed, incrementing a difference
count when something is made different on the two machines and
decrementing it when something is made the same. As a matter of fact,
this (at least for memory) is already done by good caches. It would
be a simple modification to those caches designed for multiprocessors
to have them keep track of (1) registers and flags as well as memory
and (2) a difference count.

Of course, this eminently practical hardware solution is only
appropriate if the entire machine is involved in a single computation
that we don't want to have accidentally looping. But I'd say that
the problem is practically solvable in software for many situations.

For example, MACSYMA and similar programs could have a feature that
a user-defined function be run three times slower and have it detect
infinite loops of variables blah, blah, and blah in the function. I
would expect that this be restricted to non-recursively written functions,
and restricted to functions that don't use non-mathematical stuff like
reading from a disk file---but it's still quite doable and would be a
real, live, practical solution to the halting problem.

More ambitiously, I can see how a C compiler could compile a function to
detect infinite loops. The function would probably run somewhat slower
than just three times, as most optimizations would go down the drain and
dealing with the difference count would be a major speed factor relative
to the speed of single expressions. And yes, it would take double the
memory---which could be a problem if the function had an array taking
an amount of space comparable to the space available on the machine.
And I would expect the restriction that the function and everything it
calls must use only built-in C, no system calls or anything else possibly
external; and also that the function and everything it calls must only
use variables local to themselves. But after all these caveats this still
remains a valuable tool that I would have loved to have for testing many
programs: the practical solution to the halting problem.

---Dan Bernstein, bernsten@phoenix.princeton.edu