61–70 of 124 posts
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…
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…
I think you misunderstood the question. If you insert an element at the beginning, there's no list iteration cost.
It stipulates that elements are selected at random.
You select k integers at random.
Some of them might be inserted faster into linked list, but when you average it over k integers you will still be slower because inserting into array will be faster, on average.
Just think what happens if the integer is inserted at the END of the list (same probability...) You need to slowly iterate over entire linked list. While you quickly land at the result with a binary search on an array and then pay almost no cost inserting it there.
If you think about it, ON AVERAGE, you have to search through half of the list (if you are linked list) or move half of the array (if you are an array).
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 comments so far have tended to focus on the proof itself, but for me the coolest part of the blog post were the formal methods. Does anyone here also use SPARK for this sort of thing? Are there other formal methods tools you'd use if you had to prove something like this?
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. Gnatstudio wouldn't run for me until I realized it needed ncurses. It also had some unhandled exceptions for me (raised PROGRAM_ERROR : adjust/finalize raised GNATCOLL.VFS.VFS_INVALID_FILE_ERROR: gnatcoll-vfs.adb:340), but in the end I managed to get it up and running.
Edit2: After playing around with it, I'm extremely impressed with what spark can do. I made a function to add 7 to numbers. Tried putting a post condition that the return value is bigger than input. "Nuh uh, it could overflow". Ok so I add a pre condition that numbers must be less than 100. "Uhm, buddy you are passing in 200 right there". This is useful stuff for real and easy to write too.
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.
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.
That's all we need to know: during each iteration after the first, the algorithm inserts the ith element into the previously sorted list from A[1] to A[i-1], giving a new sorted list from A[1] to A[i], and doesn't touch the rest because A[i] contains the maximum element.
Then when i=n the whole list is sorted.
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…
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…
Note that the equality sign is less than, but the algorithm sorts in a descending order.
Clojure code:
(defn swap [items i j]
(assoc items
i (items j)
j (items i)))
(defn weirdsort [items]
(let [ct (count items)
indices (for [i (range ct)
j (range ct)]
[i j])]
(reduce (fn [items [i j]]
(let [ith (nth items i)
jth (nth items j)]
(if ( my-namespace> (def items (shuffle (range 20)))
#'my-namespace/items
my-namespace> items
[19 0 13 16 14 18 15 7 10 17 9 11 6 1 3 4 12 2 5 8]
my-namespace> (weirdsort items)
[0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19]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…
Well, there is one case where a linked list may be faster: when due to memory fragmentation you are unable to allocate contiguous k elements (hence efficiency would drop to zero) but you would still able to allocate k nodes (or k / n nodes with n elements each). It can therefore make sense to use a linked list of arrays with some sensible limit on the array size (e.g. in the gigabyte range). As long as a smaller numb…
On new operating systems process address space is pieced together independently from physical space. So you can have contiguous, multi-GB array even if you don't have contiguous, multi-GB physical region.
As you read/write your virtual address space the CPU detects that there is no TLB mapping and interrupts into operating system which behind the scenes finds a page, returns the mapping and continues as if nothing ever happened.
This is why a process nowadays can allocate any amount of memory -- more than there is physical memory on the machine. It only starts grinding to a halt when you actually try to use it all. (This actually is one of my interview questions -- Can a process allocate more memory than is physically available on the machine? Why does it work?)
The comments so far have tended to focus on the proof itself, but for me the coolest part of the blog post were the formal methods. Does anyone here also use SPARK for this sort of thing? Are there other formal methods tools you'd use if you had to prove something like this?