[plt-scheme] OT: not the halting problem, but what is it?
Looks like Gödel numbering, afaics. It's called incompleteness.
See for example:
http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems
Jos
-----Original Message-----
From: plt-scheme-bounces at list.cs.brown.edu
[mailto:plt-scheme-bounces at list.cs.brown.edu] On Behalf Of John Clements
Sent: 04 May 2010 06:55
To: plt-scheme at list.cs.brown.edu ML
Subject: [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