Long proofs are not always the most important results
Michael Rabin is visiting Georgia Tech today and tomorrow to give a pair of distinguished lectures. Both of these will be on applications of cryptography. One is to help auctions avoid cheaters, while the other is to help elections avoid cheaters. I see a pattern. Ken sees another pattern— he is helping chess tournaments avoid cheaters.
Today I want to comment about Rabin’s fame and what makes a result important.
I have known Michael since I was a graduate student at CMU—I have talked about this before here. In the decades since then I have heard him given many talks, all of which have been brilliant. He is one of the best presenters of technical material I have every seen, perhaps the best in the world. My “proof” of this statement is:
that I can still recall—in detail—most of his talks, even ones from decades ago.
Can you recall that talk you heard last year, or even one you heard last month? I have trouble recalling my own talks. But Michael’s talks are special, memorable, informative, clear, and fun.
I have selected a few talks of Michael that I recall in great detail—they span about forty years. There are many others that I could have added, but these should make my point.
His talk on Theoretical impediments to artificial intelligence, was the first of his talks that I had ever heard. It was at the 1974 IFIP Congress, which occurred in Stockholm Sweden. There was a time when the IFIP Congress was a major conference that many of us went to. I met Dick Karp there for the first time.
His talk on the introduction of randomness to algorithms, which was given at Yale when I was there as a junior faculty member. It was in 1977, I recall. This talk made the case for the power of randomness—Michael showed that randomness could help in a certain geometric search problem. I talked about this in detail in the same post with the CMU story.
His talk on the Karp-Rabin pattern matching algorithm was given in the 1980′s at Princeton University. We have also talked about this before here.
His talk on hyper-encryption was given at Georgia Tech about ten years ago. This was an cool idea—I believe—on using non-complexity assumptions to build encryption methods that were very powerful. The short insight was that memory is expensive, and one could defeat an adversary that had limited memory. This yielded a protocol that needed no assumptions about factoring or the existence of one-way functions.
Why indeed is Rabin famous? He received the Turing Award with Dana Scott for their work on finite state automata (FSA). I would argue that his most exciting results were curiously his least deep results. We all know about FSA; his introduction of randomness to all parts of computing; his primality test, independent but related to Gary Miller’s work; his pattern matching algorithm with Karp; and much more. Yet, I would argue that his deepest result is probably his least known. It was, is, his brilliant work on S2S.
Second Order Monadic Theory
What is S2S?
There are many logical theories that we study, such as Peano Arithmetic (PA). PA is a first-order theory. This means that quantifiers can only range over individual elements—in PA they range over integers. Thus, in PA we can say
This states that all numbers have a non-zero multiple that is a sum of two cubes. This is true—but it is not trivial.
The reason PA is so powerful is that it allows both addition and multiplication. Given a statement like the above about cubes it is impossible, in general, to decide whether the statement is true or not.
We obviously like decidable theories since at least in principle they allow us to tell if a statement is true or false. Of course if , then even for a decidable theory it may be hard to tell whether something is true. But still decidable is a great property for a theory to have.
A difficulty is the tension between being an expressive theory and being decidable. PA is very expressive, most everyday theorems of mathematics can be proved in it, at least in principle. It is so expressive that even weak subtheories are undecidable.
Enter S2S. The theory S2S is a different kind of theory from PA. While PA is a first-order theory, S2S is a second-order theory. The “S” in “S2S” stands for second order. It allows quantifiers to range over individual elements and also over finite or infinite sets of elements. The basic objects in S2S are finite paths in the infinite binary tree.
In S2S we can talk about the left and right successor to any such element: if is an element, then and are the respective successors. Since it is a second order theory we are also allowed quantifiy over sets of such elements.
Decidedly More Power
The magic of this is that while the theory is expressive, it is not too expressive. Indeed the Rabin proved in 1969:
Theorem 1 The monadic second order theory of the infinite binary tree is decidable.
When I first looked at Rabin’s paper, as a graduate student at CMU, it was not the depth of his proof, which is wonderful, but rather the array of applications that followed that excited me. One measure of the depth of a theorem is the number of open problems it solves. Rabin’s theorem can be used to prove the following other theories are decidable:
- The first order theory of rationals with the order relation.
- The first order theory of boolean algebras with ideals.
- Certain modal logics, such as S4.
These results follow by encoding the decidability question into the powerful theory S2S and invoking Rabin’s Theorem. See this for a nice summary of S2S in slide format by Shane Steinert-Threlkeld.
The proof of Rabin’s Theorem was a tour-de-force. It requires clever definitions and some quite detailed inductive arguments. Since his original proof people have found “easier” proofs, but the original was quite deep and intricate.
I would argue that this theorem is one of the deepest results of Rabin’s many beautiful results over his long career. It is well known to those who work in logic and automata theory, but is perhaps less known to the whole theory community. If you already knew it fine, if not, then I hope you begin to appreciate the depth of his work.
Perhaps a lesson here for all: fame comes from results that are game-changers, which does not always mean they are deep long complex arguments. Sometimes that is the case: clearly the solution to Fermat Last Theorem and the Poincaré Conjecture are famous and deep results. Yet many times I think Rabin’s situation is more often the case: a simple to state result that yields an “ah” moment, that opens doors for others, that changes the landscape of thinking about an area, is the most important type of result. Rabin has many many of these results. I would argue that without S2S he still would be one of the greatest theorists who has ever lived.
What do you think?
Results and problems about primes that make us think of coding theory
Cropped from source.
Zhi-Wei Sun is a professor in Mathematics at Nanjing University in China. He is the Editor in Chief of the recently-founded Journal of Combinatorics and Number Theory. His homepage is unique in prominently featuring a long list of
- …not his awards,
- …not his papers,
- …not his theorems,
- …but rather his conjectures.
Indeed we count 432 total conjectures in his list, subtracting one that he seems last year to have proved. They do not seem to be easy conjectures—this one implies the Riemann Hypothesis in a nontrivial way. Some of them involve powers of 2, which lend them a coding-theory flavor.
Today Ken and I wish to share ideas of using coding theory to prove number-theoretic results. Read more…
The computational power of plants
Martin Howard and Alison Smith are research scientists at the John Innes Centre (JIC) in Norwich, England. JIC was founded as a horticultural institution by the philanthropist John Innes in 1910, and is today one of several independent institutes affiliated to the University of East Anglia. Howard and Smith are the senior scientists on a paper that claims to show that plants can perform arithmetic division. Their co-authors are Antonio Scialdone, Sam Mugford, Doreen Feike, Alastair Skeffington, Philippa Borrill, and Alexander Graf.
Today I thought we might look at their claim and see if theory can shed any light on it.
Solving is believing
Cropped from source.
Boris Konev and Alexei Lisitsa are both researchers at the University of Liverpool, who work in Logic and Computation. They have recently made important progress on the Erdős Discrepancy Problem using computer tools from logic. Unlike the approach of a PolyMath project on the problem, their proof comes from a single program that ran for just over 6 hours, a program administered only by them, but mostly not written by them.
Today Ken and I wish to talk about their paper and two consequences of it. Read more…
Do our computers live in a simulation?
René Descartes is famous for countless things in mathematics—Cartesian products, Cartesian coordinates, Descartes’ rule of signs, the folium of Descartes. He is also famous for his work in philosophy and the notion of an evil genius. The evil genius presents a full illusion of a reality, and “fools” Descartes into believing there is a reality, while actually there is none.
Today Ken and I want to talk about the evil genius, and its relationship to the simulation hypothesis.
Comments on three papers from the Conference on Computational Complexity
Michael Saks is Chair of the Program Committee of this year’s Conference on Computational Complexity (CCC). He was helped by Paul Beame, Lance Fortnow, Elena Grigorescu, Yuval Ishai, Shachar Lovett, Alexander Sherstov, Srikanth Srinivasan, Madhur Tulsiani, Ryan Williams, and Ronald de Wolf. I have no doubt that they were faced with many difficult decisions—no doubt some worthy papers could not be included. The program committee’s work does not completely end after the list of accepted papers is posted, but it is not too early to thank them all for their hard work in putting together a terrific program.
Today I wish to highlight three papers from the list of accepted ones. Read more…
How can we possibly see atoms?
John Sidles is a medical researcher and a quantum systems engineer. His major focus is on quantum spin microscopy for regenerative medicine. He is both Professor of Orthopedics and Sports Medicine in the University of Washington School of Medicine, and co-director of the UW Quantum Systems Engineering Lab. Watching various injury troubles at the Sochi Winter Olympics makes us wonder whether quantum sports medicine is an idea whose time has come. Well beyond some media’s overheated references to our athletes as “warriors” is a nice reality: John’s main project is for healing those injured in the armed services.
Today Ken and I wish to talk about John and his work in general. We especially like his title of quantum systems engineer. Read more…