General Halting Problem Problem

[[What follows below is simply misunderstanding about the Halting Problem and the proof that it is undecidable. Instead of P and Q, below, let me use Halt for the alleged program (of one argument) that solves the Halting Problem, and Spoiler the program (of zero arguments) that shows that Halt cannot work. It is a plain and simple result that Spoiler will cause Halt to fail. That is unavoidable. If you want, you can take the text of Spoiler, and incorporate it into another program Halt1, which tests to see if its input is the program Spoiler. But that program Halt1 will have its own Spoiler1. There is, quite simply, no way to avoid this. It simply does not matter what sort of examination Halt makes of its input tape, or whatever. Spoiler takes Halt as given, and is constructed to make Halt fail. That's it. End of story.

Nor are the attempted objections to the misunderstanding relevant. Even if Spoiler includes the text of Halt directly in some sense, Halt will not be able to exploit that fact. Spoiler is constructed by definition to make Halt fail, the proof that it does so is simple. There is no need to invoke an "obfuscated" version of Halt inside a virtual machine to thwart it. In fact, the problem of whether or not an obfuscated version of a program is equivalent to the original version is also undecidable (it is the problem of program equivalence), but this fact is proven by reducing the halting problem to the problem of program equivalence, not vice versa.

But ... there is apparently an even more basic misunderstanding which has to be addressed, because of the potential mechanics of Turing Machines and how they might be put together

It was to clear up this misunderstanding that the argument about an "interpreter" was invoked below. Let's summarize it up here. It relies specifically on Turing Machine formulations of the problem. Halt is defined so that, on a tape that contains nothing but a description of a 0-argument Turing Machine, it runs and leaves a tape which contains only a 0 or a 1, depending on whether or not the given Turing Machine halts on an empty tape. (This is all without loss of generality, I think everyone can agree.). The alleged refutation relies on the fact that when Halt is run, it need not assume that the tape is empty except for its own input. The tape may contain some other markings that a containing program, such as Spoiler, has placed on the tape. It is alleged that by examining these markings, Halt can alter its output to get around the problem Spoiler presents it with. But this is quite simply false. This is where the "interpreter" comes into play (not to obfuscate, as I thought was being suggested, but) by preventing the version of Halt contained within it from accessing anything outside what it would be able to access had it been started under normal conditions. In fact, it is not Halt that is contained within Spoiler, but a lobotomized version of it that forces it to work only on the Halting Problem and not anything else weird involving going outside its own input. It may be objected that this is not fair, restricting Halt in this way, but of course it is totally fair, because there is no obligation to include Halt inside Spoiler. All that is required for the simple proof to go through is a program that is input-output equivalent to Halt when it is started on as tape containing nothing but the program whose halting status it is supposed to ascertain. An "interpreter" of some form may be required to do this (such as one that simulates that otherwise empty tape, even while the program doing the simulation writes other stuff on the "real" tape). But the key is that the modified Halt, contained as a subroutine in Spoiler, is input-output equivalent to the original Halt on the actual problem that was given to the original Halt. It is irrelevant that it is not input-output equivalent on some other strange problem.]]

[[Uh, no. There is no need to be concerned with the undecidability of program equivalence here. There is no need for "uncrackable" anything, whatever that means, and certainly the version of Halt used by Spoiler (Halt') is more than "any source that expresses the same function" as Halt (how would one find such a thing if not as a provably equivalent minor modification of Halt itself?) It is in fact essentially Halt, but Halt restricted to run on a tape that it was required to be designed for. Note that Halt must be able to run on a tape that starts with nothing on it but a representation of the program it is required to test. It may contain some extra code to look elsewhere on that tape in order to see if it is "being tricked", however, it must be able to solve the Halting Problem without applying that code, in the circumstance that it is started normally on a tape containing only its own input. It is thus a simple matter for Spoiler to take the tuples defining Halt, and alter them so in effect they are running on a virtual tape/head combination, instead of the real tape/head (which is simulating them), and, most importantly, deliver the same answer as would be delivered by Halt running on the real tape/head combination, which, by the claim of its author, has input/output behaviour defining the Halting Problem, and which is the minimum anyone claiming to solve the Halting Problem must be able to provide. Given this using of the simulated Halt, which has input/output behavior equivalent to the original Halt, it is the usual simple proof to show that Halt applied to Spoiler cannot deliver a consistent result.

You know, computability theory is a highly developed and very interesting discipline. Do you really think you have found some problem at the very basis of it that renders all of the deep and complex results (such as those describing the highly complex structure of the recursively enumerable degrees) somehow flawed? Perhaps you should have a little less hubris. I see this has all been explained before, below, although perhaps the explanation that stays at a more concrete level (keeping always in mind that we are dealing with concrete Turing Machines, not lisp machines, abstract environments and interpreters not directly reduced to Turing Machines, etc) may be more helpful. But maybe nothing is helpful for a troll?]]

Brand new semi-humorous argument: my machine P is both a GeneralHaltingProblem solver and also good at inferring the intent of its input. When invoked as Q's inner loop, P will examine its input (source of Q) and immediately realize that it (P) is being used in a misguided attempt to prove that it (P) cannot actually exist. It (P as Q's inner loop) will consequently print "0" - causing Q to halt - while simultaneously adding states to its (Q's) FSM which, when inspected by the outer invocation (P), explain the subterfuge, permitting it - the outer invocation of P - to assert the correct halting value. Which is, correctly, "1".

Please email the Nobel to Pete@that-place-I' Thanks!

But seriously, where's the logic error above?

You're brilliant, Pete, but you just overstepped the limitation of Turing Machines. Programs for TM are deterministic, and therefore two runs of the same program for the same input cannot give different results.

If we allow for non-determinism, then, yes, you can make a program P that somehow (magically) distinguishes when it is run from the supervision of Q and does whatever trick it needs. But then, you haven't disproved the HaltingTheorem because such a program cannot be constructed in TMs. So, you don't get the Nobel.

 ;assume we have a program p
 ;without side-effects, in Scheme
 (define p (lambda (x) <body-of-p>))

; and p solves the halting question for a program x returning ; true if (x) halts and false otherwise.

; then we define the program q (define (q) ( if (p q) (loop-forever) #t)) ; and if p doesn't have side-effects (it is purely functional) ; then (p q) should yield the same result in all context, ; and it is easy to see that ; (p q) = true implies q loops forever

; Now the inventive Peter, will protest that q has access to an environment ;(which makes the recursive invocation (p q) possible, so then if p has access to the ; environment than p can distinguish the places of invocation ; therefore the only technical trick to be done is to de-recursify q, ; remove all access to the environment while keeping it a program equivalent with the above, ; To do that we use a fixed-point combinator like the U ; (define U (lambda (f) (f f)))

; we can then define q as (define q (U (lambda (f) (if (p f) ((lambda (x) (x x))(lambda (x) (x x)));loop forever #t)))) ; now we eliminated the recursion while keeping q the same ; let's inline the lambda expression for U and p ; let's inline the lambda expression for U and p (define q ((lambda (f) (f f)) (lambda (f) ( if ( (lambda (x) <body-of-p>) ;p actually, applied to (f f)) ; applied to (f f), which is actually a stand-in for q, ; then ((lambda (x) (x x))(lambda (x) (x x)));loop forever ; else #t)))) ;therefore if <body-of-p> exists with the above property, ;there exists the lambda expression denoted by q ;and evaluating ((lambda (x) <body-of-p>) ; p applied to ; q unrolled ((lambda (f) (f f)) (lambda (f) ( if ((lambda (x) <body-of-p>) (f f)) ((lambda (x) (x x))(lambda (x) (x x))) #t)))) ;we reach the conclusion that body-of-p cannot ;exist with the specified properties

 (define q (if (scheme_interpreter '(p q)) 

In any case, you guys can quit your crowing on the A-machine. Costin is, above, assuming the existence of an interpreter that can't be cracked. Let's call it I. If you'll kindly refer me to a proof that such an interpreter can exist, then you're out of the woods. To forestall the usual squawking, no, I don't know that you can't prove such a thing - but the burden of proof remains with you. It sure doesn't smell recursive ... -- Pete

Ahem, I beg to differ, Pete. If we restrict the discussion to a purely functional subset of Scheme, then such interpreters of a functional subset of Scheme are written by students around the globe all the time. That they cannot be "broken" follows trivially from the semantic of Scheme: if all the primitives (car,cdr, define, let, if` etc) are deterministic, and all the composition constructs are deterministic, it follows by structural induction that all constructed procedures are deterministic so that evaluating the same expression in any correctly implemented interpreter will always yield the same result.

In principle, of course, I agree. Or else I would have popped up a counter-example. But a specification is not a proof; you'll need to start by proving that each of these primitives cannot be cracked, then show that their principal of combination cannot be cracked. Given RicesTheorem ( this is not a trivial undertaking. At each step you risk the AntecedentAssumedFallacy. This is why I say the uncrackable interpreter smells non-recursive.

Mapping from a purely functional subset of scheme to lambda calculus is also a beaten path, so if you want a full-blown interpreter to be presented to you as part of the proof, you'd better give us some good reason rather than asserting the burden of proof on the other side. Because it's surely boring to write down that interpreter and it provides no insight into the HaltingProblem whatsoever. A quick reference could be SiCp, but examples of such interpreters are so many, I don't know where to begin.

I don't actually expect you do any such thing. It sounds like a frightful waste of time. But until you or someone does, the A-machine version of the halting problem remains cracked. And then as Doug points out most likely TM != LC.

There's a valid conclusion to be drawn that maybe TM are not as good as real computers (those can do all kinds of non-deterministic tricks, like being connected through networks, running MS Windows, or using non-ECC memory :) ), but then the stuff that we need TM for can be adequately modeled using TM.

Even more serious than CC's critique: there's no Nobel prize in math. There's the Field's medal, but you may be a bit long in the tooth for that.

Yes, apparently a mathematician raced off Nobel's wife. Strange thing, science ;-) Keep in mind that Turing's original machines are far from the only model of computation ever studied. Machines with oracles are non-deterministic, for instance, and there are also randomized machines, which do indeed have different performance. For instance, the computational complexity of some algorithms depends on whether the Extended Riemann Hypothesis is true, which no one knows is true or not - however, such algorithms can typically be converted into the faster computational class simply by using randomness, which doesn't exist in the original Turing machines. It's a pretty big topic, and TuringMachines are simply a starting place. -- Doug

The most fundamental plank of ComputerScience is the General HaltingProblem. Unfortunately there appears to be a problem with the GHP, as follows:


I don't have any such program P and anyone else who says they do is full of it.


Realizing this, it's plain that the whole form of the proof is identical with the convict's invalid reasoning in the UnexpectedExecutionParadox. All the computability results that rest on the GHP are therefore null and void, and we better start over on this topic. Oh, another Nobel for me? Pesky things, I keep tripping over 'em. -- PeterMerel

I can't quite tell whether this is a joke or not. Assuming it's serious (DeleteMe if it's just a joke): There is no fallacy. Here's one way to adjust the proof that may make it clearer that there is no fallacy.

Hence, we've shown that no program P can be a halting tester in the precise sense described by that statement. And we haven't had to assume that any program is a halting tester in order to do it. We started with any candidate program, and produced a new program for which it doesn't give the right answer. -- GarethMcCaughan

I expected this semi-humorous argument to go down in flames, but couldn't quite put my finger on why just yet. Anyway you're quite right, many thanks. A more serious if exformal objection is raised on WhatDoesHaltingMean and discussed on GeneralHaltingProblemProblemProblem, suggesting that InfiniteLooping is in fact exactly what halting means. Ergo Q can not fail to halt, and the Turing fence is down again ... -- PeterMerel

The clearest technical book on the subject that I've ever seen is The Language of Machines - An introduction to Computability and Formal Languages by Floyd and Beigel, ISBN 0716782669 . Obviously, these things cannot be adequately covered non-technically/non-mathematically. -- DougMerritt

Here's a program (in an imaginary language, for an imaginary machine) that might explicate things.

 # ALLEGED_TESTER is a function which accepts a single argument.
 # We return a new function F that proves that ALLEGED_TESTER isn't
 # a perfect termination tester: in other words, either F terminates
 # and ALLEGED_TESTER(F) doesn't return 1, or else F doesn't terminate
 # and ALLEGED_TESTER(F) doesn't return 0.
 def thing_not_tested_validly(alleged_tester):
   def f():
     tester_result = alleged_tester(f)         # same f as we're now defining
     if tester_result == 1 then loop_forever()
   return f

Proving the assertions in the comments there is easy. If ALLEGED_TESTER(F) returns 1 then F loops for ever. If ALLEGED_TESTER(F) returns something other than 1 then F doesn't loop for ever.

If you're bothered by the "same f as we're now defining" thing, don't be: there are ways of working round that. But this is one of the subtle points of the proof. -- GarethMcCaughan

What is wrong with the first proof? It's proof by reductio ad absurdum. To prove that P can't exist you assume P does exist and make it lead to a false conclusion, given your knowledge base.

If you do away with this kind of proof you do away not just with the GHP but with most of mathematics too. :-)

Nothing is wrong with it. I provided the second one because I thought it might evade some mental blocks. It might be worth mentioning that a similar thing can be done to many proofs by reductio ad absurdum, for the sake of those who find RAA hard to trust. -- GarethMcCaughan

Let me know if I get this:


What this is really telling me is that there's no way to actually completely test a program except by running it. -- CristiOpris

Yes, that's the idea. It's a proof that actually we don't have a program P that tells whether things terminate or not. And it's even worse than you say :-), because even running a program can't prove that it doesn't terminate. -- GarethMcCaughan

Yes, the "general halting problem" proof is one that is commonly given in college courses. (At least it was in the early '80s. ;-)

But I think it's flawed.

Briefly, to know if Q halts, you need to know its input. Its input is Q, but to know if that Q halts, you need to know its input. So, you're really testing this:
  Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q(Q( ... ))))))))))))))))))))))))
Where there's an infinite number of Qs.

The definition of the thing you wish to run doesn't halt, so you can never get to the point of running it. -- JeffGrigg

Ahhh, yes: THAT is the approach I was looking for. Thanks, Jeff! -- TomStambaugh

No, what you input to Q is the "source code" of Q, so no need to get all recursive here.

No, there's no way to know if a program will halt or not unless you know the input. Consider this program: { if input = "halt" then halt else loop_forever } Now, does it halt or run forever? You can't know if it halts unless you know if the input is "halt".

So, to evaluate if Q halts, you have to know its input halts. That input would be Q, so...

Yes, but the input to Q is not the result of executing Q, it's nothing at all. Here's a slightly reworded definition that makes that a little clearer: -- GavinLambert

I think the problem might be relating to the definition of 'input'. I'd say that, although there is no explicit input to 'Q()' (according to the signature), there is an implicit input, in the form of the call to 'P' ('Q' asks for input from 'P'). With that call, 'P' ends up having to analyse itself with the associate input of 'Q'... and now we've got a problem.

As an aside, there would seem to be no reason that 'Q' couldn't detect the situation, that it has processed itself multiple times, or even processed itself at all, and therefore respond to the question with a question, so to speak: "Does 'Q' halt? I don't know... do you want it to halt?"

-- WilliamUnderwood

OK, so suppose we have this program "R" which can analyze an input and halts if the input is equivalent to itself...

"Does 'Q' halt? I don't know..." Well if 'P' doesn't know then it isn't solving the halting problem. If you ask the question "does this program halts?" and for some programs like 'Q' you are forced to answer something else than 'yes' or 'no', then Turing is right: you cannot write a program which can answer that question with a 'yes' or 'no' for any given input program. -- Samuel Gélineau

To break down what I see as the problem here, at least on the top part of the page, the proof is this: "Even if you had a halting predictor, you don't have a halting predictor. I can do this for all putative halting predicters." To put something else in that form, "Even if you think you have an integer that is greater then all others, I can prove that your integer isn't greater then all others (by simply adding 1 to yours). I can do this for all putative largest integers."

Your inability to produce the integer that is greater then all others isn't a problem. I never really depended on your specific integer, I made a statement about all of them, by showing concretely that each and every one of them is inadequate. -- JeremyBowers


Assuming that a program could be defined which can recognize itself as input:

From any halting detector, you can provide a program which halts or not based on the opposite of the decision of that detector.

And for any such program you provide me which does that, I can provide a program which can detect trickery of that specific nature.

We can't solve the halting problem in general, but we can get as close as we'd like.

Now, "Can this result be made useful?" is a completely different question.

-- WilliamUnderwood

P.S., where n = the biggest number you can quote to me, the number returned by (n+1) is the largest integer. Prove me otherwise :p (n+1)+1 - I don't think you really understand mathematical symbology. Anything goes in those variables, not just pure numbers.

It is well known that it is, on the other hand, feasible to solve the halting problem for all machines up to size K, for any given finite constant K you care to name. The machine that solves that particular finite K-halting problem will be bigger than K (O(2^K) does it nicely). Unsurprisingly, the class of machines it can solve does not, therefore, include itself. -- dm

Hence the answer of "I don't know. Find a bigger machine." :)

Also, yes, it is useful. Many proof techniques are based on exhaustive examination of state space for things that are equivalent to solving the halting problem. Since the state space is finite, it is sometimes feasible, whereas in the general case it clearly isn't. This is another critical thing to understand about the Halting Problem non-Problem: It specifically refers to the general case, and does not apply in less general cases. Though even in the less general cases it does tend to imply an irreducible exponential cost. -- JeremyBowers

Why need a "Halting Predictor" to prove the point...

How about "Is it possible to predict the output of the function f(int i){return i;}"? The function takes an int (let's say only 0 or 1) and spits it out. It is not possible to tell exactly what it spits out, whether a 0 or a 1 (without knowing the input). Doesn't this qualify as a "proof" that it is not possible to predict the output? If NO (it doesn't qualify), then how different is the "Halting Problem" from this one other than to disguise the input and output in some fancy programmer's formalism? -- Mohyneen Mehdi

You don't necessarily need something fancier, but you do need to consider all possibilities one way or another. You're basically assuming the result you want to prove; that's why this is not a proof.

Maybe I am missing something or maybe I am not, but I can't give in to the "circular reasoning" that lurks in the proof of the Halting Problem. In standard English, the solution goes like this... P has the task of predicting Q's output (or behavior). But Q has the final say in the matter and waits till P makes its prediction, after which Q conveniently adapts its behavior only to violate that prediction.

So, as I see it, P has to look at "Q AND Q's Input" in order to predict its behavior (or output). But Q's INPUT is P's OUTPUT. So, effectively, P has to look at "Q AND P's OUTPUT". But P's OUTPUT is obtained only by looking at "Q AND Q's Input". Back to square one! It's important to understand that by Q's INPUT I don't mean Q's parameter values; I mean information that Q eventually uses to behave the way it does.

P needs information which is obtained from Q, who in turn needs the "same" information from P. But according to the proof, that information is generated on the fly and P is given the credit (or discredit) for generating it. That information (i.e the prediction P makes) couldn't have been generated because P doesn't know Q's complete Input information, information which can come only AFTER P makes it's prediction (i.e the prediction itself).

Where exactly am I going wrong?

-- Mohyneen Mehdi

Here's how I see it: Q's input doesn't have to be a precalculated boolean value equal to P's output. P is supposed to (among other things) look at its own source code and figure out for himself what P's output is supposed to be. If P wants to execute this code in order to find out then P will loop forever, won't ever give an answer for this particular program, and cannot solve the HaltingProblem in general. If P chooses to guess Q's input without executing its own source code, then whatever his guess will be he will give a wrong final answer about Q, so P still isn't solving the HaltingProblem in all cases. -- Samuel Gélineau

Where exactly am I going wrong?

There's several common spots of confusion. Maybe you can help us re-state or otherwise explain the problem so it's less confusing. (But I don't think there's any way of getting around the contradiction, since it's a proof-by-contradiction.) Confusion between what people mean by Q: Other people are mislead into The same sorts of confusion have led many people to claim that QuinePrograms are impossible, when clearly several do exist.

Also, a few of the "proofs" of FreeWill seem to be based on the same confusion.

P needs information which is obtained from Q, who in turn needs the "same" information from P.

Yes, sort of. When P runs, it inspects the source code for Q, and also inspects the input that will be fed to Q.

Please note that P does not actually call() or eval() or execute Q. (Although the sorts of analysis it does are probably very similar to the sorts of analysis that go on when the compiler compiles and partially evaluates Q when we later compile Q).

But according to the proof, that information is generated on the fly and P is given the credit (or discredit) for generating it.

Yes, exactly.

That information (i.e the prediction P makes) couldn't have been generated because P doesn't know Q's complete Input information, information which can come only AFTER P makes it's prediction (i.e the prediction itself).

I think you're very close to understanding the HaltingProblem.

In this case, P *does* know Q's complete input information. Tell me the source code to P (long before you ever *compile* P), and I can tell you the long string that makes up Q's complete input information. It is, in fact, the source code to Q (which includes a copy of the source code to P that you gave me).

Say I want to know whether this function halts (i.e., whether it is an algorithm), and if so what value it returns:

  int count_apples(){
    int left = count_apples_on_left();
    int right = count_apples_on_right();
    return( left + right );
By "input", we normally mean input from *outside* the computer. The value returned by count_apples_on_left() does *not* count as "input". I inspect that function and see that it calculates a value without any input from *outside* the computer. Say I run count_apples_on_left() once and it returns "17". I can be confident that it will return "17" every time I or anyone else runs that subroutine. Right?

So, what does count_apples() return? Or does it never halt?

I inspect count_apples_on_right(), and I see that it reads in 2 characters from standard input. Those 2 characters count as "input", not just to count_apples_on_right(), but to any program that calls it (such as count_apples() ), and to any program that indirectly calls it (perhaps by calling count_apples() ).

If I know what those 2 characters will be, do I have any hope of figuring out the output of count_apples()?

I just came to read here; correct me if I misunderstood something.

For halting property, there are three kind of program. Halting problem states that (I took this from first line in HaltingProblem)

"It is impossible to write a program that runs in finite time that is able to decide whether an arbitrary program will halt (with a certain input)."

Let P be the halt tester program, and Q be the program that will be feed to P, and go in infinite if P return "Q will halt", and halt if P says "Q never halts"

Now the statement With a certain input is where the flawed is.

What is the input to first Q that is fed to P?

''The input is empty, or a dummy string, it does not matter at all. As a matter of fact you can consider the input to be part of the program, and that settles all the useless discussion about input. You cannot define a program P that decides for all programs if they halt with an empty input.The counter-example Q defined by
   (define (Q) (if (eval '(P Q)) (loopforever) true))
settles it. If you notice, Q does not use any input at all. So the input can be anything, it's better left out of the picture.

Technically Q is often constructed along the lines
  (define (Q X)  (if (P X X) (loopforever) true))
And the counter-example is that P cannot decide for
 (P Q Q)

Which is more faithful to the original formulation of the halting problem where P had to have 2 arguments (P X I) where X is the program and I is the input. But this later arrangement, while valid, makes it less intuitive, as the reader is distracted by the artifice of using Q both as program and input, and by the role of the dummy variable X in the body of Q. So reducing the problem to programs with empty input, makes the intuition much more accessible. So we prove that we cannot even construct a program that decides the termination of all programs with an empty input.

I took the liberty to delete the flawed discussion about the lookup tables, and the relative sizes of programs and lookup tables. It just distracts from a technically trivial proof. -- CostinCozianu

I don't see why you did so. I said explicitly that it was the starting place for one of the classic approaches to proofs, which I was trying to lead up to one step at a time - maybe not one of the proofs that you prefer, but I don't see why that's reason to delete it. It's possible that your explanation will be better understood by the current audience, but even that is hard to say - obviously, many people do not find the topic clear even when I think it's clearly presented (and yes, I think your statements are clear). I mean, I do see your point that the topic should be simpler, the way you presented it; the question is, will your audience get it. If they do, cool. -- DougMerritt''

I just reread the above and I see specifically what was subconsciously bothering me. I do not think you were clear in the critical part, the conclusion: "And the counter-example is that P cannot decide for (P Q Q)". I think you need to do something to make that much more glaringly obvious, or else your "simplified" approach won't get the point across. -- Doug

But that was exactly the point: that if we discuss about a program/procedure say P2 that takes 2 parameters: (P2 X I), we make it far less obvious to come up with (Q2 X) that evals (P2 X X) and turns the result on its head. Instead if we focus just on P1 that takes input a program that runs with an empty (or otherwise fixed) input then we construct Q1 that evaluates (P1 Q1) and turns it on its head. So assuming a purely functional subset of Scheme, the proof is:

 ;Proof 1
 ;assume there is a P1 that decide termination for procedures with no parameters
  (define (P1 X) (...))
 ;where  forall X, (P1 X) evaluates true if (X) halts, false otherwise [1]
 ;construct the function with no parameter 
  (define (Q1) (if (eval '(P1 Q1)) (loopforever) true)) ;[QDEF]
 ; then 
 ;  if (P1 Q1) evaluates to true, it follows according to [QDEF] that (Q1) loops forever , contradicting [1] --  -- {step A}
 ;  if (P1 Q1) evaluates to false, it follows according to the definition of Q1 that (Q1) terminates , contradicting [1] -- [step B]
 ; therefore because (P1 Q1) cannot evaluate to either true or false without contradicting [1]
 ; the assumption that there exists P1 leads to a contradiction and is therefore false (reductio ad absurdum)

This is the complete sketch of the proof about the non-existence of a Scheme procedure P1 that can decide for all Scheme procedures with no argument if they terminate or not. Using code in a real language makes it easier to follow, while keeping it reasonably formal. If on the other hand we try to prove the version with (P2 X I), coming up with [QDEF] and verifying [step A] and [step B] is less intuitive:

 ;Proof 2
 ;assume there is a P2 that decide termination for procedures with one parameter ("input")
  (define (P2 X I) (...))
 ;where  forall X, (P2 X I) evaluates true if (X I) halts, false otherwise [1]
 ;construct the procedure with one parameter 
  (define (Q2 R) (if (eval '(P2 R R)) (loopforever) true)) ;[QDEF]
 ; then 
 ;  if (P2 Q2 Q2) evaluates to true, it follows according to [QDEF] that (Q2 Q2) loops forever, contradicting [1] -- [step A]
 ;  if (P2 Q2 Q2) evaluates to false, it follows according to the definition of Q2 that (Q2 Q2) terminates, contradicting [1] -- [step B]
 ; therefore because (P2 Q2 Q2) cannot evaluate to either true or false without contradicting [1]
 ; the assumption that there exists P1 leads to a contradiction and is therefore false (reductio ad absurdum)

So I think that it is clear that Proof 2 is both harder to follow and harder to remember at a later time than Proof 1, and this responds directly top the anonymous contributor's question as to what happened with the input for Q. There is no input, and I presented the justification why it is better to look at the version with no input.

Now for GoldPlating we can tighten some details by to replacing recursion with a fixed-point combinator to make the proof adequate for the halting problem within LambdaCalculus {there's no lambda expression P so that for any other lambda expression X the application (P X) reduces to "true" (aka (lambda (x y) x) ) if X has normal form, and to "false" if X doesn't have a normal form }. Because LC and TM are known to be computationally equivalent this is as good as a proof of the halting problem for TM.

BeingRefactored? See HaltingProblemDiscussions

Potential New Pages: See for a really understandable, and funny halting problem proof.
CategoryProof CategoryCoding

View edit of November 23, 2014 or FindPage with title or text search