John, (01)
On Mon, Feb 8, 2010 at 10:30 AM, John F. Sowa <sowa@xxxxxxxxxxx> wrote:
>
> RF> But we have to remember there are at least some properties
> > of computable processes which are not specified, other than by
> > running the process itself.
>
> That is no different from running a theorem prover on the axioms:
>
> If you have a program for which the halting problem is undecidable,
> the program will loop forever.
>
> If you try to determine whether the program will halt by starting
> with the axioms, your theorem prover will loop forever.
>
> That makes the two different specifications -- the axiomatic and
> the procedural -- identical in meaning ... (02)
You can think of the axioms as specifying an answer, it's true. But
what use is that "answer" if you will have no access to it until the
theorem prover halts. If it always halted the difference would just be
one of time. But if it may never halt? (03)
The actual non-halting case is only of theoretical interest. An
infinitely looping program is not of much practical use. (04)
It becomes more interesting when a process does halt. Say, there may
be specific conditions under which one or other axiom applies. (05)
What the halting "problem" tells us is that you cannot simply list
these true and untrue cases. You might have to go on forever waiting
to see if your process halts and you can add another case to your
list. (06)
If the halting "problem" did not exist, it would be possible to list
all the true axioms with some finite process and we would have our FO.
That the halting "problem" does exist means the testing process may go
on for ever, there is no finite process to get them all, and the best
you can do is test the ones of interest to you as you come across
them. (07)
However, on the plus side, given any case, you can run a process and
if it halts you have an answer, the exact conditions for halting
telling you the validity of your theory. (08)
So in practice you can get any answer which is possible. But only by
running a process, and seeing if it halts. (09)
-Rob (010)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (011)
|