[Prev][Next][Index][Thread]
re: more about kingdoms

To: types

Subject: re: more about kingdoms

From: Gianluigi Bellin <glb@dcs.edinburgh.ac.uk>

Date: Wed, 27 Nov 91 17:33:52 EST

InReplyTo: Vincent Danos <danos@logique.jussieu.fr> Sat, 23 Nov 91 13:58:43 EST

Sender: meyer@theory.lcs.mit.edu
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 proofnets 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 "backandforth"
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