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

111–120 of 124 posts

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

#111

Post by fdupress »

touisteur wrote: post #93
fdupress wrote: post #80

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…

Hi, co-author here. We actually touched upon this subject in the article: 'Tip: Don’t prove what you don’t need to prove' and surrounding text. Also previous comment by Yannick: https://news.ycombinator.com/item?id=31980126

Looked for it and missed it.

And thanks for writing this up, by the way. Having people less familiar with formal methods try and write up their experiences is, I think, much more effective at letting people in than having experts try and write tutorials.

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

#112

Post by zoomablemind »

TFA seems to be a somewhat wasteful version of an algo which in my mind I call 'sinkersort' or 'minsort':

  for (i=0; i
Here the inner loop basically finds a min value of the remaining subset. This progressively fills the array in the sorted order.

The number of comparisons is bound by n^2/2 vs n^2 of TFA.

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

#113

Post by palunon »

zoomablemind wrote: post #112

TFA seems to be a somewhat wasteful version of an algo which in my mind I call 'sinkersort' or 'minsort': for (i=0; i Here the inner loop basically finds a min value of the remaining subset. This progressively fills the array in the sorted order. The number of comparisons is bound by n^2/2 vs n^2 of TFA.

Yours looks like selection sort but with more swapping.

The one in TFA isn't, for one crucial reason: the comparison is the other way around... And yet, it sorts.

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

#114

Post by Dylan16807 »

naniwaduni wrote: post #53
iib wrote: post #7

Earlier quoted context omitted.

I guess it can be thought of as an unoptimized insertion or bubble sort. I think it is very possible to write this algorithm by mistake in intro compsci classes when you try to code a bubble sort by heart. I would think TAs may have many such instances in their students' homework.

There's a surprisingly large class of "sorts people accidentally write while intending to write a bubble sort". This one is kind of special, though, since it's somehow more offensive to intuition than bubble sort itself.

Bubble sort is offensive to intuition? I would have said it was the most intuitive, because each step is very simple and you only have to remember one numeric variable in your core loop.

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

#115

Post by phkahler »

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

Earlier quoted context omitted.

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

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.

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

#116

Post by astrange »

twawaaay wrote: post #42
dahart wrote: post #30

Earlier quoted context omitted.

You sure it was this algorithm and not Bubble Sort? > algorithmic complexity isn’t everything Yeah very true. Or at least hopefully everyone knows that complexity analysis only applies to large n, and small inputs can change everything. In console video games it was very common to avoid dynamic allocation and to use bubble sort on small arrays. Also extremely common to avoid a sort completely and just do a linear sea…

Oh yeah, linear search I did a lot to the same consternation of other devs. The issue was the device was so low in memory (2MB of unified NV and flash for code, files and operating memory) that there simply did not exist enough space for a lot of things to be held to be any problem for the 20MHz ARM7 controller as long as you did not do anything stupid. 600kB of it was used by OpenSSL and further 300kB by operating s…

That’s not surprising, OpenSSL has terrible code quality and besides that was written in the era of thinking you should unroll all your loops so they go faster.

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

#117

Post by zoomablemind »

palunon wrote: post #113
zoomablemind wrote: post #112

TFA seems to be a somewhat wasteful version of an algo which in my mind I call 'sinkersort' or 'minsort': for (i=0; i Here the inner loop basically finds a min value of the remaining subset. This progressively fills the array in the sorted order. The number of comparisons is bound by n^2/2 vs n^2 of TFA.

Yours looks like selection sort but with more swapping. The one in TFA isn't, for one crucial reason: the comparison is the other way around... And yet, it sorts.

> Yours looks like selection sort but with more swapping...

Well, shooting for the simplicity (as posited in the Fung's arxiv paper) -- this one is on par with TFA and somewhat simpler in expression than the selection sort.

This is also direct, less 'magical' and indeed less wasteful than TFA. So for those roll-your-own-sort moments I'd rather remember this one instead.

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

#118

Post by naniwaduni »

Dylan16807 wrote: post #114
naniwaduni wrote: post #53

Earlier quoted context omitted.

There's a surprisingly large class of "sorts people accidentally write while intending to write a bubble sort". This one is kind of special, though, since it's somehow more offensive to intuition than bubble sort itself.

Bubble sort is offensive to intuition? I would have said it was the most intuitive, because each step is very simple and you only have to remember one numeric variable in your core loop.

Bubble sort's inner loop is so hilariously pessimal that it's incredibly easy to accidentally write an insertion sort because you intuition tells you it can't possibly be intended to be that bad.

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

#119

Post by simiones »

twawaaay wrote: post #57
simiones wrote: post #56

Earlier quoted context omitted.

> The fun part of this question is that the answer is: NEVER. Are you claiming that it is faster in practice to insert an element at the beginning of an array with 1G items, than it is to insert it at the beginning of a linked list with 1G items? Or that, on average, the time spent traversing the linked list (assuming an average number of cache misses) the time taken to move all elements in the array one to the right…

> Are you claiming that it is faster in practice to insert an element at the beginning of an array with 1G items, than it is to insert it at the beginning of a linked list with 1G items? You missed that insertion point is selected at random and must be found as part of the operation. But in practice if you know data will be inserted preferentially at the wrong end -- you can just easily reverse the data structure to…

> The cost of binary search goes to negligible pretty fast and cost of moving 8 bytes of memory is always going to be lower than the cost of iterating over one entry (16 bytes) of linked list. And you have statistically equal number of both assuming you are selecting values at random with equal chance for each 64 integer to be next choice.

That makes a lot of sense, thank you for the more detailed explanation.

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

#120

Post by zoomablemind »

palunon wrote: post #113
zoomablemind wrote: post #112

TFA seems to be a somewhat wasteful version of an algo which in my mind I call 'sinkersort' or 'minsort': for (i=0; i Here the inner loop basically finds a min value of the remaining subset. This progressively fills the array in the sorted order. The number of comparisons is bound by n^2/2 vs n^2 of TFA.

Yours looks like selection sort but with more swapping. The one in TFA isn't, for one crucial reason: the comparison is the other way around... And yet, it sorts.

By the way, the TFA algo is equivalent to:

  for (i=0; i
Once the max has been swaped in, further inner iterations past i (the position of max) are redundant.

However, we can go even further:

  for (i=0; i
This dispenses with the explicit max swap and simply does progressive insertion.

Curiously, in such transformed form the algo echoes the 'selection sort' from my previous post, performs equivalently too (wrt ncmpr, nswp).

Post reply on HN