Re: Program analysis
- From: "Stuart" <stuart@xxx>
- Date: Mon, 13 Aug 2007 10:05:06 +0100
"Richard Harter" <cri@xxxxxxxx> wrote in message
news:46bdd885.511881343@xxxxxxxxxxxxxxxx
On Fri, 10 Aug 2007 10:01:15 +0100, "Stuart" <stuart@xxx> wrote:
Richard Harter identified 3 classses of program - I think he was not quite
right; I think there are
- Those that provably halt
- Those that provably don't halt
- Those where halting is provably uncomputable
- Those where halting is unknown
<Nitpick>
If your first three are meant to be the three classes that I mentioned
then
you've slightly misquoted me. I wrote:
"Programs fall into three classes; those that provably halt, those
that provably never halt, and those that never halt but cannot be
proven never to halt."
"those that never halt but cannot be proven never to halt" is a different
concept from "halting is provably uncomputable".
</Nitpick>
I am happy to clarify that I was not quoting you: I only intended to
incidentally refer to your posting elsethread, which had commented upon the
different types of program, before presenting my own thoughts on the
different types of program the OP might encounter. I very much regret it if
you feel you were misrepresented [I expect the wrath of the gods of
nettiquette will be visited upon me for my sins].
More importantly your fourth class is of a different kind of thing from
the
other three. The first three are, so to speak, absolute. They specify
what can and cannot be proven. Your fourth is a different kind of
animal -
it is temporal. That is, it doesn't address what can be done; rather it
addresses what is known at present.
It was this that I wanted to point out; especially as it [to me anyhow]
represents a very large class of interesting problems - the things we don't
yet know.
The temporal version of my three classes is:
Those are known to halt.
Those that are known not to halt.
Those where halting is unknown.
In cases 1 and 2 we have a proof; in case 3 we don't have a proof and
cannot know for certain that we will ever find a proof.
For my own nitpick I would say that these do not cover the class of
'uncomputable' very well. Surely the main point of Turing's Halting Problem
is that it _proves_ there is a class of program, which does not fit into
either of the first two classes. You may say that this means halting is
unknown; but I think this is not a very good fit. We 'know' that it is
'uncomputable' and that it would be a fruitless endeavour to try and
determine whether it halts. I would prefer to separate problems that are
uncomputable from others which are simply unknown - yet!
An important thing distinction to keep in mind is whether we are talking
about abstract programs or programs in the real world. Programs in the
real world halt when their instantiating device fails; there are no
programs in the real world that never halt.
Agreed!
--
Stuart
.
- References:
- Program analysis
- From: Tim Frink
- Re: Program analysis
- From: Stuart
- Re: Program analysis
- From: Logan Shaw
- Re: Program analysis
- From: Stuart
- Re: Program analysis
- From: Richard Harter
- Program analysis
- Prev by Date: Re: Rock paper scissors population algorithm, need help
- Next by Date: Computer Programmer Cartoon "code" Seeks Sponsor
- Previous by thread: Re: Program analysis
- Next by thread: Re: Program analysis
- Index(es):
Relevant Pages
|
