Two proofs about the Diplomacy rulesAs said earlier, the interpretation of the official rulebook is encoded in the equations, while any follow up is a matter of mathematics. In this chapter we will prove two properties of the rules. But first, I have to introduce the notion of a “dependency graph”. If we look again at figure 9:
Then we can make a directed graph between the dependencies of the orders:  The arrows no longer represent moves, but dependencies. Resolving the North Sea order depends on both on the resolution of Norway and on the resolution of the support order of Skagerrak. This is shown by the two arrows originating from nth. Some people might like to draw dependency arrows in the opposite direction: however, this way the dependency arrows have the same direction as the movement, and in the case of the simple recursive algorithm, recursion is entered in the direction of the arrow. In the dependency graphs we only look at the real move, support and convoy orders. The equations do also have other values — attack strength, hold strength, and so on — but those are shortcut in the graph. In case of the convoy paradox of figure 7:
The dependencies are as follows:  Although the army in Tunis plays a major role in this convoy paradox, the resolution of the Tunis order is not part of the cyclic dependency. In resolving the support order of Fleet Greece it is important to know whether the fleet in the Ionian Sea will start the convoying operation or not, but the success or failure of the Tunis order is irrelevant. This example shows that there is a subtle difference between a dependency on the existence of an order and a dependency on the resolution of an order. The existence of the Tunis order may cut the support in Greece as a result, but the resolution of the Tunis order is of no importance for that matter. This subtle difference occurs also in much simpler situations. Consider the bounce situation of figure 6:
If we remove the move orders for Berlin and Warsaw from the order set, then the army in Bohemia could advance. So the resolution of the Bohemia order depends on the existence of the Berlin and Warsaw orders. However, if we look at the equations, then we see that the resolutions of the Berlin and Warsaw orders are of no importance to the resolution of the Bohemia order. To adjudicate the Bohemia order we need to calculate the attack strength of the Bohemia unit and the prevent strength of both the army in Berlin and the army in Warsaw. The prevent strength of the Berlin unit is dependent on the success of the support of Munich. For those calculations we do not need to know the success or failure of any move. As a result, the dependency graph is (surprisingly) as follows:  The dependency graph indicates (correctly) that after resolving Munich, any of the orders Berlin, Bohemia or Warsaw can be adjudicated. Having established the concept of a dependency graph, we now want to prove the following: THEOREM I
No order can be part of two different cycles of dependencies. This means that an order set with the following dependency graph cannot exist:  Both x and y are part of a cycle with p and a cycle with q, which violates the theorem. To prove this theorem, we have to distinguish between 6 types of orders, which are listed in the following table:
The dependencies in the last column list the type of orders on which the resolution of the order can depend directly or indirectly. The set of support orders is split between orders of type D and orders of type E. The purpose for this split is to distinguish between orders that are subject to the dislodgement rule (a support is cut when it is dislodged), and those that are not. Formally, the dislodge rule would still apply for orders of type E: however, the rule is not relevant for that type, since the support is already cut by the simple fact that the unit is being attacked by the unit that may dislodge. Again, remember the difference between a dependency on the existence of an order and the resolution of an order. Support orders of type E can be cut due to the existence of an order of type C, but cannot depend on the resolution of an order of type C. The detailed proof of each of the dependencies can be derived from the equations and is left as an exercise for the reader. When we have a situation on the board, we mark every dependency and every order that is in a cycle. We cannot remove the unmarked orders from the scene, because those orders can play a role in the adjudication of the marked orders in various ways. If we observe the dependencies, then the marked orders (connected by marked dependencies) form pockets (islands) that consist entirely of orders of type A, or a mixture of B, E and F. Still, a single pocket may contain an order that is part of multiple cycles. For a pocket that consists only of orders of type A, it is rather clear that these orders form one circular movement, with all orders in one cycle. The same counts for a pocket with orders of type B, E and F, because a movement of type B can only disrupt one convoy, a support of type E can only support one unit, and a convoy of type F can only convoy one unit. Although the above reasoning may look obvious, it gave me a headache to get the right arguments. The tricky part is that the orders that can influence the order of the row are written down in the third column of the table. Thus, an order of type B, E, or F can only be influenced by the resolution of an order of type B, E or F. However, to prove that a pocket of B, E and F orders cannot have orders that are part of multiple cycles, we look at the dependencies in the opposite direction (the influence of the order). Thus, the overall proof consists first of limiting the scope to pockets of certain types of orders, and second of proving that those pockets constitute a single cycle. For the convoy paradoxes, in the second step we look at the dependencies in the opposite direction. This ends the proof of Theorem I. Theorem I implies that if we have a cycle, then any order on which the cycle depends, can be resolved first. Consider the dependency graph based on figure 9 drawn in figure 11: We maybe could extend the situation and make the success of the Skagerrak order dependent on other orders. However, we could never make the resolution of the Skaggerak order dependent, directly or indirectly, on North Sea, Norway, or Norwegian Sea. If so, the North Sea order would be in the cycle nth-nwy-nwg and in another cycle with ska. This violates theorem I. This is true in general, meaning that in case of a cycle, all orders on which the cycle depends can be resolved first. This counts even when the orders on which the cycle depends contain an independent cycle. Consider the following dependency relationship:  In such a situation, the pqr cycle can be resolved first, resolving all orders on which the xyz cycle depends. The dependency relationship of this figure does not violate theorem I, because every order is part of at most one cycle. Nevertheless, this situation cannot occur with the standard rules. The proof is left as exercise for the reader. Of course, a variant rule might introduce this kind of situation, but that does not concern us for now. Given the fact that any order on which a cycle depends can be resolved first, we want to prove: THEOREM II
In case of the following conditions:
Then there is at least one order in the cycle that can be resolved based only on partial information. We prove this by contradiction. That is, we assume:
Back to the dependency graph of figure 11: If the resolution of the order to Fleet Skagerrak makes the order to Fleet Norway irrelevant for purposes of resolving the order to Fleet North Sea (which is the case when this graph is based on the situation of figure 9), then the order of the North Sea can be adjudicated based on partial information. This means that if we respect the assumption that none of the orders in the cycle can be resolved with only partial information, the cycle may depend on other orders, but that those other orders may not make the dependencies on the orders within the cycle irrelevant. This restricts the dependency relations within the cycle. Suppose we have a direct x→y dependency in the cycle. Since y must be relevant for x, a different value for y must mean a different value for x (note this is only true because y is limited to two values). This means that x has the same resolution as y (x fails when y fails and x succeeds when y succeeds) or x has the opposite resolution of y (x fails when y succeeds and x succeeds when y fails). From the initial assumption we know that there is one exclusive resolution. From the restricted dependency relations, it follows that the opposite of the resolution must also be a resolution respecting the equations. But this contradicts the assumption that there is a single resolution. And this proves Theorem II. Theorems I and II together prove that an algorithm that can make decisions based on partial information will find the unique resolution for a cyclic dependency.
|
