[plt-scheme] OT: not the halting problem, but what is it?

On May 4, 2010, at 6:49 AM, Sam Tobin-Hochstadt wrote:

> On Tue, May 4, 2010 at 9:37 AM, Prabhakar Ragde <plragde at uwaterloo.ca> wrote:
>> 
>> What you are doing is diagonalization, which as you point out is at the
>> heart of Cantor's power set proof, and at the heart of the proof of the
>> halting problem. The definition in step 2 ensures that the constructed
>> function differs from any enumerated function on the argument which is its
>> encoding. You've shown that there is no enumeration of total functions
>> int->bool (and thus no programming language can express all such functions,
>> even if the computational model guaranteed termination).
> 
> I think this just *is* Cantor's power set proof.  We've proved that we
> can't put N into a bijection with N -> B, which is just a
> representation of P(N).  But |P(N)| = |R|, so we've proved exactly
> what Cantor proved.

Right. What's curious to me is how this is applicable to the problem of programming, and how close it is to the halting problem, without having invoked computability or effectiveness or divergence or any of the things that I associate with the halting problem. 

John
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4669 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20100504/c766bd9d/attachment.p7s>