Thanks! OT ist TOT. (was: Re: [plt-scheme] OT: not the halting problem, but what is it?)

On May 4, 2010, at 8:03 AM, Sam Tobin-Hochstadt wrote:

> On Tue, May 4, 2010 at 10:50 AM, John Clements
> <clements at brinckerhoff.org> wrote:
>> 
>> 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.
> 
> I don't think it's really that close to the halting problem.  There's
> two ways that it might be related to the halting problem: it uses a
> diagonalization proof, and it shows an inexpressibility result for
> programming.  But countability arguments  (which is what this proof
> is) show lots of things to be inexpressible (for example, almost all
> reals are not computable), and diagonalization is a general proof
> technique.
> 
> Fundamentally, this proof is an instance of the fact that there are
> many fewer programs than characteristic functions on programs.  It
> happens that the "does it halt" predicate is a characteristic
> function, and that it is one of the many such characteristic functions
> that are not computable.  But I think that's a mostly coincidental
> relationship.

Thanks! That makes a lot of sense.

(I'm now returning you to your regularly scheduled life.)

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/a47cb1ad/attachment.p7s>