[drdrek]

He starts from the wrong axiom that its hard to prove and creates a lot of nonsense over that.

Its requires just two induction proofs: - One that for I=1, after N comparisons the largest number is at position 1 (Proven with induction) its the base case - The other, that for any I=n+1 if we assume that the first n slots are ordered we can treat n+1 as a new array of length N-n and solve using the base case proof.

Talking about computer science and not doing the bare minimum of computer science is peak software engineering :)

[phkahler]

I thought his goal was to get the prover to prove it without understanding it himself.

By realizing the low-indexed portion is always sorted, you've already proved the algorithm yourself and the prover is just checking for bugs in your logic.

I'm not saying the proof isnt valuable, just that it's not magical and actually requires the user to understand the majority of the proof already.

[leereeves]

This algorithm is surprising and interesting because it doesn't work at all like it at first seems to.

The low-indexed portion is sorted, but isn't guaranteed to contain the lowest or the highest i elements of the list (except when i=1), and the list is ultimately sorted in decreasing, not increasing order. The final sort doesn't occur until the last iteration of the outer loop when the inequality is reversed (the interesting variable, j, is on the right).

Because of that, the proof outline discussed here doesn't work.

Consider what happens if the unique smallest element starts at position n. It is placed at the start of the list (the correct final position) in the final iteration of the outer loop (i=n), and not before.

Proof (for simplicity the list is indexed 1 to n):

Let A[n] < A[k] for all k != n in the initial list.

Elements are only swapped when A[i] < A[j]. If i != n and j = n, then A[i] > A[n] = A[j], so A[n] is not swapped.

Then, when i = n and j = 1, A[i] = A[n] < A[1] = A[j], so A[1] and A[n] are swapped, placing the smallest element in position 1 at last.

[umanwizard]

It’s not true that it’s sorted in decreasing order. See my comment here: https://news.ycombinator.com/item?id=31978942

[leereeves]

Quite right, that was a silly mistake on my part. I did say the smallest element was placed first, but wrote "the list is ultimately sorted in decreasing, not increasing order" backwards.

I meant to contradict the top post: "the largest number is at position 1...we can treat n+1 as a new array of length N-n and solve using the base case proof", which would result in decreasing order (largest first).

[phkahler]

The largest number is at position 1 after the first pass of the inner j loop. In fact it's at the ith position after each completion of the j loop, and it serves to separate the sorted and unsorted parts of the array.

Beyond that it's just inserting the ith element into the list by finding its place and shifting everything over one position.

[puffoflogic]

That is an elegant proof... for a totally different algorithm. J starts at 1, not at I. Every element of the loop is subject to be moved in every single outer iteration. Besides it gets the comparison backwards.

[drdrek]

You are absolutely correct, I was gun ho and got punished with internet shame, bellow is the correct proof. but the point still stands.

Solution is even simpler:

Empty case after 1 iteration (I=1) the largest number is at position 1 Base case: after 2 iterations (I=2) the 2 first elements are ordered, and the largest number is at position 2

Assume N case: after N iterations the first N numbers are ordered (within the sub list, not for the entire array) and the largest number is at position N

N+1 case (I=N+1): For Every J<N+1 and A[J]>= A[I] nothing will happen From the first J where J<N+1 and A[J] < A[I] (denote x) each cell will switch as A[J] < A[J+1] At J=N+1 the largest number will move from A[N] to A[I] For every J>N+1 Nothing will happen as the largest number is at A[I]

Not part of the proof but to make it clear we get: - for J<x A[J]<A[I] - for J=x A[J]=A[I] - for J<x A[J]>=A[I] and the list is ordered for the first J elements

[alex_smart]

> Solution is even simpler:

Press X to doubt.

[umanwizard]

No, it works, there's just a bit of an unstated step in the proof.

After j ranges from 1 to i, it will still be the case that the values from 1 to i are sorted. So you can assume that j starts at i without disturbing the induction condition.

The reason this is true is... If A[i] is >= any element A[j] for j < i, then it is clearly true. Otherwise, there is some smallest j in 1 to i-1 inclusive such that A[i] < A[j]. Then A[i] will swap with that A[j], then it will swap again with the next A[j+1] (because the original A[j] was < A[j+1]) by the induction case, then with the next element, ... swapping with every element until j reaches i.

After this is done we have maintained the condition that A[1] .. A[i] are sorted after j ranges from 1 to i.

[leereeves]

That is the correct inductive step all by itself.

That's all we need to know: during each iteration after the first, the algorithm inserts the ith element into the previously sorted list from A[1] to A[i-1], giving a new sorted list from A[1] to A[i], and doesn't touch the rest because A[i] contains the maximum element.

Then when i=n the whole list is sorted.

[tromp]

If the (i+1)'st outer loop starts with the first i elements in sorted order, then it ends with the first i+1 elements in sorted order.

In fact if k of the first i elements are <= A[i+1], then the first k iterations of the inner loop will not swap, and the next i-k iterations will swap. The latter can be seen to maintain order.

The last n-i iterations of the inner loop (where j>=i) do not affect this reasoning and can be omitted, as can the first iteration of the outer loop.

[tonmoy]

Note that the equality sign is less than, but the algorithm sorts in a descending order.

[umanwizard]

Not true.

Clojure code:

    (defn swap [items i j]
      (assoc items
             i (items j)
             j (items i)))
    
    (defn weirdsort [items]
      (let [ct (count items)
            indices (for [i (range ct)
                          j (range ct)]
                      [i j])]
        (reduce (fn [items [i j]]
                  (let [ith (nth items i)
                        jth (nth items j)]
                    (if (< ith jth)
                      (swap items i j)
                      items)))
                items indices))
      )

Then in the repl:

    my-namespace> (def items (shuffle (range 20)))
    #'my-namespace/items
    my-namespace> items
    [19 0 13 16 14 18 15 7 10 17 9 11 6 1 3 4 12 2 5 8]
    my-namespace> (weirdsort items)
    [0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19]

[tonmoy]

Sorry I meant to write ascending. It is weird that it swaps when i < j, but the list ends up ascending