Skip to content

Fathering Randomized Fault Tolerance

June 21, 2015


Plus visiting Michael Rabin and talking about Gödel’s Theorems

BenOrRabin

Michael Ben-Or and Michael Rabin have won the 2015 Dijkstra Prize for Distributed Computing. The citation says,

In [two] seminal papers, published in close succession in 1983, Michael Ben-Or and Michael O. Rabin started the field of fault-tolerant randomized distributed algorithms.

Today Ken and I wish to congratulate both Michaels for the well deserved recognition for their brilliant work.

Ben-Or’s paper is titled, “Another Advantage of Free Choice: Completely Asynchronous Agreement Protocols.” Rabin’s paper, “Randomized Byzantine Generals,” brought randomness to a distributed consensus problem whose catchy name had been coined in 1982. The award committee said:

Ben-Or and Rabin were the first to use randomness to solve a problem, consensus in an asynchronous distributed system subject to failures, which had provably no deterministic solution. In other words, they were addressing a computability question and not a complexity one, and the answer was far from obvious.

Their work has continued to have a huge impact on the whole area of distributed computing. The fact that a negative result, an impossibility result, could be circumvented by using randomness was quite surprising back then. It changed the face of distributed algorithms by showing that a problem with no deterministic solution might still have a solution provided randomness is allowed. Besides being a beautiful result, it has great practical importance, since randomness can be used in “real” algorithms.

We applaud the prize committee—Paul Spirakis, James Aspnes, Pierre Fraigniaud, Rachid Guerraoui, Nancy Lynch, and Yoram Moses—for making such a thoughtful choice, which shows that even “old” results can be recognized. It took {2^{5}} years for Ben-Or and Rabin to be honored: we are glad they did not have to wait for the next power of two.

A Visit to Rabin

While we are thrilled to see Rabin honored for his work on distributed computing, we are even more excited to report that he is doing well. This year he had a serious health issue that required a major operation. The operation went well, but unfortunately during and after it Michael had serious complications.

I, Dick, just visited him at his home in Cambridge. I am happy to report that Michael seems to be on his way to a full recovery. He is as sharp as ever, and looks like he will be his normal self in the near future. This is great news.

LiptonRabinJune2015

We wish Michael and his wonderful wife Ruth and their daughters the best. His elder daughter, Tal Rabin, also works in cryptography; I heard her give a talk four years ago on their father-daughter research. Michael plans to be part of several upcoming events—a good sign that he is on the mend. Again our best wishes to Michael and his family.

Incompleteness

Most of my conversation with Michael was about friends, gossip, and funny stories. As always it was fascinating to hear Michael tell stories—he is such a great story teller. As I left, after over two hours together, I talked to him about research—if only for a few minutes.

He surprised me by averring that he had been thinking anew about the famous Incompleteness Theorems of Kurt Gödel. Recall the first of these theorems implies that in any sufficiently powerful consistent theory, there exist true sentences that are unprovable, and the second says the consistency of the theory is one of these sentences. There are by now many proofs of these great results: some short and clever, some longer and more natural, some via unusual connections with other parts of mathematics.

What could be new here? Michael pointed to recent proofs he really liked. These include an AMS Notices article by Shira Kritchman and Ran Raz. The thrust is that one can view the Second Incompleteness Theorem through the lens of Kolmogorov complexity as a logical version of the famous Unexpected Examination paradox. As expressed by Timothy Chow, this paradox goes as follows:

A teacher announces in class that an examination will be held on some day during the following week, and moreover that the examination will be a surprise. The students argue that a surprise exam cannot occur. For suppose the exam were on the last day of the week. Then on the previous night, the students would be able to predict that the exam would occur on the following day, and the exam would not be a surprise. So it is impossible for a surprise exam to occur on the last day. But then a surprise exam cannot occur on the penultimate day, either, for in that case the students, knowing that the last day is an impossible day for a surprise exam, would be able to predict on the night before the exam that the exam would occur on the following day. Similarly, the students argue that a surprise exam cannot occur on any other day of the week either. Confident in this conclusion, they are of course totally surprised when the exam occurs (on Wednesday, say). The announcement is vindicated after all. Where did the students’ reasoning go wrong?

Michael said something about getting sharper bounds on the Kolmogorov complexity constant {L} involved in their article. There wasn’t time to go into details, so we had to leave the discussion “incomplete.” So I asked Ken to try to help reconstruct what Michael was seeing and trying to do.

Gödel’s Theorems

I, Ken, usually give only a quick taste of Gödel’s theorems in one lecture in Buffalo’s introductory graduate theory course. Let {Q(e)} be the predicate that the Turing machine {M_e} with numerical code {e} never halts when run on empty input. Let {F} be a strong effective formal system such as Peano arithmetic or set theory. Then I show (or give as homework) the following two observations:

  • The set {T} of {e} such that {F} proves {Q(e)} is computably enumerable.

  • But the set {U} of {e} such that {Q(e)} is true is not c.e. So {U \neq T}.

Now if {T} is not included in {U}, there is an {a} such that {F} proves {Q(a)} but {Q(a)} is false. {Q(a)} being false means that in the real world the machine {M_a} does halt on input the empty string {\lambda}. Hence there is some finite number {t} such that the decidable predicate {H(a,t)} (saying {M_a(\lambda)} halts in {t} steps) is true. By the strength assumption on {F} it proves all true and false cases of {H}, so {F} proves {H(a,t)}, but since {F} proves {Q(a) \equiv (\forall t)\neg H(a,t)}, {F} also proves {\neg H(a,t)}. This makes {F} inconsistent.

Thus if {F} is consistent, then {T} is included in {U}, and properly so by the c.e./not-c.e. reasoning. Taking any {b \in U \setminus T} gives a true statement {Q(b)} that {F} cannot prove.

Gödel’s diagonal method shows how to construct such a {b}, and Gödel’s definition of incompleteness also requires showing that {F} cannot prove {\neg Q(b)} either. This is more subtle: proving {\neg Q(b)} when {Q(b)} is true is not a violation of consistency as with proving {Q(a)} when {Q(a)} is false. Note that

\displaystyle  \neg Q(b) \equiv M_b(\lambda) \text{ does halt } \equiv (\exists t)\,H(b,t).

For reasons we put in Gödel’s own voice at the end of our second interview with him, it is possible to have a model with a non-standard integer {t_* > \mathbb{N}} in which the statements {H(b,t_*)} and {\neg H(b,t)} for all {t \in \mathbb{N}} all hold. This is why Gödel originally used a stronger condition he called {\omega}-consistency which rules out {F} proving {(\exists t)\,H(b,t)} and all the statements {\neg H(b,t)}. (As Wikipedia notes, since {H} is a halting predicate the restricted case called {\Sigma_1}-soundness is enough.) It took Barkley Rosser in 1935 to make this too work with just consistency as the assumption.

But if all we care about is having a true statement that {F} cannot prove, the c.e./not-c.e. argument appealing to consistency is enough. Then comes the “meta-argument” that if {F} could prove its own consistency, then because {F} can prove the c.e./not-c.e. part of the argument, {F} would prove {U \setminus T \neq \emptyset}. As Kritchman and Raz observe in related instances, this does not alone yield a concrete {b \in U \setminus T} such that {F} proves {Q(b)}, which is the real contradiction needed to deduce the second theorem. Still, I think the above is a reasonable “hand-wave” to convey the import of the second theorem with minimal logical apparatus.

The question becomes, How concrete can we make this? Can we push the indeterminate quantity {t} into the background and quantify ideas of logical strength and complexity in terms of a parameter that we can bound more meaningfully? Dick and I believe this objective is what attracted Rabin to the Kritchman-Raz article.

Concrete Gödel

Kritchman and Raz obtain the second argument without hand-wave and with minimal “meta” by focusing on the Kolmogorov complexity {K(x)} of a binary string {x}:

\displaystyle  K(x) = \min\{|e| : M_e(\lambda) \text{ halts and outputs } x\}.

Here {|e|} means the string length of {e}—that is, the length of the program {M_e} producing {x} from empty tape. Now let us imagine a function {C}—for Gregory Chaitin—that takes as parameters a description {d_F} of {F} and a number {L} and outputs a program {e = C(d_F,L)} that does the following on empty tape:

Search through all proofs in {F} of statements of the form ‘{K(x) > L}‘ and as soon as one is found, output {x}.

Then {|e| = |d_F| + \log_2 L + c}, where {c} is a constant independent of {F}. Whenever {L} exceeds a constant

\displaystyle  L_0 = -\frac{1}{\ln 2} W\left(\frac{-\ln 2}{2^{|d_F|+c}}\right),

where {W} is the Lambert {W}-function, we have {|e| = |d_F| + c + \log_2 L \leq L}.

Thus for {L \geq L_0} there are no proofs in {F} of the form {K(x) > L}, for any {x}—else by running {M_e} until it finds such a proof and outputs {x} we prove {K(x) \leq L_0} and so expose the inconsistency of {F}. Define {Q(x) \equiv K(x) > L_0}; then we need only find {y} such that {Q(y)} is true to prove the first theorem concretely. Most important, by simple counting that is provable in {F}, such a {y} must exist among the finite set {B} of binary strings of length {L_0 + 1}.

Kritchman and Raz conclude their argument by letting {S_m} be the statement “at least {m} strings {x \in B} have {K(x) > L_0}” for {0 \leq m \leq M = 2^{L_0 + 1}}, and {R_m \equiv S_m \wedge \neg S_{m+1}} (taking {S_{M+1} \equiv\,} false). There is exactly one {m} such that {R_m} is true, but {F} cannot even prove {S_m}: By the truth of {R_m} there are {M - m} strings {x \in B} with {K(x) \leq L_0}. {F} can guess and verify them all by running their programs {M_e} with {|e| \leq L_0} to completion. If {F} proves {S_m} then {F} deduces that all other {y \in B} have {K(y) > L_0}, which is impossible by the choice of {L_0}. Likewise, {F} cannot prove {S_M} since then it proves {Q(x)} for every {x \in B}.

We start a ball rolling, however, by observing that via the counting argument, {F} does prove {S_1}. So either {R_1} is false or {F} is inconsistent. This turns around to say that if {F} proves its own consistency, then {F} proves that {R_1} is false—which is like the “surprise exam” not being possible on the last day. But since {F} proves {S_1 \wedge \neg R_1}, {F} proves {S_2}. Hence either {R_2} is false or {F} is inconsistent. This turns around to make {F} deduce that its ability to prove its consistency implies the ability to prove {S_3}. This rips right on through to make {F} prove {S_M}, which however it can do only if {F} really is inconsistent. Thus {F} cannot prove its own consistency—unless it is inconsistent—which is Gödel’s second theorem.

The article by Kritchman and Raz has the full formal proof-predicate detail. There is a “{t}” lurking about—it’s the number of steps the programs {M_e} outputting {x}-es need to take—but the structure ensures that the eventuality of a non-standard length-{t_*} computation outputting an {x} never arises. The finiteness of {L_0} and {B} drives the improvement.

Along with Michael we wonder, what can be done further with this? Can we turn the underlying computability questions into complexity ones? The natural place to start is, how low can {L_0} be? If {F} is Peano arithmetic or set theory, can we take {L_0 = 1000}? This seemed to be what Michael was saying. It depends on {d_F}. And there is another thought here: We don’t need the length of {d_F} to be bounded, but rather its own Kolmogorov complexity, {K(d_F)}. Can we upper-bound this—for set theory or Peano—by setting up some kind of self-referential loop?

Open Problems

The main open problem is how fast will Michael be back in form. We hope that the answer to this open problem is simple: very soon. Congratulations again to him and Michael Ben-Or on the prize, and Happy Father’s Day to all.

[fixed inequality after Lambert W]

6 Comments leave one →
  1. June 21, 2015 11:15 pm

    That reminds me of the proof that there can be no uninteresting numbers.

  2. Serge permalink
    June 22, 2015 9:48 am

    I’ve been dreaming of a proof that, if a polynomial algorithm for a hard problem were found, then it would imply the inconsistency of Peano arithmetic with a nonzero probability. The reason is because such an algorithm would look too much like the proof that it can’t exist. I don’t know if that makes sense at all, but I find it interesting to use the probability of a contradiction in PA as a new kind of computational ressource. After all, solving a hard problem can drive you crazy sometimes…

  3. Geoffrey Irving permalink
    June 22, 2015 3:43 pm

    If further work establishes the bound on L more completely, I would love to hear about it!

  4. edon permalink
    June 23, 2015 5:47 pm

    Shouldn’t it rather be {|e| = |d_F| + c + \log_2 L > L_0} i.e. the inverse inequality, whenever {L} exceeds {L_0}

    • June 24, 2015 8:08 am

      Thanks. In fact the subscript 0 was the error—the point is to have just “L” on both sides.

  5. July 14, 2015 1:27 pm

    Congratulations, to Michael and Michael!

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s