![\"The](\"http:\/\/blogs.law.harvard.edu\/pamphlet\/files\/2011\/09\/mjrty-pattern1.png\")
<\/a><\/td>\n<\/tr>\nThis past week I was reading Robert Boyer<\/a> and J Strother Moore<\/a>‘s paper on computing the majority element of a multiset, which presents a very clever simple algorithm for this fundamental problem and a description of a mechanical proof<\/a> of its correctness. The authors aptly consider the work a “minor landmark\u00a0in the development of formal verification and automated reasoning”.<\/p>\n Below is the postscript to that paper, in its entirety, which describes the history of the paper including how and why it was “repeatedly rejected for publication”. (It was eventually published as a chapter in a 1991 festschrift for Woody Bledsoe<\/a>,\u00a0ten years<\/em>\u00a0after it was written, and is now also\u00a0available from Moore’s website<\/a>.)<\/p>\n In this paper we have described a linear time majority vote algorithm and discussed the mechanically checked correctness proof of a Fortran implementation of it. This work has a rather convoluted history which we would here like to clarify.<\/p>\n The algorithm described here was invented in 1980 while we worked at SRI International. A colleague at SRI, working on fault tolerance, was trying to specify some algorithms using the logic supported by “Boyer-Moore Theorem Prover.” He asked us for an elegant definition within that logic of the notion of the majority element of a list. Our answer to this challenge was the recursive expression of the algorithm described here.<\/p>\n In late 1980, we wrote a Fortran version of the algorithm and proved it correct mechanically. In February, 1981, we wrote this paper, describing that work. In our minds the paper was noteworthy because it simultaneously announced an interesting new algorithm and offered a mechanically checked correctness proof. We submitted the paper for publication.<\/p>\n In 1981 we moved to the University of Texas. Jay Misra, a colleague at UT, heard our presentation of the algorithm to an NSF site-visit team. According to Misra (private communication, 1990): “I wondered how to generalize [the algorithm] to detect elements that occur more than n<\/em>\/k<\/em> times, for all k<\/em>, k<\/em> \u2265 2. I developed algorithm 2 [given in Section 3 of [9]] which is directly inspired by your algorithm. Also, I showed that this algorithm is optimal [Section 5, op. cit.<\/em>]. On a visit to Cornell, I showed all this to David Gries; he was inspired enough to contribute algorithm 1 [Section 2, op. cit.<\/em>].” In 1982, Misra and Gries published their work [9], citing our technical report appropriately as “submitted for publication.”<\/p>\n However, our paper was repeatedly rejected for publication, largely because of its emphasis on Fortran and mechanical verification. A rewritten version emphasizing the algorithm itself was rejected on the grounds that the work was superceded by the paper of Misra and Gries!<\/p>\n When we were invited to contribute to the Bledsoe festschrift we decided to use the opportunity to put our original paper into the literature. We still think of this as a minor landmark in the development of formal verification and automated reasoning: here for the first time a new algorithm is presented along with its mechanically checked correctness proof\u2014eleven years after the work.<\/p>\n I have to think the world would have been better off if Boyer and Moore had just posted the paper to the web in 1981 and been done with it. Unfortunately, the web hadn’t been developed yet.<\/p>\n","protected":false},"excerpt":{"rendered":" I’m generally a big fan of peer review. I think it plays an important role in the improvement and “chromatography” of the scholarly literature. But sometimes. Sometimes. The Boyer-Moore MJRTY algorithm allows efficient determination of which shape (triangle, circle, square) is in the majority without counting each shape. This past week I was reading Robert […]<\/p>\n","protected":false},"author":2110,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[380,68],"tags":[],"class_list":["post-937","post","type-post","status-publish","format-standard","hentry","category-computer-science","category-scholarly-communication"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_shortlink":"https:\/\/wp.me\/p5pLfN-f7","jetpack-related-posts":[{"id":471,"url":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/2010\/06\/09\/a-proposal-to-simplify-the-university-of-north-texas-open-access-policy\/","url_meta":{"origin":937,"position":0},"title":"A proposal to simplify the University of North Texas open-access policy","author":"Stuart Shieber","date":"Wednesday, June 9, 2010","format":false,"excerpt":"\"In High Places\", statue by Gerald Balciar, University of North Texas - Denton campus, installed 1990. Image via Wikipedia. The University of North Texas is engaged in a laudable process of designing an open-access policy for their community. Draft language for their policy is now available at their site on\u2026","rel":"","context":"In "open access"","block_context":{"text":"open access","link":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/category\/scholarly-communication\/open-access\/"},"img":{"alt_text":"","src":"http:\/\/upload.wikimedia.org\/wikipedia\/en\/thumb\/c\/c4\/UNT_Eagle_statue.jpg\/300px-UNT_Eagle_statue.jpg","width":350,"height":200},"classes":[]},{"id":32,"url":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/2009\/05\/28\/open-access-policies-and-academic-freedom\/","url_meta":{"origin":937,"position":1},"title":"Open-access policies and academic freedom","author":"Stuart Shieber","date":"Thursday, May 28, 2009","format":false,"excerpt":"I very occasionally hear expressed a concern about the Harvard open-access policy that it violates some aspect of academic freedom. The argument seems to be that by granting a prior license to Harvard, faculty may be forced to forgo publication in certain venues.\u00a0 Our rights as scholars to determine the\u2026","rel":"","context":"In "open access"","block_context":{"text":"open access","link":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/category\/scholarly-communication\/open-access\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":2445,"url":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/2022\/07\/25\/moderating-principles\/","url_meta":{"origin":937,"position":2},"title":"Moderating principles","author":"Stuart Shieber","date":"Monday, July 25, 2022","format":false,"excerpt":"Some time around April 1994, I founded the Computation and Language E-Print Archive, the first preprint repository for a subfield of computer science. It was hosted on Paul Ginsparg\u2019s arXiv platform, which at the time had been hosting only physics papers, built out from the original arXiv repository for high-energy\u2026","rel":"","context":"In "computational linguistics"","block_context":{"text":"computational linguistics","link":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/category\/linguistics\/computational-linguistics\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":858,"url":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/2011\/06\/07\/the-nih-responds-to-my-letter\/","url_meta":{"origin":937,"position":3},"title":"The NIH responds to my letter","author":"Stuart Shieber","date":"Tuesday, June 7, 2011","format":false,"excerpt":"Front steps of National Library of Medicine, 2008, photo courtesy of NIH Image Bank Imagine my surprise when I actually received a response to my letters in recognition of the NIH public access policy, a form letter undoubtedly, but nonetheless gratefully received. And as a side effect, it allows us\u2026","rel":"","context":"In "open access"","block_context":{"text":"open access","link":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/category\/scholarly-communication\/open-access\/"},"img":{"alt_text":"Front steps of National Library of Medicine, 2008, photo courtesy of NIH Image Bank","src":"https:\/\/i0.wp.com\/blogs.law.harvard.edu\/pamphlet\/files\/2011\/06\/nlm-203x300.jpg?resize=350%2C200","width":350,"height":200},"classes":[]},{"id":431,"url":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/2010\/05\/01\/worlds-most-excruciatingly-ironic-conference\/","url_meta":{"origin":937,"position":4},"title":"World’s most excruciatingly ironic conference?","author":"Stuart Shieber","date":"Saturday, May 1, 2010","format":false,"excerpt":"Could this be the world's most excruciatingly ironic conference? \u00a0The Second\u00a0International Symposium on\u00a0Peer Reviewing (ISPR 2010) is soliciting papers. Their call for papers emphasizes the sorry state of peer-review, calling for\u00a0\"more research and reflections [that] are urgently needed on research quality assurance and, specifically, on Peer Review.\" What could be\u2026","rel":"","context":"In "scholarly communication"","block_context":{"text":"scholarly communication","link":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/category\/scholarly-communication\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":56,"url":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/2009\/05\/27\/some-background-on-open-access\/","url_meta":{"origin":937,"position":5},"title":"Some background on open access","author":"Stuart Shieber","date":"Wednesday, May 27, 2009","format":false,"excerpt":"I assume that readers of the open access discussions on this blog are familiar with the state of play in the area, but just in case, here's some background. Peter Suber defines open access in his A Very Brief Introduction to Open Access as follows: \"Open-access (OA) literature is digital,\u2026","rel":"","context":"In "meta"","block_context":{"text":"meta","link":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/category\/meta\/"},"img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]}],"_links":{"self":[{"href":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/wp-json\/wp\/v2\/posts\/937","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/wp-json\/wp\/v2\/users\/2110"}],"replies":[{"embeddable":true,"href":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/wp-json\/wp\/v2\/comments?post=937"}],"version-history":[{"count":18,"href":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/wp-json\/wp\/v2\/posts\/937\/revisions"}],"predecessor-version":[{"id":958,"href":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/wp-json\/wp\/v2\/posts\/937\/revisions\/958"}],"wp:attachment":[{"href":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/wp-json\/wp\/v2\/media?parent=937"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/wp-json\/wp\/v2\/categories?post=937"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/archive.blogs.harvard.edu\/pamphlet\/wp-json\/wp\/v2\/tags?post=937"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}