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

-----Original Message-----
From: plt-scheme-bounces at list.cs.brown.edu
[mailto:plt-scheme-bounces at list.cs.brown.edu] On Behalf Of Sam
Tobin-Hochstadt
Sent: 04 May 2010 17:04
To: John Clements
Cc: Prabhakar Ragde; plt-scheme at list.cs.brown.edu ML
Subject: Re: [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 
>>> int->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

-------------------------------------------

I don't think the relationship is coincidental. The fact that "does halt" or
"does have a normal form" is not decidible is, imho, a direct consequence of
the more general fact that there is no complete non trivial predicate.

Jos