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