Is there a subset of programs that avoid the halting problem

Question

I was just reading another explanation of the halting problem, and it got me thinking all the problems I've seen that are given as examples involve infinite sequences. But I never use infinite sequences in my programs - they take too long. All the real world applications have lower and upper bounds. Even reals aren't truly reals - they are approximations stored as 32/64 bits etc.

So the question is, is there a subset of programs that can be determined if they halt? Is it good enough for most programs. Can I build a set of language constructs that I can determine the 'haltability' of a program. I'm sure this has been studied somewhere before so any pointers would be appreciated. The language wouldn't be turing complete, but is there such a thing as nearly turing complete which is good enough?

Naturally enough such a construct would have to exclude recursion and unbounded while loops, but I can write a program without those easily enough.

Reading from standard input as an example would have to be bounded, but that's easy enough - I'll limit my input to 10,000,000 characters etc, depending on the problem domain.

tia

[Update]

After reading the comments and answers perhaps I should restate my question.

For a given program in which all inputs are bounded can you determine if the program halts. If so what are the constraints of the language and what are the limits of the input set. The maximal set of these constructs would determine a language which can be deduced to halt or not. Is there some study that's been done on this?

[Update 2]

here's the answer, it's yes, way back in 1967 from http://www.isp.uni-luebeck.de/kps07/files/papers/kirner.pdf

That the halting problem can be at least theoretically solved for finite-state systems has been already argued by Minsky in 1967 [4]: “...any finite-state machine, if left completely to itself, will fall eventually into a perfectly periodic repetitive pattern. The duration of this repeating pattern cannot exceed the number of internal states of the machine...”

(and so if you stick to finite turing machines then you can build an oracle)

Answer 1

The issue isn't on the input (obviously, with unbounded input, you can have unbounded running time just to read the input), it is on the number of internal states.

When the number of internal state is bounded, theoretically you can solve the halting problem in all cases (just emulate it until you reach halting or the repetition of a state), when it isn't, there are cases where it isn't solvable. But even if the number of internal states is in practice bounded, it is also so huge that the methods relying of the boundedness of the number of internal states are useless to prove the termination of any but the most trivial programs.

There are more practical ways to check the termination of programs. For instance, express them in a programming language which hasn't recursion nor goto and whose looping structures have all a bound on the number of iterations which has to be specified on entry of the loop. (Note that the bound hasn't to be really related to the effective number of iterations, a standard way to prove the termination of a loop is to have a function which you prove is strictly decreasing from one iteration to the other and your entry condition ensure is positive, you could put the first evaluation as your bound).

Answer 2

First off, consider what would happen if we had a halting detector. We know from the diagonal argument that there exists at least one program that would cause a halting detector to either never halt or give a wrong answer. But that's a bizarre and unlikely program.

There is another argument though that a halting detector is impossible, and that is the more intuitive argument that a halting detector would be magical. Suppose you want to know if Fermat's Last Theorem is true or false. You just write a program that halts if it is true and runs forever if it is false, and then run the halting detector on it. You don't run the program, you just run the halting detector on the program. A halting detector would enable us to immediately solve a huge number of open problems in number theory just by writing programs.

So, can you write a programming language that is guaranteed to produce programs whose halting can be always determined? Sure. It just cannot have loops, conditions and use arbitrarily much storage. If you're willing to live with no loops, or no "if" statements, or a strictly restricted amount of storage, then sure, you can write a language whose halting is always determinable.

Answer 3

I recommend you to read Gödel, Escher, Bach. It's a very fun and illuminating book that, among other things, touches on Gödel's incompleteness theorem and the halting problem.

To answer your question in a nutshell: the halting problem is decidable as long as your program does not contain a while loop (or any of its many possible manifestations).

Answer 4

For every program that works on a limited amount of memory (including storage of all kind), the halting problem can be solved; i.e. an undecidable program is bound to take more and more memory on the run.

But even so, this insight doesn't mean that it can be used for real-world problems, since a halting program, working on just a few kilobytes of memory, can easily take longer than the remaining lifetime of the universe to halt.

Answer 5

To (partially) answer your question "Is there a subset of programs that avoid the halting problem": yes, in fact there is. However, this subset is amazingly useless (note that the subset I'm talking about is a strict subset of the programs that halt).

The study of the complexity of problems for 'most inputs' is called generic-case complexity. You define some subset of the possible inputs, prove that this subset covers 'most inputs' and give an algorithm that solves the problem for this subset.

For instance, the halting problem is solvable in polynomial time for most inputs (in fact, in linear time, if I understand the paper correctly).

However, this result is rather useless because of three side notes: firstly, we talk about Turing machines with a single tape, rather than real-world computer programs on real-world computers. As far as I know, no one knows whether the same holds for real-world computers (even though real world computers may be able to compute the same functions as Turing machines, the number of allowed programs, their lengths and whether they halt may be completely different).

Secondly, you have to watch out what 'most inputs' means. It means that the probability that a random program of 'length' n can be checked by this algorithm tends to 1 as n tends to infinity. In other words, if n is large enough, then a random program of length n can almost surely be checked by this algorithm.

Which programs can be checked by the approach described in the paper? Essentially, all programs that halt before repeating a state (where 'state' roughly corresponds to a line of code in a program).

Even though nearly all programs can be checked in this way, none of the programs that can be checked in this way are very interesting and they usually won't be designed by humans, so this is of no practical value whatsoever.

It also indicates that generic-case complexity will probably not be able to help us with the halting problem, as nearly all interesting programs are (apparently) hard to check. Or, alternatively phrased: nearly all programs are uninteresting, but easy to check.

Answer 6

There is, and in fact there are programs in real life that solve the halting problem for other problems all the time. They are part of the operating system you are running your computer on. Undecidability is a weird claim that only says that there isn't such a program that works for ALL other programs.

One person correctly stated that the halting proof seems to be the only program for which it cannot be solved, as it infinitely traces itself like a mirror. This same person also stated that if there was a halting machine, it would be magic because it would tell us hard math problems by telling us ahead of time if it's solver algorithm would halt.

The assumption in both of these cases is that the halting machine doesn't trace because there is no proof that it traces. However, in reality it actually does trace/ run the program it is run on with the input given.

The logical proof at least is simple. If it didn't need to trace at least the first step, it wouldn't need the input along with the program it's run on. In order to make any use of the information, it has to at least trace the first step before trying to analyze where that path is going.

The hard math problems mentioned in the top answer are ones where you cannot fast forward to figure out the answer, which means the halting problem would have to continue tracing until some pattern was recognizable.

So the only practical argument to get from the halting problem is that a halting machine can't determine the outcome of an optimized problem solver faster than the problem solver can finish.

Giving a formal proof for this reasoning is harder, and although I believe I could, attempting to explain it to anyone an academia will result in them throwing an ape like temper-tantrum and swinging from the chandelier. It's best just not to argue with those people.

Answer 7

here's the answer, it's yes, way back in 1967 from http://www.isp.uni-luebeck.de/kps07/files/papers/kirner.pdf

That the halting problem can be at least theoretically solved for finite-state systems has been already argued by Minsky in 1967 [4]: “...any finite-state machine, if left completely to itself, will fall eventually into a perfectly periodic repetitive pattern. The duration of this repeating pattern cannot exceed the number of internal states of the machine...”

(and so if you stick to finite turing machines then you can build an oracle)

Of course how long this takes is another question

Answer 8

is there a subset of programs that can be determined if they halt?

Yes.

Is it good enough for most programs?

Define "most".

Can I build a set of language constructs that I can determine the 'haltability' of a program?

Yes.

is there such a thing as nearly turing complete which is good enough?

Define "nearly".

Many folks write Python without using while statement or recursion.

Many folks write Java using only the for statement with simple iterators or counters that can be trivially proven to terminate; and they write without recursion.

It's pretty easy to avoid while and recursion.

---

For a given program in which all inputs are bounded can you determine if the program halts?

No.

If so what are the constraints of the language and what are the limits of the input set.

Um. The Halting problem means the program can't ever determine things about programs as complex as itself. You can add any one of a large number of constraints to get past the halting problem.

The standard approach to the halting problem is to allow proofs using a slightly "richer" set of mathematical formalisms than are available in the programming language.

It's easier to extend the proof system than it is to restrict the language. Any restriction leads to arguments for the one algorithm that's difficult to express because of the restriction.

The maximal set of these constructs would determine a language which can be deduced to halt or not. Is there some study that's been done on this?

Yes. It's called "Group Theory". A set of values closed under a set of operations. Pretty well understood stuff.

Answer 9

For many programs P, we can write a decider which halts on any input X, and tells us correctly whether P(X) halts or not. That is especially true for all programs with finite state. It is true for programs without loops, or with loops that have a structure that the decider is capable of analysing well enough.

An example: Let S be a state with a complete and discrete ordering and a smallest value. If S is initialised before the loop starts, and becomes smaller at each iteration of the loop, and the loop stops when the state is small enough, then the loop finishes and cannot stop P from halting. This allows to prove for example that the calculation of the big Ackermann function halts (in theory obviously. In practice the universe will be long gone before calculating A(4) would finish).

There are programs P where writing the correct decider takes some very hard maths, possibly beyond what we have now. On the borderline: I can easily write a program P where P(n) halts if n ≥ 0 and there are 0 < a < b < c such that $a^n + b^n = c^n$. Only quite recently there has been enough progress in maths to write a correct and very simple decider. (P will halt if and only if n = 1 or n = 2).

Note that a correct decider would have been possible without proving Fermat's last theorem. For example if someone had proved "there are no solutions with n ≥ 3 where a, b, c are co-prime and c > n^10000", that wouldn't prove Fermats Last Theorem, but would allow us to write a decider for the program P.