[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