Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

I can’t believe that I can prove that it can sort

blog.adacore.com

Post reply on HN
Print view View original

71–80 of 124 posts

Re: I can’t believe that I can prove that it can sort

#71

Post by drdrek »

puffoflogic wrote: post #49
drdrek wrote: post #32

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. Talk…

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.

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= A[I] nothing will happen From the first J where JN+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=A[I] and the list is ordered for the first J elements

Re: I can’t believe that I can prove that it can sort

#72

Post by jwilk »

twawaaay wrote: post #62
jwilk wrote: post #60

Earlier quoted context omitted.

I think you misunderstood the question. If you insert an element at the beginning, there's no list iteration cost.

Please, read the question. It stipulates that elements are selected at random. You select k integers at random. Some of them might be inserted faster into linked list, but when you average it over k integers you will still be slower because inserting into array will be faster, on average. Just think what happens if the integer is inserted at the END of the list (same probability...) You need to slowly iterate over en…

The parts of simiones's message you quoted are not about the average case. They are about the corner case when an item would be added the beginning, meaning the linked list has the biggest advantage.

Re: I can’t believe that I can prove that it can sort

#73

Post by School-Cotton »

leereeves wrote: post #51
phkahler wrote: post #35

Earlier quoted context omitted.

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.

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 in…

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

Re: I can’t believe that I can prove that it can sort

#74

Post by twawaaay »

jwilk wrote: post #72
twawaaay wrote: post #62

Earlier quoted context omitted.

Please, read the question. It stipulates that elements are selected at random. You select k integers at random. Some of them might be inserted faster into linked list, but when you average it over k integers you will still be slower because inserting into array will be faster, on average. Just think what happens if the integer is inserted at the END of the list (same probability...) You need to slowly iterate over en…

The parts of simiones's message you quoted are not about the average case. They are about the corner case when an item would be added the beginning, meaning the linked list has the biggest advantage.

You don't get to change the rules of the game while the game is being played.

The original problem, as stated by me, was:

"You are generating k random 64 bit integers. Each time you generate the integer, you have to insert it in a sorted collection.

(...)

The question: in your estimation, both algorithms being implemented optimally, what magnitude k needs to be for the linked list to start being more efficient than array list."

The cost is not evaluated for any individual insertion, only for the total cost of inserting k integers.

For some of the integers the cost of inserting to linked list will be higher, and for some the cost of inserting to array will be higher. It does not matter. We do not care. We just care about what is the cost of inserting k integers thus randomly generated a) into sorted linked list and b) into sorted array list.

Re: I can’t believe that I can prove that it can sort

#75

Post by tromp »

drdrek wrote: post #32

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. Talk…

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 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.

Re: I can’t believe that I can prove that it can sort

#76

Post by bjterry »

smusamashah wrote: post #5

Here is how it looks. https://xosh.org/VisualizingSorts/sorting.html#IYZwngdgxgBAZ... If you compare it with both Insertion and Bubble sort. You can see it looks more like insertion sort than bubble sort.

The video from the article (https://www.youtube.com/watch?app=desktop&v=bydMm4cJDeU) is much better because it highlights the index of the outer loop, which is unclear from the cascading visualization there. By seeing the indexes it becomes clear that (1) in the area before the outer index, every value gets swapped in and out of the outer loop location to put them in order, and (2) at the end of the first outer loop iteration, the largest element will be at the location of the outer loop index, and so everything to the right is unchanged in each iteration.

Re: I can’t believe that I can prove that it can sort

#78

Post by leereeves »

School-Cotton wrote: post #73
leereeves wrote: post #51

Earlier quoted context omitted.

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 in…

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

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).

Re: I can’t believe that I can prove that it can sort

#79

Post by fweimer »

Isn't the proof incomplete because it does not ensure that the result is a permutation of the original array contents? Just overwriting the entire array with its first element should still satisfy the post-condition as specified, but is obviously not a valid sorting implementation.

Re: I can’t believe that I can prove that it can sort

#80

Post by fdupress »

Every time somebody proves that a sorting algorithm sorts, they forget to prove that the algorithm doesn't just drop values or fill the entire array with 0s (with fixed-length arrays, as here).

On paper: "it's just swaps" Formally: "how do I even specify this?"

(For every value e of the element type original array and the final array have the same number of occurrences of e. Show that that's transitive, and show it's preserved by swap.)

Post reply on HN