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

91–100 of 124 posts

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

#91

Post by Jtsummers »

MrYellowP wrote: post #87

> published at the end of 2021 I'm so confused. That "new" algorithm is just BubbleSort?

As addressed in other comments in this thread and past threads on this sort (when the paper came out), it is not bubble sort. Bubble sort only compares adjacent items and swaps them if they are in the wrong order. This has the effect of "bubbling" the largest value to the top (the way it's often written, could also reverse it to push the smallest down first).

This sort is like a worse performance version of insertion sort. But insertion sort creates a partition (and in doing this performs a sort) of the first i+1 items, with i increasing until the entire sequence is sorted. This one will scan the entire sequence every time on the inner loop instead of just a subset of it and usually perform more swaps.

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

#92

Post by [deleted] »

twawaaay wrote: post #39
delecti wrote: post #27

Earlier quoted context omitted.

I fee like anyone who was surprised that algorithmic complexity isn't everything, probably didn't totally understand it. The assumptions (like ignoring constants) are straight out of calculus limits. That (+10000) on the end doesn't mean anything if you're sorting an infinite list, but it means a lot if you're sorting 15 (or in your case 500) entries.

Well, it actually is kinda worse (or better, depends how you look at it). It is not necessarily +10000, it can also be something like x5000. Because CPUs really, really, really like working short, simple, predictable loops that traverse data in a simple pattern and hate when it is interrupted with something like dereferencing a pointer or looking up a missing page. So your super complex and super intelligent algorith…

[deleted]

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

#93

Post by touisteur »

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

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

#94

Post by im3w1l »

yannickmoy wrote: post #89
im3w1l wrote: post #64

Earlier quoted context omitted.

Yeah, I see this as a very interesting reply to the TLA+ post. Might spend my evening diving into Ada and Spark. Edit: Some things I noticed. The package gnat-12 does not have gnatprove. Ada mode for emacs requires a compilation step that failes with gnat community edition. With alire there is no system gnat so it cannot compile it (quite possible I'm missing something). In the end I gave up on using emacs. Gnatstudi…

you can ask Alire to install the latest GNAT it built, or to use another version installed on your machine, see https://alire.ada.dev/transition_from_gnat_community.html It also explains how to install GNATprove: ``alr with gnatprove``

Sorry if it was confusing I kind of jumped between the issues I had with various approaches. I did manage to get gnatprove through alire through just that command, it was the apt gnat that didnt have gnatprove. What I wasn't sure how to correctly do with the alire install was

  cd ~/.emacs.d/elpa/ada-mode-i.j.k
  ./build.sh
  ./install.sh
Actually I didn't get that working with any of the options I tried I guess.

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

#95

Post by kmonsen »

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…

You are right and this is will know, but not only for the reason you state. Cache locality is so much better on an array/vector compared to linked list and that is really important.

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

#96

Post by touisteur »

dgan wrote: post #17

So, Lionel knew how to implement a 3D Renderer, but had no clue about O(n) complexity neither other sorting algorithms? I am buffled

Well, Hi there, it me. Back then I was 17 and wading through software rendering so (light) mesh tessellation, triangle projection (twice, for a stereoscopic anaglyph renderer), triangle filling, texture mapping, with at most 300 objects, all in crappy crashy C (first with VESA, then SDL eased my life...) with lots of misunderstandings about pointers.

I was welllll over my head with complex stuff, and sorting didn't appear in the profiles, so... I guess you can call that profile-guided learning? I had the formal training, later on, and even then it didn't stick until I faced the actual complexity problem head-on.

I'll never forget that whole weekend with my AMD Athlon 900 at 100% CPU sorting a 200 000 words dictionary... It was still not finished on Monday. Implemented (a very primitive) insertion sort and it was done in less than 2 minutes...

That was my 10000-a-day day https://xkcd.com/1053

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

#97

Post by Agingcoder »

dgan wrote: post #17

So, Lionel knew how to implement a 3D Renderer, but had no clue about O(n) complexity neither other sorting algorithms? I am buffled

The exact same thing happened to me, and this is how I discovered algorithmic complexity. Sorting my triangles took forever (I saw it in the profile, taking a whopping 90% of the time ) and I eventually figured there might be a proper sorting algorithms out there.

I was at the same time happily churning out assembly code, talking to the vga card, writing a dos extender, etc.

You can actually do quite a few things without formal education!

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

#98

Post by Izkata »

twawaaay wrote: post #45
eranation wrote: post #44

Earlier quoted context omitted.

That is pretty awesome if you came up with this exact algorithm a decade ago, ( it was published in 2021, but apparently was in the wild in 2015[1] and I assume discovered earlier, but no one thought it was interesting enough to publish). Why didn’t you use bubble sort / insertion sort? (The algorithm in the paper looks like bubble sort at first look but is basically a clever insertion sort) what was the benefit of u…

I am not sure how awesome it is. It looks like something you can stumble on your own by accident on a whiteboard on an interview and use successfully even if you don't know why it works exactly. Honestly, I always thought it is a common knowledge and it is just too simple and for this reason gets omitted from books. People in CS/IT tend to not spend a lot of time on algorithms with bad complexity and so I am used to…

Yeah, this sorting algorithm is something you can come up with by accident if you do bubble sort wrong. I wouldn't be surprised if a lot of beginners came up with this one in intro courses. I think I saw it around 2006-2008 when I was a TA and one of my students couldn't figure out why his array got sorted in the wrong order (don't remember for sure though).

For example, from 2016, here's someone not getting the difference between the two: https://stackoverflow.com/questions/40786409/whats-the-diffe...

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

#99

Post by twawaaay »

kmonsen wrote: post #95
twawaaay wrote: post #57

Earlier quoted context omitted.

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

You are right and this is will know, but not only for the reason you state. Cache locality is so much better on an array/vector compared to linked list and that is really important.

Good point. Cache locality is another important reason that I should have mentioned. I have not run tests, but it may possibly be the most important reason of them all.

In many linked data structures you can mitigate a lot of this problem. For example, in the past I have used contiguous arrays where I would allocate linked elements, then I would try to exploit how the elements are produced to get them placed one after another, if possible.

When data is produced randomly you can try to create "buckets", where each bucket is backed by an array and attempts to keep consecutive elements relatively close to each other. You could then try to rewrite those buckets in a way that gets amortised. Or you can just straight write it as if it was an array of sorted linked list elements where on each delete or insert you have to move some of the elements, but you only need to reorganise one bucket and not others.

All a bit cumbersome and at the end of it you are still wasting at least half of the cache on pointers.

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

#100

Post by OJFord »

Why is this algorithm at all surprising?

(I'm really not trying to brag - I assume I must be missing something, that I'm naïve to think it obviously works, and it actually works for a different reason.)

In plain English - 'for every element, compare to every element, and swap position if necessary' - .. of course that works? It's as brute force as you can get?

Post reply on HN