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

John Clements wrote:

> 1) As our model of a programming language, consider an injective mapping E (for "encoding") from the integers (a.k.a. the "programs") to functions in (int -> bool) (a.k.a. the "meanings"). Note that I don't claim that this map is a total function, or that it's surjective. There's also no "bottom" needed in this model. Also, I'm referring to real mathematical functions, and not their computational approximations.
>
> 2) Next, consider the set of numbers for which (E(n)) (n) returns true.  That is, the numbers that represent functions which when called with their "program" form return true.
>
> 3) This set can be represented as a characteristic function, m, (in (int -> bool) that maps n to false when it's a member of the set described above, and otherwise produces true.
>
> 4) Q: Is there some number p such that E(p) = m ? That is, is there a program 'p' that corresponds to the meaning 'm'?
>
> 5) No, there can't be, for the usual paradox reasons. (If there were such a number, then if E(p) (p)  = true then it belongs to the set and therefore E(p) (p) = false, and if E(p) (p) = false then it doesn't belong to the set and thus E(p) (p) should return true.)

Usually a characteristic function of a set produces `true' for elements 
in the set and `false' otherwise. So you would want to, in step 2, 
consider {n | (E(n)) (n) = `false'}.

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). 
--PR