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

WARNING: UNRELATED TO PLT SCHEME

While I was out riding today, I came up with a formulation of something extraordinarily close to the halting problem that's entirely independent of halting, computation and decidability, and that is essentially a restatement of the cantor theorem (power set of A is bigger than A).  I'm confident that many people in the world can tell me swiftly whether this is well-known or incorrect and how it fails to lead to the halting problem, and optimistic that one of them is reading this message and inclined to answer it.

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

What's the interpretation of this in computing? That for any programming language as defined here with at least two possible outputs, the program that determines whether another program produces one of the two values *when called with its own representation* is inexpressible in the language.

Note that (unlike the proof on the wikipedia page :)) this proof has nothing at all to do with halting, and doesn't even require a model of computability / turing completeness / whatever.  In essence, it's just a restatement of the theorem that you can't put the programs (ints) into correspondence with the meanings (functions from ints->bools, a.k.a. the power set of the ints).

The only gap between this and the halting problem, AFAICT, is that it applies only to the expressibility of the function that computes whether a program produces true when called with itself, and not the expressibility of the function that decides whether a program produces true when called with, say, 4. In most of the pop proofs of the halting problem that I've read, this difference is glossed over, but it now appears to me that *this* is the point where you actually have to bring in the big heavy machinery so that you can talk about reducing the problem of determining programs' behavior on 4 to their behavior on their own representations.

Am I missing something obvious? 


Lonely in rural CA,

John Clements

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