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

101–110 of 124 posts

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

#101

Post by touisteur »

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.

Two of the most interesting things that trickled down during the design of Spark2014:

1- contracts are written in the same language as the code to be checked/proved. This made important to add expressive features to the language (for all / for some: quantifiers! expression functions, if- and case-statements and more recently the new delta-aggregates notation): these additions make the language far more expressive without too much loss of readability.

2- executable contracts: most contracts can be checked at runtime or proved. And the escape hatch (code only present for proof) is 'ghost' code which is also a nice addition.

Lots of little nifty additions to the language, from just 'thinking in contracts' or 'designing for probability'.

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

#102

Post by Asooka »

OJFord wrote: post #100

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?

The comparison is not the way you'd expect. Index j goes past index i, but the comparison doesn't change. What you propose is a condition more like

    if ((a[i]
Which obviously works.

The surprising algorithm sorts even though it swaps elements that are already ordered.

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

#103

Post by YetAnotherNick »

OJFord wrote: post #100

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?

If the second loop is from j = i to n, it is easy to see that it will sort in decreasing order. But notice j = 1 to n, then suddenly it will sort in increasing order

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

#104

Post by OJFord »

Asooka wrote: post #102
OJFord wrote: post #100

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?

The comparison is not the way you'd expect. Index j goes past index i, but the comparison doesn't change. What you propose is a condition more like if ((a[i] Which obviously works. The surprising algorithm sorts even though it swaps elements that are already ordered.

Ok, I think I see why it's a bit weird '1,2,3 when i=1 and j=3 it swaps them anyway' sort of thing?

But i-loop comes through 'afterwards', so when i=3 (value now 1) and j=1 (3) it sets them straight.

It still seems quite intuitive, but I think I cheated by skimming over it initially and thinking it was clear, whereas actually I've thought about it more now.

(Not to compare myself to anything like him, I'm no mathematician at all, but I'm reminded of an amusing Erdós anecdote in which he apparently paused mid-sentence in some lecture, left the room, and came back some time later continuing 'is clearly [...]' or similar!)

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

#105

Post by smusamashah »

bjterry wrote: post #76
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 loo…

This is nice. I had a way to highlight indexes at one point in this tool. Got rid of it when I was trying to add a way to visualize any custom algo. I should add it back. It adds more value/info to the visualization.

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

#106

Post by jasonwatkinspdx »

twawaaay wrote: post #99
kmonsen wrote: post #95

Earlier quoted context omitted.

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

A fun related thing I first learned about years ago due to a Dr Dobbs article: some strided access patterns are FAR worse than random access patterns. This is because certain strides hit the worst case behavior of limited associativity caches, dramatically reducing the effective cache size.

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

#107

Post by Stampo00 »

I've been watching those mesmerizing YouTube videos visualizing sorting algorithms lately. The header of this article uses a screen cap from one of them.

Them: So what shows do you watch?

Me: ... It's complicated.

There are a lot of different sorting algorithms. Like, a lot, a lot.

As I watch them, I try to figure out what they were optimizing for. Some only scan in one direction. Some only use the swap operation. Some seem to do the minimum number of writes. Some are incremental performance improvements over others.

When I see an algorithm like this, I don't assume the person who wrote it was an idiot. I assume they were optimizing for something that's not obvious to me. Its only modifying operation is swap, so maybe that operation is faster than an arbitrary insert for whatever system or data structure they're using. There are no temporary variables besides loop counters, so maybe they're on a memory-constrained environment. There's barely any code here, so maybe this is for a microcontroller with precious little ROM. Or maybe they're applying this as a binary patch and they have a strict ceiling to the number of ops they can fit in.

Or maybe it's just the first sorting algorithm they could think of in an environment that doesn't ship with one and the performance is adequate for their needs. In that case, it's optimized for developer time and productivity. And honestly, it's a far more elegant algorithm than my "naive" version would be.

These are all valid reasons to use a "naive" sorting algorithm.

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

#108

Post by kmonsen »

twawaaay wrote: post #99
kmonsen wrote: post #95

Earlier quoted context omitted.

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

Here is a video by Bjarne himself explaining this: https://youtu.be/YQs6IC-vgmo

Note there is a use case for linked list, inserting/deleting one or few items once in a while. But in general you can just use vector for anything that is not a leetcode problem.

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

#109

Post by alex_smart »

drdrek wrote: post #71
puffoflogic wrote: post #49

Earlier quoted context omitted.

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…

> Solution is even simpler:

Press X to doubt.

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

#110

Post by shp0ngle »

OJFord wrote: post #100

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?

look again at the comparison direction.

It is opposite!

It works but not as you think it does.

Post reply on HN