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

51–60 of 124 posts

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

#51

Post by leereeves »

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

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] Elements are only swapped when 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.

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

#52

Post by Jtsummers »

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

Is the visualization supposed to animate? I can’t figure out how to make it start.

There is a "start" button at the end of the list of sorts.

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

#53

Post by naniwaduni »

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.

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.

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

#54

Post by Jtsummers »

donatj wrote: post #36

Is this not a standard sorting algorithm? If I'm not mistaken this is my coworkers go to sort when writing custom sorts.

It manages to be more inefficient than most, and will even disorder and then reorder an already sorted input. Bubble sort (a very low bar to beat) doesn't even do that. If you've only got a small number of items, it doesn't matter unless you're sorting a small number of items a large number of times.

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

#56

Post by simiones »

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…

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

I am certain the first item will not be true, and the second may or may not be true depending on many many other details (e.g., in a language with a compacting GC, the linked list elements will often be stored approximately like in the array case, and you may not pay too high a cost for cache misses).

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

#57

Post by twawaaay »

simiones wrote: post #56
twawaaay wrote: post #39

Earlier quoted context omitted.

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…

> 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 make insertions prefer the better end.

> I am certain the first item will not be true

I am used to it. Everybody gets it wrong until they spend some time thinking about it, get it explained and/or run a real life test.

Hint: think about the cost of iterating over half of the linked list versus performing binary search over the array AND moving half of it.

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.

CPU can be moving a lot of bytes at the same time but it has to dereference the pointer before it can get to perform comparison before it can dereference the next pointer...

Actual algorithmic complexity of both algorithms is exactly the same. But an array is much more efficient (instructions per item).

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

#58

Post by School-Cotton »

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.

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 After this is done we have maintained the condition that A[1] .. A[i] are sorted after j ranges from 1 to i.

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

#59

Post by Jtsummers »

eatonphil wrote: post #9

This is a fantastic post! It's great to have a concrete example of proving a not-trivial algorithm. And somehow this Ada code feels more approachable to me than HOL4 and other functional proof assistants I've looked at. While it's been on my list for a while, I'm more curious to try out Ada now.

It'll take you less than a week to get proficient enough in it to make something useful, or at least interesting. It's a very straightforward language, overall.

https://learn.adacore.com/ - Pretty much the best free source until you're actually ready to commit to the language. The "Introduction to Ada" course took me maybe a week of 1-2 hours a day reading and practicing to go through. There's also a SPARK course that takes a bit longer, but is also interactive.

The language reference manuals for 2012 and 202x (which should become Ada 2022):

http://www.ada-auth.org/standards/ada12.html

http://www.ada-auth.org/standards/ada2x.html

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

#60

Post by jwilk »

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…

I think you misunderstood the question.

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

Post reply on HN