Re: Confused, was Re: functions that halt
From: Kent Paul Dolan (xanthian_at_well.com)
Date: 05/12/04
- Next message: dmerony: "Re: Are there any non-gifted scientists?!?!?"
- Previous message: |-|erc: "Re: PROOF that numbers are countable"
- In reply to: Arthur J. O'Dwyer: "Confused, was Re: functions that halt"
- Next in thread: |-|erc: "Re: Confused, was Re: functions that halt"
- Reply: |-|erc: "Re: Confused, was Re: functions that halt"
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Date: 11 May 2004 20:54:19 -0700
"Arthur J. O'Dwyer" <ajo@nospam.andrew.cmu.edu> wrote:
> Sorry if I'm missing something obvious here, but
> isn't the following a proof that we *can*
> enumerate all halting programs in a list?
I don't think so.
> I agree that we can't produce a demonstrably
> complete list in finite time, but that's obvious;
> there are infinitely many programs on the list in
> any case.
I think it's a bit worse than that.
> Lemma 1: There are countably many programs.
OK.
> Lemma 2: We can produce a program that accepts all
> halting programs. [Simply, in ML syntax: fun
> DoesHalt(P) = (P() ; true) In other words, run
> the program and return 'true' whenever it
> finishes.]
That's not good enough, because we still have no
decision procedure that lets us say the program does
_not_ halt; in other words there is no point short
of infinitely many steps at which we can safely say:
this program doesn't halt. "Waiting an infinite
time" doesn't work, that's the problem Russ Easterly
is always stumbling over to produce all his "proofs"
in contradiction to known results. You just can't
_say_, in a proof, "do this procedure step by step,
and then *do something with the result* _after_ an
infinite number of those steps; that point never
arrives.
> Lemma 3: Given countably many programs, we can
> produce a program that will execute all of them
> that halt, to completion. [Proof similar to the
> countability of the union of countable sets, I
> think. We run the first program on the list for
> one second, then the first two programs on the
> list for one second each, then the first three
> programs for one second each, then the first
> four...]
Nope, that's worse, squared. After any finite number
of seconds, there are still infinitely many programs
that _do_ halt that you have not yet even _begun_ to
test.
> Theorem: We can produce a program that enumerates
> all halting programs. [Simply produce a list L of
> *all* programs, by Lemma 1;
Nope, Lemma 1 says that they are countable, not that
you can produce a list (i.e., an _ordered_ list) of
them; just like the rational numbers, they are
countable, and have an order relationship
("arithmetically less than" for the rationals,
"lexicographically less than" for the programs) but
still cannot be listed in any totally ordered list,
by the usual diagonal argument in each case.
> then, using Lemma 3, run the list of programs
> DoesHalt(L) to completion.
Can't do that, even in concept.
> Every time one of the programs DoesHalt(L_i)
> returns 'true', print out program L_i.]
> OTOH, we can use a diagonal argument to show that
> if we *had* a list H of halting programs, we could
> take the program fun Contradiction(i) = ~H_i(i)
> which would halt for all inputs, but not be on the
> list.
> But my first argument shows that we can compute
> H_i in finite time simply by waiting long enough
> --- thus Contradiction also exists!
> What's wrong here? Now I'm *really* confused!
The same problem Russ has; you cannot take the
*results* of a process with an infinite number of
steps as input to a "next" step; you never get to
that "next" step.
xanthian.
I tried to write that in plain language, which
surely means it is broken somewhere, but I hope
I got across at least the flavor of the correct
argument.
- Next message: dmerony: "Re: Are there any non-gifted scientists?!?!?"
- Previous message: |-|erc: "Re: PROOF that numbers are countable"
- In reply to: Arthur J. O'Dwyer: "Confused, was Re: functions that halt"
- Next in thread: |-|erc: "Re: Confused, was Re: functions that halt"
- Reply: |-|erc: "Re: Confused, was Re: functions that halt"
- Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Relevant Pages
|