Two Generals and Time Machines
mwhittaker.github.io
mwhittaker.github.io
As a rule of thumb, if you could replace the word "formal" with "mechanical" and your sentence would still be true, then you can use the word formal (this is the case, say, with formal software verification, which is simply mechanical software verification, or formal proofs in a proof assistant, that are mechanical proofs). So, a formal description is one that could be directly mechanically interpreted by a simple computer program as written, and a formal proof is one that could be mechanically checked. If this is not the case -- use the word "precise" (or "mathematical" if you prefer). It's both simpler and more accurate.
As the description given here makes heavy use of natural language that is not easily interpretable by a computer, it is not formal, and since the proof makes use of a notion of a time machine, as well as others, not given a formal definition, it is very much informal, even if sufficiently precise to be acceptable as a mathematical proof.
That immediately forces the question: which machine?
> a formal description is one that could be directly mechanically interpreted by a simple computer program as written
Outside of automated theorem proving and checking, very little done in math or theoretical CS actually meets the definition you gave for 'formal'. E.g. the proof of FLT is clearly not 'formal', it has not been reduced to steps that are all machine-checkable. The proof of, say, the Halting Problem as is normally given is also not formal.
If you relax your definition of 'machine' to include 'humans with mathematical context following a sequence of steps', then most proofs can be 'formal', depending on how much context the proof assumes of the reader.
Anyway, I think the distinction you make is useful to think about, but in this context (where the audience is mostly non-mathematicians, of which CS theorists are a variety), the better definition of formal is not mechanical, but are we attempting to abstract the problem down into a collection of fixed rules, and it's clear the author has done so.
The principle of charity would ask of us to ask, 'Is there another definition of 'formal' that would be reasonable, even if it's not the definition that I am most accustomed to?'
Yes, I say, "in the context of proofs."
> That immediately forces the question: which machine?
From Aristotle and up until Turing (exclusive) the answer was no machine, but the mechanical application of formal -- i.e., "of form" -- inference rules. That this mechanical process could actually be carried out by a machine was only realized later. Today we know what "mechanical" means, and the word is better understood than "formal" in this context, so it's easier to explain that formal just means mechanical.
> Outside of automated theorem proving and checking, very little done in math or theoretical CS actually meets the definition you gave for 'formal'.
That's right, but mathematicians know they're working informally. It is true that on occasion you do see a mathematician use the word formal for an informal presentation and proof, but I think that mostly happens because they hear the word from logicians and computer scientists and may not know what it means. Given that the word in this context originated together with the concept of computation, computer scientists should know better.
> If you relax your definition of 'machine' to include 'humans with mathematical context following a sequence of steps', then most proofs can be 'formal', depending on how much context the proof assumes of the reader.
If the derivations are not done formally then they are not formal even if a human does them. We certainly do hope that most mathematical proofs have formal counterparts, but unless you provide the formal proof, or make the relationship of your proof to a formal one obvious, then you are not providing a formal proof.
> the better definition of formal is not mechanical, but are we attempting to abstract the problem down into a collection of fixed rules, and it's clear the author has done so.
I don't know if it's better or not, but it is not the one that has been used for centuries. For example, in the book Formal Logic (1847) by Augustus de Morgan, he writes, "This logical truth depends upon the structure of the sentence and not upon the particular matters spoken of." In this particular case, the discussion of time machines in the construction of the proof clearly was not related to the structure (form) of the presentation but on the particular matters spoken-of, hence it is informal.
See https://en.wikipedia.org/wiki/Logic#Logical_form and https://en.wikipedia.org/wiki/Logical_form
> 'Is there another definition of 'formal' that would be reasonable, even if it's not the definition that I am most accustomed to?'
I don't think it would qualify as a defintion, but clearly some people mean precise or mathematical when they say formal. This mistake is merely annoying and not serious. The reason that's annoying is that the words precise and mathematical are both more accurate and simpler/more familiar.
Note that 'formal' has another common definition in the context of software engineering: https://en.wikipedia.org/wiki/Formal_methods#Taxonomy
I like this definition because it explicitly shows formal is really a continuum—since in the limit, you should go all the way down to ZF, but in practice nobody actually does this. A hard, black-and-white definition for formal is simply less useful.
It seems that your objection can be summarized as: 'formally prove' has only a single meaning in the context of a proof, the mathematical one.
IMHO is uncharitable to the author, since there are other, looser definitions of 'formal' in the context of algorithm analysis and software engineering.
Not really, because he doesn't formalize the problem (i.e. write it in a formal system). But I may not have commented if the term "formal" wasn't so emphasized and used so often. This emphasis and repetition means that people simply don't know what formal means, and so I thought it was an opportunity to point out this rather common mistake.
> Note that 'formal' has another common definition in the context of software engineering
It's the very same definition. At all levels, the word "formal" actually means formal -- i.e., stated in a formal language.
> but in practice nobody actually does this.
100% of whatever it is that you do in formal methods is actually formal. You don't necessarily need a deductive formal proof, but in order to say formal you need to be formal. Static analyzers are 100% formal, as are model checkers. Even tests are 100% formal (although they don't fall under the umbrella term "formal verification" for unrelated reasons).
> there are other, looser definitions of 'formal' in the context of algorithm analysis and software engineering.
Not to my knowledge. I am not aware of any use of "formal" in the context of logic, proofs, computer science or software where it does not mean "mechanical".
"It will then formalize the Two Generals' Problem and formally prove the impossibility."
yes because i have heard of the word juxtaposition
>This guide will introduce the Two Generals' Problem and give an [INTUITIVE] explanation for why finding a solution to the problem is impossible. It will then formalize the Two Generals' Problem and formally prove the impossibility.
The problem states that the two generals have decided to attack but need to coordinate on when. Failure to attack at the same time will result in defeat.
Full details are available on Wikipedia:
Normally for the two generals problem, you assume if you retry a message indefinitely, the message will eventually be delivered. If this isn't the case, the problem is trivially impossible. If every message is dropped, the two generals cannot communicate with each other at all.
With this assumption, deciding on an action eventually becomes possible. Let's say the two generals strategy is the following. Each general individually decides to attack or retreat, then communicates their plan to the other general. If both general's agree they will execute that plan. Otherwise they will both retreat. To execute this strategy, the generals can use a protocol like TCP.
Each general repeatedly sends their plan to the other general until they receive an acknowledgement. Whenever a general receives a plan from the other general they send an acknowledgement, even if they have acknowledgement before. Based on the assumption above, if the first general keeps sending their plan, the second general will eventually receive it. When this happens the second general sends an acknowledgment. If the acknowledgement gets dropped, this cycle repeats. This is because the first general keeps sending the plan and the second general acknowledges it every time they receive it. Since the second general repeatedly sends the acknowledgement indefinitely, the first general will eventually receive it. Since both generals eventually receive the acknowledgement from the other general, using this algorithm will eventually finish.
This algorithm allows the generals to eventually agree an action. To see why the algorithm doesn't work for deciding on a time to attack, you can notice that in the above algorithm that each general never actually learns when both general's agree on an action. If a general doesn't know if the other general knows the plan, they cannot attack. If one general learns they are going to attack at 2pm, but the other general hasn't yet learned the time to attack, the first general will attack at 2pm, but the second general won't. Not only do you have to decide on a time, but each general needs to know that the other general has agreed with the time.
Doing this is impossible. The proof from Wikipedia looks something like the following. If the two generals eventually reach a point where they both know that "we will attack at 2pm" and "both generals know to attack at 2pm", there must have been some specific message where that statement became true. Without loss of generality, let's say that message was a message sent from the first general to the second. If that message was dropped, everything appears the same to the first general, but not to the second. The first general is now thinking "both generals will attack at 2pm", but the other general doesn't think that yet. This means that its impossible to construct any algorithm that works.
This is implicitly dropping the requirement that the actions be coordinated.
When the message is what to do, the when must have been previously agreed upon (e.g. "dawn of the day after we figure out what we're going to do").
> using this algorithm will eventually finish
No, the same problem exists as in the other scenario: neither general knows when the other learned the correct action to take, and cannot schedule it correctly.
> The article incorrectly defines the two generals problem.
> The [actual] problem states that the two generals have decided to attack but need to coordinate on when. Failure to attack at the same time will result in defeat.
Now, as far as Alice is concerned, both Alice and Bob acknowledged. However, Bob never got Alice's acknowledgement, so he won't attack.
But if we don't know that the other army is in position, and if Eve burns every message, then the problem is clearly unsolvable.
Working distributed systems have to work around this (and other) restrictions that are implicit to the properties of a distributed system. So TCP still works perfectly fine even though a perfect version of TCP (that didn't have timeouts) would be mathematically impossible to implement.
Another (practical) solution could be to spoof a message, making it appear as if from Eve. Some kind of steganography might work as well (or alternative forms of communication such as pigeons or smoke signals). And if all communications between Alice and Bob is discarded, this would worry either one of them to send a personal messenger who is human. This person could be captured and tortured, sure. But if they get "burned" as well, that'd be an act of war. Plus, if they are able to predetermine that if they don't hear from each other after X time, they attack after X + Y time (e.g. 3 months and 1 month [to prepare]) then the problem can be solved. If they cannot create a clear way of predetermined action based on actions then they'll always retreat.
Actually now that I gave it some further thought this "two general problem" can be observed in the cold war as well via (the nuclear threat of both parties). The nuclear threat from both sides created an equilibrium akin to what could happen in the described situation.
So they could choose as algorithm: never attack
(Even if they cannot meet beforehand, the above is a strategy they can figure out on their own assuming the other is also choosing an optimal solution. Never attack is better than always attack because it doesn't depend on timing)
Then they need no communication yet know what to do and what the other does.
So problem is solvable, and something is wrong in the proof? Or alternatively I missed something in the problem statement preventing the above.
What also makes it unsolvable is that you do not want to endanger more messengers than necessary, i.e you don't want to send the another messenger with a message already sent. It's impossible to always know whether or not the receiver really did get the last message.
Two ships on the ocean of two different civilizations (who don't have shared traffic rules, and they also cannot communicate) are by accident on a head-on collision course towards each other. To avoid collision, they each need to turn a different direction, not the same direction. So each needs to quickly decide which direction to turn.
(Actually, more recognizable: walking on a sidewalk in a different country where people appear to have a different, or no, convention about which side people should cross each other)
Both generals start with either 0 or 1, and the condition is that if both started with 0 (i.e., initially wanted to individually retreat), they should both output 0. Likewise for 1. The thing about Eve deciding which value the generals start with may also be confusing; a better way to think of it is that 'no matter what both generals start with, this validity condition holds'.
Alice sends a message saying "Attack on XX:XX on the nth day", and sends that message each day, with nth changing to (n - days)th. If the network (Eve) is lossy, it means she doesn't automatically burn all messages, so eventually, Bob will receive Alice's message. Bob then responds with the same message back to Alice, until Alice receives it.
I initially thought this would work, but the extra round-trip from Bob to Alice makes it a problem.
I suppose with a long enough 'n', one only needs 2 round-trips, but with a state beyond {0;1}, it's probably impossible to reach "eventual consistency"
So, I agree re. strong consistency; as the problem was about that, and not eventual consistency.
A sends "Attack?Send your plan"
B sends "Retreat,Send your plan"
A sends "Retreat,Send your plan"
B sends "Retreat,Send your plan"
A sends "Retreat,Send your plan"
B sends "Retreat,Send your plan"Here's another example: Alice asks Bob to attack in the morning. Bob accepts. But Eve doesn't let Bob's acceptance message to get to Alice. Alice waits for some time and asks Bob again to attack in the morning. Bob accepts. But message still doesn't reach Alice. If message does reach Alice before the attack, it's a win. If not, i.e. Eve holds messages past the attack time, only Bob attacks, as Alice won't know if he will.
A sends "Attack at 5:00, send your plan"
B sends "Attack at 5:00, send your plan"
A sends "Attack at 5:00, send your plan"
B sends "Attack at 5:00, send your plan"
A sends "Attack at 5:00, send your plan"
B sends "Attack at 5:00, send your plan"
Let’s say the last message in your example is dropped
B would have 3 acks from A while A only has 2 acks from B.
Will A attack? If not, B is left attacking on their own.
Similarly, what if none of Bs messages make it back to A? How does B know to attack?
I think it doesn't work because the problem becomes "when to retreat". It actually introduces a third state (attack; retreat; do nothing), where I might retreat today, and you do nothing.
Out of interest, if you set a time/date on when to retreat, how would the message look like, and how would you define confirmation for both parties?
This is wrong. Alice and Bob should be switched.
What is consensus [1]?
As oh_sign noted in an earlier comment here, if Eve blocks all messages there is obviously no way to achieve consensus, so if there are no constraints on Eve's ability to interfere this is a trivial problem, so I'm going to assume that Eve is not able to block everything.
Suppose each general does this:
1. Generate a random 128 bit integer, P.
2. Decide the action they are going to take, A (attack or retreat).
3. Repeatedly send the message: "I will do A with priority P". (To be clear, P is only generated once. That single P is used in all messages).
4. They take action A unless they receive a message from the other general that states a different action, A', AND the other general's message has a lower P. In that case, they take action A'.
Without loss of generality, assume Alice has the lower P.
With the above procedure, as long as a single message from Alice to Bob makes it through, the generals will take the same action, which will be the action Alice picked.
Although they take the same action, only Bob knows that they are going to do so. He knows this because since a message from Alice got through to him, he knows she has a lower P so will stick with her original action regardless of whether or not his messages got through, and he will match her action because he knows she has a lower P.
Is that consensus, or to count as consensus do they both have to know before they act that they will be taking the same action?
Let's say that they do both have to know. Modify the above procedure so that if a general finds out they have the higher P, they change the message they are repeatedly sending to "I will do action A', following your lead", where A' is the action from the other general's message.
With this modified procedure, if Eve lets one message through from Alice, and after that lets one message through from Bob, then (1) the two generals take the same action, (2) Bob knows they will be taking the same action, and (3) Alice knows they will be taking the same action.
Is that now consensus? They are taking the same action and they both know they are doing so. Furthermore Alice knows that Bob knows. Bob, however, does not know that Alice knows. Do we need not only agreement, but each knowing that there is agreement, and knowing that they each know, and knowing that they each know that they each know, ad infinitum?
[1] Are consensus problems usually stated in terms of agreements between generals because the definition of consensus is literally, at least in Oxford, "A general agreement"?
The missing piece in your algorithm is how long do they wait to receive a message from each other and how they can know that it's long enough? If they don't wait long enough they will not receive a message and will make wrong assumptions about the other general, will not reach consensus and will take each their own action. To fix this each has to wait as long as it takes to receive a message from the other general and know about this (which in itself requires more messages).
But what if one of the generals dies in the meantime and stops sending messages? Or what if both Bob and Alice got the same random integer? There are other issues too.
But the important thing is it's all about time. You can always wait out uncertainty, but of course you won't be able to make progress waiting.
The issue here is different to what you are modelling; imagine this payoff table for A
B attacks B holds
A attacks +1 -∞
A holds 0 0
The issue with your strategy is that even if Eve never interfered with the connection once, Alice does not know that, so will hold.
This problem keeps coming up in distributes systems and sadly, a full breakdown of internal communication is also possible.
I.e. internet routing works, switch for lan/cluster communication broke.
FTA:
> Eve receives every message and decides whether she wants to deliver the message or burn the message. She does not, however, get to open the enveloped message.
This is guaranteed to fail eventually, but if you can characterize the likelihood of dropping messages, you can set up agreed-upon sequences to improve the probability of eventual cooperation -- but you can never guarantee it.
For example: you can put checksums or hashes on your message to help detect corruption. You can put sequence numbers on your messages to help detect message loss. You can run an isochronous stream of very short messages to help decide on a base error rate, or to increase the likelihood of detecting a major loss. You can set up N different networks and hope that they don't all have losses at the same time.
All of these techniques help identify and remediate some degree of message loss, but cannot guarantee to solve it given a cantankerous enough -- or evil enough -- message killer.
That has been accounted for.
" [Eve] does not, however, get to open the enveloped message."
> timeouts and defaults it can be
These time-outs and defaults would have to be negotiated between the generals over the postal system and wouldn't help them.
> as seen by many the distributed systems on the Internet
Those would have implemented a form of fault-tolerance for the more general "Byzantine Generals Problem."
Can you point me at an algorithm that guarantees consensus? Your claim seems to be at odds with the formal proof in the article. I particular, the article already allows for encryption, timeouts, and defaults.
So I can't see how you are right, and would appreciate some additional information as to why you think the article is wrong.
If it's pragmatic to dismiss impossibility results, perhaps revisit pragmatism.