[Prev][Next][Index][Thread]

re: more about kingdoms

Date: Mon, 25 Nov 91 12:38:08 GMT
To: linear@cs.stanford.edu

Congratulations, this is exciting!
 ---------------------------------------------------------------------
Given a proof net R and a set of formula occurrences F1,..., Fn in R, 
it makes sense to ask what is the intersection of all subnets
containing F1,...,Fn, call it k(F1,...,Fn).

It seems that one could generalize your computation of kingdoms

> k(A TIMES B)= k(A) TIMES k(B)
> Let S be any switch of R, then:
> k(A PAR B)= PAR(union(k(F); F in the path connecting A to B under switch S));
> where TIMES means "add the TIMES link between A and B"
> and PAR means "add the PAR link between A and B".

to cover this case. Suppose Fj is in e(Fi), then for any switch S

k(Fi,Fj)= union(k(F); F in the path connecting Fi to Fj under switch S).

Moreover, if Fj is also in e(Fm), then Fi, Fj and Fm are all in the 
empire of one of them, so that for any switch S there is a path
connecting Fi, Fj and Fm under switch S; more generally, if there
is a common intersection of all empires of F1,...,Fn, then we can define
for any switch S

k(F1,...,Fn) = 
   = union(k(F); for some j, F is in the path connecting all Fi's under S)

Suppose the e(Fi), e(Fj) are pairwise disjoint, we can choose a switching 
which is principal simultaneously for e(Fi) and e(Fj); now consider 
the minimal set of tensor links in R that establishes a connection 
between all the Fi under that switching. It seems to me that there 
is such a thing. Then for such a switching S, define

k(F1,...,Fn) = 
   = union(k(F); for some i,j, F is in the path connecting Fi with Fj under S)

[E.g., if for some A times B in R, F1 is above A and F2 is above B, 
then k(F1,F2) = k(A times B)]

Putting together the two definition, we obtain the general case.

 ---------------------------------------------------------------------

Further, if the construction of the kingdom k(F1,...,Fn) described above
makes sense, then we have the following algorithm for computing the 
kingdoms in the additive case. 

Clearly, for a \plus link with premise Ai we take
	k(A0 plus A1) = k(Ai) U {A0 plus A1}

Suppose we have a \with box containing proof-nets R1, R2 (let us suppose
without boxes first):

      -----------------------------
      |     R1               R2   |
      |                           |
      | A, Gamma         B, Gamma |
      --        ---------        --
	   A \with B,  Gamma

The kingdom of A\with B is computed by the following "back-and-forth" 
algorithm. Let Delta=k(A) and Theta=k(B).

For each D in Delta there must be a smallest D1 such that D is above D1
and a copy D2 of D1 occurs in R2. If Lambda is the set of such D2,
let Theta1 = k(Theta,Lambda), a kingdom in R2.
For each F in Theta1 there must be a smallest F1 such that F is above F1
and a copy F2 of F1 occurs in R1. If Xi is the set of such F2,
let Delta1 = k(Delta, Xi), a kingdom in R1.
Similarly construct Lambda1 and let Theta2 = k(Theta1,Lambda1), and so on.

There is a smallest fixed point, Gamma at worst, call it Gamma*. 
This yields the smallest box for A \with B. 

It would seem that these minimal boxes are the best candidates for "slicing".
Given the good behavior of kingdoms w.r.t. normalization, we would have
"good" commutative reductions as well.


Gianluigi Bellin