From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,c42dbf68f5320193 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2002-05-09 16:48:02 PST Path: archiver1.google.com!postnews1.google.com!not-for-mail From: dewar@gnat.com (Robert Dewar) Newsgroups: comp.lang.ada Subject: Re: Generation of permutations Date: 9 May 2002 16:48:02 -0700 Organization: http://groups.google.com/ Message-ID: <5ee5b646.0205091548.cd99d4c@posting.google.com> References: <5ee5b646.0205041652.63032ba6@posting.google.com> <3CDAB578.6F32339D@san.rr.com> NNTP-Posting-Host: 205.232.38.14 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Trace: posting.google.com 1020988082 832 127.0.0.1 (9 May 2002 23:48:02 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: 9 May 2002 23:48:02 GMT Xref: archiver1.google.com comp.lang.ada:23809 Date: 2002-05-09T23:48:02+00:00 List-Id: Stephen Leake wrote in message news:... > Darren New writes: > >> Right. So? The question is not whether it's possible to >> look at one program and decide what it does. The >> question is whether it's possible to write a program to >> look at all programs and decide whether or not they sort > > That's _your_ question. The question _I_ was addressing, > as posed by TMoran, was "Is the sequence of instructions > emitted by GNAT when it compiles bubble sort a program > that sorts it's input". But that's an entirely trivial question, if you thin anyone was addressing that or interest in that, you were confused. Of course the sequence of instructions generated by GNAT for bubble sort is provably a general sorting algorithm. That cannot be in question (if anyone questions that they are really really confused :-) Here is the actual Tom Moran quote: Robert: > but to determine whether a set of instructions > constitutes a general sorting algorithm is obviously > recursively undecidable. Tom: > So the set of instructions emitted by Gnat when it > compiles bubble sort code may or may not constitute a > general sorting algorithm, and whether it does or not is > undecidable? Now it is (I trust :-) so completely obvious that you can prove that the output of GNAT when it compile bubble sort is indeed a general sorting algorithm. We can't for a moment assume that Tom *really* thinks that it is undecidable :-) So the only reading of Tom's message is an attempt to disprove what I wrote by example. In other words he thinks my statement was implying the obviously incorrect conclusion. But that's where the misunderstanding crept in, because of course what I said does NOT imply this Assuming that anyone not interested in this has long ago killed this thread, let's take another stab at clarifying this issue. As I said earlier, the placement of quantifies is absolutely crucial. At the risk of boring everyone, let's persue this: The following statement is true: For any sequence of code that does NOT constitute a general sorting algorithm, there is a trivial proof that it does not constitute swuch an algorithm (namely a counter example). The following statement is true For any particular sequence of code, there is an algorithm that determines whether or not this sequence of code is or is not a general sorting algorithm (trivially true, the answer is Yes or No :-) The following statement is true There is NO general algorithm, which when presented with a particular sequence of code as input, can determine whether or not the piece of code is a general sorting algorithm. Understanding why all three statements are true is instructive :-) The first two statements are trivially true, and once you understand them, you should be able to immediately see that they are true. To see that the third statement is true is non-trivial. To prove this, we assume the halting problem and then prove by equivalence to this problem. Let's take a bubble sort and in the middle of it, run some arbitrary Turing machine till it halts. But now the general algorithm will have to be able to determine if it halts (algorithm is a good sort) or does not halt (algorithm is junk, runs for ever). The proof of the undecidability of the halting problem can be found in any book on computability. It's not that difficult to follow, but too much to outline here.