Is it possible to solve the halting problem if you have a constrained or a predictable input?

The halting problem cannot be solved in the general case. It is possible to come up with defined rules that restrict allowed inputs and can the halting problem be solved for that special case?

For example, it seems likely that a language that does not allow loops for instance, would be very easy to tell if the program would halt or not.

The problem I'm trying to solve right now is that I'm trying to make a script checker that checks for the validity of the program. Can halting problem be solved if I know exactly what to expect from script writers, meaning very predictable inputs. If this cannot be solved exactly, what are some good approximation techniques to solve this?

Ken Li

Posted 2012-03-12T23:00:03.130

Reputation: 2 928

Answers

The intuitive answer is that if you don't have unbounded loops and you don't have recursion and you don't have goto, your programs terminate. This isn't quite true, there are other ways to sneak non-termination in, but it's good enough for most practical cases. Of course the converse is wrong, there are languages with these constructs that do not allow non-terminating programs, but they use other kinds of restrictions such as sophisticated type systems.

Recursion

A common restriction in scripting languages is to dynamically prevent recursion: if A calls B calls C calls … calls A, then the interpreter (or checker, in your case) gives up or signals an error, even if the recursion might actually terminate. Two concrete examples:

The C preprocessor leaves a macro intact while it is expanding that macro. The most common use is to define a wrapper around a function:
```
#define f(x) (printf("calling f(%d)\n", (x)), f(x))
f(3);
```
This expands to
```
(printf("calling f(%d)\n", (3)), f(3))
```
Mutual recursion is handled as well. A consequence is that the C preprocessor always terminates, although it's possible to build macros with high run-time complexity.
```
#define f0(x) x(x)x(x)
#define f1(x) f0(f0(x))
#define f2(x) f1(f1(x))
#define f3(x) f2(f2(x))
f3(x)
```
Unix shells expand aliases recursively, but only until they encounter an alias that's already being expanded. Again, the primary purpose is to define an alias for a similarly-named command.
```
alias ls='ls --color'
alias ll='ls -l'
```

An obvious generalization is to allow a recursion depth of up to $n$, with $n$ perhaps being configurable.

There are more general techniques to prove that recursive calls terminate, such as finding some positive integer that always decreases from one recursive call to the next, but these are considerably harder to detect. They are often hard to verify, let alone infer.

Loops

Loops do terminate if you can bound the number of iterations. The most common criterion is that if you have a for loop (without tricks, i.e. one that really counts from $m$ to $n$), it performs a finite number of iterations. So if the body of the loop terminates, the loop itself terminates.

In particular, with for loops (plus reasonable language constructs such as conditionals), you can write all primitive recursive functions, and vice versa. You can recognize primitive recursive functions syntactically (if they are written in an unobfuscated way), because they use no while loop or goto or recursion or other trick. Primitive recursive functions are guaranteed to terminate, and most practical tasks don't go beyond primitive recursion.

Gilles 'SO- stop being evil'

Posted 2012-03-12T23:00:03.130

Reputation: 39 868

See Terminator and AProVe. They tend to rely on heuristics, and I'm not sure if they clearly describe the class of programs for which they work. Still, they are regarded as state-of-the art, so they should be good starting points for you.

rgrig

Posted 2012-03-12T23:00:03.130

Reputation: 1 256

Not a formally rigid answer, but here it goes:

The problem in determining if it halts or loops forever. Looping on finite collections one element at a time or between an interval of numbers is ok. EDIT: Obviously, this will only work if the iterated collection or interval are prohibited to change (e.g., by immutability) when it is being iterated (or at least, prohibited to grow).

Recursion is probably not ok, unless if you set an artifical rule to make it finite, like allowing a maximum stack depth, or forcing that a non-negative parameter decreases in each iteration.

Arbitrary gotos are generally bad. Backwards-gotos are very likely to lead to loops that might be infinite.

Whiles and do-whiles statements are a problem, because they depend on a condition that is not guaranted to change or not during the execution. A possible (but probably very unsatisfatory) way to restrict that is to give a maximum number of iterations possible.

Victor Stafusa

Posted 2012-03-12T23:00:03.130

Reputation: 1 162

Yes, it can be possible. One common way of solving such problems is considering an extra (monotone) uncomputable parameter depending of the code as a part of input. The complexity of the problem having that parameter can be severely reduced.

We cannot compute the parameter, but if you know that the input instances you are dealing with have small parameter values, you can fix it to a small number and use the algorithm.

This and similar tricks are used in formal-methods to deal with undecidability of halting and similar problems. But if what you want to decide is complicated, the complexity of your algorithms is unlikely to be better than running the algorithm on those instances.

Regarding the other question, if you restrict the inputs enough, then the halting problem can be come easy. For example, if you know that the inputs are polynomial time algorithms, deciding the halting problem for them is trivial (since every polynomial time algorithm halts).

Problems that arise in formal-methods are typically undecidable, you may want to check the literature on how they deal with these problems in practice.

Kaveh

Posted 2012-03-12T23:00:03.130

Reputation: 20 985

You need to provide a definition of your script language, and what do you mean by "expect" from the script writers.

If the language is allowing only linear assignments and linear conditionals, then this halting is decidable in polynomial time (more or less ${\cal O}(n^\omega)$) by Tiwari's paper in my comment.

There is a similar result for a class of polynomial program by Aaron R. Bradley, Zohar Manna and Henny B. Sipma. But AFAIK (I might be wrong here) the runtime is doubly exponential (essentially the time required to compute a Groebner basis).

user20

Posted 2012-03-12T23:00:03.130

Reputation: