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

Sequentialized Empires and Kingdoms



Date: Thu, 21 Nov 91 14:19:38 GMT
To: linear@cs.stanford.edu

In response to Patrick Lincoln's note about the sequent calculus 
analog of empires and kingdoms:

What you say about the empires coincides with a result of mine
in the paper "Proof Nets for MALL" (submitted to the Annals),
which holds for the whole propositional LL including exponentials 
(provided that we agree on a discipline for the constants, e.g., 
apply/permute the \bottom rule-weakenings immediately after the axioms). 
I use the notions of proof-nets for MALL and slicings as in a previous
message.
 ----------------------------------------------------------------------
There are maps
                      *                  star
Sequent Derivations   ---->  Proof Nets  ----> Families of Slices

with the following property: 
(writing D^*, D^{*\ast}, but also A^* for A a formula-occurrence in D,
and also N^-*, etc.)

Theorem: Let D be any derivation of Gamma in propositional linear logic.
For every formula A occurring in D there exists a derivation D',
which is obtained from D by permuting the order of inferences, 
with the following properties:

(1) Suppose A is introduced in D by either the \otimes rule or 
the \par rule or by a Contraction with active formulas A_1 and A_2;
let B = A^*, B_1 = A_1^*, B_2 = A_2^*; then

(i) D^* = (D')^*;

(ii) in D', (e(B_1) U  e(B_2))^{-*} is the set of formula occurrences
that are introduced above A (= B^{-*}). 

(2) Suppose A is introduced in D either by the \oplus rule or 
by Weakening or Dereliction; let B = A^*; then

(i) D^* = (D')^*;

(ii) in D', (e(B))^{-*} is the set of formula occurrences that are 
introduced above A (= B^{-*}).

(3) Suppose A is introduced in D by the \with rule; let B = A^*; then

(i) D^{*\star} = (D')^{*\star};

(ii) there is B' in D'^* such that (e(B))^star = (e(B'))^star and 
in D', (e(B'))^{-*} is the set of formula occurrences that are 
introduced above A (= B'^{-*}).
 -----------------------------------------------------------------------
It seems reasonable that one should prove the corresponding result 
for kingdoms.

I should say that nobody else has yet checked (3), although (1) 
and (2) are established.


Gianluigi Bellin