INTUITION FOR (P3) ================== The following example gives some intuition behind (P3). The underlying sequent is: (1+1)*(X&X), (1+1)*(Y&Y), (X'*Y')*Z', Z&Z where + = plus, * = tensor, W' = perp(W), and 1 = tensor unit. (Proof nets extend to the tensor unit 1 in the obvious way; if you're not happy with that, view each 1 as (P par P') for a fresh atom P each time.) The proof net N necessarily has 2^3=8 linkings. Links on X/Y/Z atoms are determined, so it suffices to specify how the "+"s choose their 1's: (a) in (1+1)*(X&X) choose the right 1 iff Z&Z is left and Y&Y is right; (b) in (1+1)*(Y&Y) choose the right 1 iff Z&Z is right and X&X is right. Alternatively, N is the translation of the following MALL proof. (Here "I" is a distinguishable occurrence of the tensor unit 1, "(1+I)" is abbreviated to "2" on occasion, and I omit the unique proofs of X&X,X' and Y&Y,Y'. The "right iff..." labels are just to help you pattern-match with (a) and (b) above.) "(a) right iff "(b) right iff Z&Z is left and Z&Z is right and Y&Y is right" X&X is right" | | | | | | V V 1 I 1 I --- --- --- --- 1+I X&X,X' 1+I X&X,X' 1+I Y&Y,Y' 1+I Y&Y,Y' ---------- ---------- ---------- ---------- 2*(X&X),X' Y,Y' 2*(X&X),X' Y,Y' 2*(Y&Y),Y' X,X' 2*(Y&Y),Y' X,X' --------------- --------------- --------------- --------------- 1 2*(X&X),Y,X'*Y' 2*(X&X),Y,X'*Y' 1 2*(Y&Y),X,X'*Y' 2*(Y&Y),X,X'*Y' --- ------------------------------- --- ------------------------------ 1+I (1+I)*(X&X),Y&Y,X'*Y' 1+I (1+I)*(Y&Y),X&X,X'*Y' ----------------------------- ----------------------------- (1+I)*(X&X),(1+I)*(Y&Y),X'*Y' Z',Z (1+I)*(X&X),(1+I)*(Y&Y),X'*Y' Z',Z ------------------------------------ ------------------------------------ (1+I)*(X&X),(1+I)*(Y&Y),(X'*Y')*Z',Z (1+I)*(X&X),(1+I)*(Y&Y),(X'*Y')*Z',Z -------------------------------------------------------------------------- (1+I)*(X&X),(1+I)*(Y&Y),(X'*Y')*Z',Z&Z The &-rule skeleton of this proof looks like this: ----&X ----&X ----&Y ----&Y . . . . . . . . ---------&Y ---------&X . . . . -----------------------&Z (Here "&X" means "the & of X&X".) Here's how we obtain some intuition for (P3), in terms of "harmless switching cycles" and "phantom cyclic dependencies". Consider the following switching cycle C (only the relevant subgraph is shown): jump1 _______ jump2 / _\__________ / / \ \ I X / \ Y I / /__/ \__ / / + & & + \ / \ / * * C is "harmless" in the following sense: - jump1 exists only when Z&Z is left, and - jump2 exists only when Z&Z is right, therefore any set of linkings for which C is present *must* toggle Z&Z; hence C cannot witness a failure of (P3). "Harmless switching cycles" such as C correspond to "phantom cyclic dependencies", defined as follows. Recall the &-rule skeleton of the proof: ----&X ----&X ----&Y ----&Y . . . . . . . . ---------&Y ---------&X . . . . -----------------------&Z ("&X" = "the & of X&X".) In the left branch &X is forced to come above &Y, and in the right branch &Y is forced to come above &X ("forced" in the sense that every sequentialisation of our proof net N must be like this). Thus if we write "&X-->&Y" for "the &X rule is forced to come before/above the &Y rule" (think of "&X needs &Y" or "&X depends on &Y"), then we have the following diagram of dependency: ------> &X <------ &Y | | | | `--> &Z <--' But this "cyclic dependency" of &X on &Y and &Y on &X is merely a relic of the superposition of the two branches of the proof: &X-->&Y holds only in the left branch of the proof, and &Y-->&X holds only in the right branch. This kind of bogus cyclic dependency, arising from superposition, is what I call a "phantom cyclic dependency". DJDH 2003/07/10