https://rjlipton.wpcomstaging.com/2022/06/13/sorting-and-proving/ Skip to content Godel's Lost Letter and P=NP a personal view of the theory of computation * Home * About P=NP and SAT * About Us * Conventional Wisdom and P=NP * The Godel Letter * Cook's Paper * Thank You Page Sorting and Proving June 13, 2022 tags: Algorithms, Codex, formal methods, GPT-3, Hoare logic, Proofs, Quicksort, Tony Hoare by RJLipton+KWRegan A proof tells us where to concentrate our doubts--Morris Kline Tony Hoare is also known informally as Sir Charles Antony Richard Hoare. He has made key contributions to programming languages, algorithms, operating systems, formal verification, and concurrent computing. He won the 1980 Turing Award for "Fundamental contributions to the definition and design of programming languages." [th][th] Quicksort Hoare invented a new sorting algorithm in 1959. It was not later directly cited in his winning of the Turing Award--see above. Back then Hoare was a visiting student at Moscow State University. His student project at the time needed to sort words in Russian sentences before looking them up in a Russian-English dictionary, which was in alphabetical order on a magnetic tape. He tried insertion sort but it was too slow, and so he invented a new sorting algorithm--it is now called Quicksort. Amazing. On his return to England, he was asked to write code for Shellsort. Hoare mentioned to his boss that he knew of a faster algorithm and his boss bet sixpence that he did not. His boss ultimately accepted that he had lost the bet. Quicksort is well named--it is a winner. And Still Champion The most amazing thing to me--Ken writing this and the next section---is that Quicksort has remained the champion sorter. Mergesort was earlier but Heapsort came five years later. No one has improved on Hoare's idea to focus on swaps that improve the sortedness of two elements at once, both jumping over a guiding element called the pivot. Mergesort and Heapsort guarantee {O(n\log n)}{O(n\log n)} time to sort {n}{n} items, whereas Quicksort does not. Yet careful implementations of Quicksort almost always evade slow outcomes. Then they beat Mergesort and Heapsort and all other sorting methods cleanly in terms of the constant under the "{O}{O}." The algorithms-and-data-structures course I taught at UB this past term includes sorting algorithms. I have brought together and polished code instances I showed during the term to compare these three algorithms in one code file. It is in the Scala programming language. The program has options described at the top, such as setting the "tradeoff point" {m}{m} so that on recursive calls to sort pieces of size at most {m}{m}, the code uses Insertion Sort instead. It counts comparisons and copies of items separately, as well as report the time in milliseconds. A swap counts as three not two copies. Here is an example run on the English text of War and Peace using {m = 16}{m = 16} for both Quicksort and Mergesort. I wanted to salute Hoare's application by using the original Russian text, but every file of it I found was densely footnoted. The Russian version doesn't begin in Russian anyway. I've edited the output slightly. metallica<~> scala Sorts WarAndPeace.txt 16 medianRandom3 011000 Bits=(randomize)(makeHeap)(part for ==)(use Selsort)(make distinct) (pad len) Sorting 562,603 items, tradepoint 16 to insertion sort QuickSort pivot is medianRandom3 for 3-way part; heapSort uses makeHeap MergeSort made 8,874,241 comparisons and 9,001,648 copies plus 1,447,593 comparisons and 2,061,296 copies for insertionSort at bottom In total: made 10,321,834 comparisons and 11,062,944 copies Time for mergeSort: 3241 milliseconds QuickSort made 5,832,042 comparisons and 16,390,570 copies plus 74,992 comparisons and 108,450 copies for insertionSort at bottom In total: made 5,907,034 comparisons and 16,499,020 copies Time for quickSort: 1212 milliseconds HeapSort made 19,977,762 comparisons and 31,494,294 copies Time for heapSort: 1885 milliseconds This used the strategy of selecting the median of three randomly sampled elements of the array piece to be sorted as the pivot. Quicksort runs quickest when the pivot is the median, but it takes too long to find the exact median at each level of recursion. My program has the option "ninther" to select the median of three such median-of-3 samples, as proposed by John Tukey. Try my code to see if ninther works faster and with fewer comparisons on your system. Empirical Testing and Proving The person whose 1975 PhD dissertation studied the performance of Quicksort implementations with rigor and depth was none other than Bob Sedgewick, whose retirement party Dick recently covered. This led into Bob's famous textbook Algorithms, which is now in its fourth edition with Kevin Wayne as co-author. Bob's separate notes accompanying the book point out an aspect vital to running on inputs like War and Peace that have many identical (keys of) items. The simple partition for a pivot {p}{p} into [ elements <= p ][ p ][ elements >= p ] winds up doing many extra comparisons of keys equal to {p}{p}. The extra initial effort to determine a 3-way partition [ elements < p ][ elements == p ][ elements > p ] pays off in the recursion, which only needs to be on the outer two segments. Without this trick, Quicksort--on even a relatively high-entropy source like War and Peace--degrades to be worse than the other two algorithms. My code allows making all words distinct by setting the fifth bit. Then Quicksort makes more comparisons and copies than Mergesort. Yet it still runs almost 40% faster in my tests. As explained in general here, this is because the Quicksort gives better cache locality. Heapsort likewise runs in-place, but not with locality. The assertions itemized in this section are unimpeachable. But in what sense, and to what degree, are they formally provable? There is also a difference from the criterion of reproducibility in the sciences. The environmental conditions for reproducing an experiment are presumed to be closed and given. The primacy of Quicksort, however, applies to processing architectures that were unknown at the time of Sedgewick's 1975 thesis, let alone Hoare's 1959 concept. It is a more open-ended prediction that if you run mine or similar code on your system--in machine environments I may know nothing about--it will give much the same time performance. Now back to Dick, about Hoare's take on formally proving properties of programs. Hoare Logic Hoare invented a new logic for reasoning about the correctness of computer programs ten years later in 1969. It was directly counted toward his winning of the Turing Award. It was based on original ideas created by Robert Floyd, who had published a system for flowcharts. The logic is now known as Hoare logic--see this for details. This is one of the most influential papers on the theory of programming. In this paper Hoare showed how to reason about program execution using logical specifications of statement behavior that has become known as Hoare triples. A Hoare triple has three parts, a precondition {P}{P}, a program statement or series of statements {S}{S}, and a postcondition {Q}{Q}. It's is usually written in the form \displaystyle \{P\} S \{Q\} \displaystyle \{P\} S \{Q\} The meaning is "if {P}{P} is true before {S}{S} is executed, and if the execution of {S}{S} terminates, then {Q}{Q} is true afterwards". Note that the triple does not assert that {S}{S} will terminate; that requires a separate proof. As a simple example: \displaystyle \{x+1=43\}y:=x+1\{y=43\} \displaystyle \{x+1=43\}y:=x+1 \{y=43\} A key motivation for Hoare Logic is to be able to prove the correctness of real systems with real programs. The fact that Hoare Logic is possible is clear. It is possible to use it to prove Quicksort, for example. But it is less clear whether or not we will be able to apply formal methods to complex practical systems. This is a topic that I have thought about for decades. A Codex Saturday's Washington Post has a tech article, "The Google engineer who thinks the company's AI has come to life." This prompted us to visit a long article in the April 15 New York Times Magazine on Open AI's GPT-3 language engine. GPT-3 works by playing a game of guess the next word in a phrase. This is akin to guess the next move in chess and other games, and we will have more to say about it. For an example with wider context, suppose we fed it this post up before this section, and then gave it "A Cod-" as the partially completed section title. Since this comes at the end, GPT-3 might guess coda. Or since this is an addendum, maybe codicil. A codex, on the other hand, is a large manuscript book. In fact, we do mean codex, or rather Codex, which is an offshoot of GPT-3 for generating code in a wide variety of programming languages. Its emergence creates a new riff on our recent discussion on proving and how software projects have stayed robust while growing far beyond the scale on which they can be formally proved. Now Codex ventures to write one's software by gleaning the intent from one's prose specification--by drawing on millions of available coding projects that give relatable specifications. Is program output from Codex proven--or provable? This will be a challenge. It may be more feasible to integrate Codex with projects like the Verified Software Toolchain led Andrew Appel, Lennart Beringer, William Mansky, and Qinshi Wang. This is at any rate further grist for discussion. Open Problems Take a look at this for comments about the recent Harry Lewis debate. This was based on our paper. What do you think? Share this: * Reddit * Facebook * Like this: Like Loading... from - algorithms, fast, History, Ideas, News, People, Proofs, Results, Teaching - Laws and Laughs 2 Comments leave one - 1. [53463a4][53463a4] Jon Awbrey permalink June 13, 2022 4:00 am As a person who struggles on a daily basis to rise to the level of sentience I've learned it has more to do with beginning than ending this sentence. Loading... Reply 2. [4adcca4][4adcca4] space2001 permalink June 13, 2022 9:41 am Since that the constants in the O notation play a significant role in separating the different sorting algorithms in a real-world application; I got wondering how much we can reduce the constants if we relax the problem from exact-sorting to sorting-with-errors; We'll have to define of course what errors are allowable and how to parameterize these errors; e.g., up-to X% of output data-points are allowed to be incorrect in the sorted sequence. Memory access patterns are another aspect that are not captured in the O notation but can play havoc with empirical timing analyses. Sorting-with-errors could have potential applications in processing very-large sequence data. Loading... Reply Leave a Reply Cancel reply * Subscribe to Godel's Lost Letter [a28][a28] * [type and press enter] * Our Book [lrqmitbookcover] Click image for our page, with errata and links. * Recent Posts + Sorting and Proving + Laws and Laughs + Women In Theory + Easy as ABC + CCC 2022 Conference + Being Different + Hilbert's Lost Problem + Take Wing + Rafail Is No Secret + Differential Privacy + Peter's Face + Sedgewick to Emeritus Status + Math Monthly + A Paradox + Discussion About Proving--Again * Top Posts + Sorting and Proving + Laws and Laughs + Easy as ABC + The Godel Letter + Sedgewick to Emeritus Status + Women In Theory + Hilbert's Lost Problem + About Us + Mathematical Search + Branch And Bound---Why Does It Work? * Recent Comments [4adcc][4adcc] space2001 on Sorting and Proving [53463][53463] Jon Awbrey on Sorting and Proving Sorting and Proving... on Discussion About Proving... Sorting and Proving... on Sedgewick to Emeritus Status [7f5bf][7f5bf] KWRegan on Laws and Laughs [a4dee][a4dee] wjrapaport on Hilbert's Lost Problem [138dd][138dd] PaR on Laws and Laughs [d66ce][d66ce] rdmounce on Laws and Laughs [d66ce][d66ce] rdmounce on Laws and Laughs [204e7][204e7] jemand on Laws and Laughs [b5f02][b5f02] David in Tokyo on Laws and Laughs [a23b9][a23b9] Gil Kalai on Laws and Laughs [b083b][b083b] Jon Awbrey on Laws and Laughs [d66ce][d66ce] rdmounce on Laws and Laughs [afaa6][afaa6] rjlipton on Laws and Laughs * Blogroll + Alex Walker + Algorithmic Game Theory + Algorithms, Nature, and Society + AMS + Annoying Precision + Azimuth Project + Banach's Algorithmic Corner + Bits and Pieces + Blame It On The Analyst + Computational Complexity + David Mumford + Division by Zero + Ernie's 3D Pancakes + gentzen + Gil Kalai + Gowers's Weblog + Joel David Hamkins + Jon Awbrey + Kamathematics Home + Luca Trevisan + M-Phi + Martin Schwarz + math less traveled + mathbabe + Matt Baker + Michael Mitzenmacher + Michael Nielsen + Minimizing Regret + My Biased Coin + Not Even Wrong + Oddly Shaped Pegs + Peter Cameron + Pink Iguana + prior probability + Random bits + Rich DeMillo + Rigorous Trivialities + Scott Aaronson + Sebastian Pokutta + Secret Blogging Seminar + Suresh Venkatasubramanian + Tanya Khovanova + tcs math + Terence Tao + the Higher Geometer + The Mathematical Tourist + The nth Root + the polylogblog + The Unapologetic Mathematician + Todd and Vishal's blog + Turing Machine + windows on theory * Archives Archives [Select Month ] * Sitemeter Site MeterSite Meter * wordpress statwordpress stat Powered by WordPress.com. Loading Comments... Write a Comment... [ ] Email (Required) [ ] Name (Required) [ ] Website [ ] [Post Comment] %d bloggers like this: