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

31–40 of 124 posts

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

#31

Post by JadeNB »

MattPalmer1086 wrote: post #2

Interesting. It is a bit counter intuitive at first but not too hard to see how it works. After the first main loop, the first item will be the biggest item in the list. The inner loop, as it always starts from 1 again will gradually replace the bigger items with smaller items, and so on.

> After the first main loop, the first item will be the biggest item in the list.

> The inner loop, as it always starts from 1 again will gradually replace the bigger items with smaller items, and so on.

I think the "and so on" is the point. To put it more precisely, I think that anyone (with a suitable familiarity with the tools) can prove formally that "after the first main loop, the first item will be the biggest item in the list"; but I think that it might take a bit more work to prove the "and so on" in a way that satisfies a formal prover.

(As to the intuition—I can buy that the "and so on" part is reasonably intuitive, but only at a level of intuition that can also believe wrong things. For example, just always replacing bigger items with smaller items doesn't guarantee you'll get a sorted list!)

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

#32

Post by 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 :)

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

#33

Post by mmcgaha »

iib wrote: post #7
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.

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.

I am guilty. I wrote this sort for a gnu screen session menu years ago and even named my function bubsort.

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

#35

Post by phkahler »

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…

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.

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

#37

Post by phkahler »

roenxi wrote: post #3

If it looks "obviously wrong" the quick proof that it works ... the j loop will move the largest unsorted element in the array into a sorted position. Since the i loop executes the j loop n times, the array must be sorted (since the n largest elements will be in the correct order). EDIT ^W^W^W Nope, I'm wrong. I did a worked example on paper. I think the devious thing here is the algorithm looks simple at a lazy glan…

The list on the left (index less than i) is always sorted. The ith element is inserted by the j loop and the rest of the list is shifted right by one element by repeated swapping with the ith position. Nothing to the right changes because the ith element is the max of the entire list, which seems to be a red herring for analysis.

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

#38

Post by MattPalmer1086 »

JadeNB wrote: post #31
MattPalmer1086 wrote: post #2

Interesting. It is a bit counter intuitive at first but not too hard to see how it works. After the first main loop, the first item will be the biggest item in the list. The inner loop, as it always starts from 1 again will gradually replace the bigger items with smaller items, and so on.

> After the first main loop, the first item will be the biggest item in the list. > The inner loop, as it always starts from 1 again will gradually replace the bigger items with smaller items, and so on. I think the "and so on" is the point. To put it more precisely, I think that anyone (with a suitable familiarity with the tools) can prove formally that "after the first main loop, the first item will be the biggest…

Sure, formal proof would be a lot harder. I just didn't find it quite as surprising that it works as the article implied.

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

#39

Post by twawaaay »

delecti wrote: post #27
twawaaay wrote: post #13

I actually used this algorithm a decade ago to implement a log-based, transactional database system for an embedded system with very low amount of memory and requirement that all memory be statically allocated. To the frustration of the rest of the development team who first called me an idiot (I was new) then they could not make quicksort run as fast on inputs that were capped at something like 500 items. Apparently…

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 algorithm might actually be only good on paper but doing more harm to your TLB cache, prefetcher, branch predictor, instruction pipeline, memory density, etc.

So there is this fun question:

"You are generating k random 64 bit integers. Each time you generate the integer, you have to insert it in a sorted collection. You implement two versions of the algorithm, one with a singly-linked list and one with a flat array. In both cases you are not allowed to cheat by using any external storage (indexes, caches, fingers, etc.)

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 fun part of this question is that the answer is: NEVER.

Post reply on HN