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

On Tue, May 04, 2010 at 09:37:46AM -0400, Prabhakar Ragde 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).  

Actually, he's proved that no programming language that guarantees 
termination can express all such functions.

-- hendrik