[jkabrg]

Here's a way of thinking about the undecidability of the halting problem. Let's say you've got a person who's amazing at reading minds, and you bring someone off the street and tell them they can either have steak or a cupcake (but not both). You then ask the mindreader to decide if the person will have the cupcake or the steak. Conceivably, they might be able to figure out which one the person will have. Now let's say that you add a twist: you walk up to the person from the street and tell them what the mindreader predicted; in that case, the mindreader can't succeed because the subject can choose to do the opposite. That's similar to how the undecidability proof of the halting problem works.

Now instead of a mindreader, we have a halting oracle, and to make its job impossible we have a test program that is "made aware" of the halting oracle, and does the opposite of what the oracle says. Impossible problem for the oracle. But that then begs the question, how many potential applications of the halting problem will involve test subjects that actually know what the halting oracle thinks? How many test subjects even know about the halting oracle? For instance, how can a program that looks for counterexamples to the Goldbach conjecture know anything about your halting oracle? In these cases, the undecidability proof doesn't apply.

So the answer to your question is conceivably yes.

[colorint]

Yes, that was Turing's proof. Church's more indirect proof is that it's impossible to prove the equivalence of two lambda expressions. But the real essence of the problem is more like, you can't generally know ahead of time all the values that will be presented inside loop bodies. If you try to actually elaborate the loop then you get caught again: if the elaboration of the loop keeps going on for a while, the problem is re-presented, at what point do you give up? Which is to say, will this program, with these inputs, run forever? But this is basically Church's proof, since this is also the question, am I in exactly the same configuration as before? Without an ability to decide lambda expression equivalence, that question is also hopeless.

Hence the work that gets done in this area constrains the problem down to situations in which you can know enough to decide halting, like traversal of lists or trees that are known to be finite. I bring this up because, when it comes to AI, people want more than this.