Re: Generation of permutations

[dewar@gnat.com (Robert Dewar)]

Stephen Leake <stephen.a.leake.1@gsfc.nasa.gov> wrote in message news:<uwuud2o12.fsf@gsfc.nasa.gov>...
> Darren New <dnew@san.rr.com> 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.