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

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.
-- 
sam th
samth at ccs.neu.edu