[Prev][Next][Index][Thread]
more about kingdoms; with reply by de Groote; comments by Lincoln
Date: Wed, 20 Nov 91 20:37:12 +0100
To: linear@cs.stanford.edu
After entertaining discussions between Jean-Baptiste L. Joinet,
Laurent T. Regnier, Georges C. Gonthier and myself, we may add
some remarks about kingdoms:
1. a quadratic computation for 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".
How prove this ? First equality is obvious.
For the second one: each F is certainly needed to connect A and B
under S, and k(A PAR B) does connect A and B, hence each F
belongs to it and therefore also their kingdoms.
Now just notice that the rhs of the second equality
is a connected union of subnets, and hence is a subnet.
2. a notion of A being "before" B:
Write A < B if A in kB, then A < B implies B not < A,
whereas this is not the case with empires.
In Girard's terminology kingdoms cannot be in opposition.
Alas they may have proper intersections;
take for example the obvious normal (highly commutative) proof of:
A PAR B, (B* TIMES C*) TIMES (A* TIMES D*), C PAR D
where the two PAR's have almost the same kingdoms.
3. a counter example to Gallier's conjecture "e-(X)=k(X):
Let X = (C* TIMES B*) PAR A* and take the obvious normal proof-net
of conclusions X and A TIMES (B PAR C). Then k(X) strictly contains e-(X)
which is therefore (for k(X) is by the very definition the smallest
subnet of R proving X) not a subnet.
Vincent Danos.
-------------------------
Date: Wed, 20 Nov 91 19:06:45 EST
From: drac@saul.cis.upenn.edu (Philippe de Groote)
To: linear@cs.stanford.edu
Subject: Re: more about kingdoms
Answer to Danos:
After Girard showed that our first definition of e- was not
complete, we tried to fix it by extending the closure conditions
as follows:
base case: A in e-(A)
axiomatic case: if B in e-(A) then B~ in e-(A)
tensor case: if B*C in e-(A) then B,C in e-(A)
par case: if B|C in e-(A) then D in e-(A), where D is any formula occurrence
lying on the path between B and C, for some switching S.
By trying to prove that e-(A) = k(A), we considered equations very similar
to Danos's:
> 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));
However, we encounter a difficulty in proving that such equations amount to an
inductive definition for we did not know how to prove that the k(F)
were strictly included in k(A PAR B).
In other word, using the above definition of e-, we did not know how
to prove that A was a conclusion of e-(A).
For instance, in the following proof structure (which is not a proof net)
A|B is not a concluson of e-(A|B).
_________________
| ___________ |
| | _____ | |
| | | | | |
| A B | A~ C~
| ----- | -------
C (A|B) B~ (A~|C~)
------- ----------
C*(A|B) B~*(A~|C~)
Is there an obvious reason that we overlooked?
Jean Gallier et Philippe de Groote.
------------------------------------
Date: Wed, 20 Nov 91 21:30:30 -0800
From: Patrick Lincoln <lincoln@theory.Stanford.EDU>
Subject: Sequentialized Kingdoms
I've been trying to figure out what a kingdom is in terms of
sequent calculus proofs. Perhaps someone who has thought through
these concepts can confirm or deny the following correspondences.
Essentially, the definitions below should just be the definitions of
empire and kingdom viewed through Girard's sequentialization theorem.
"Empire of A"
== e(A) (Girard)
== R1(A) (Regnier, Danos)
== e+(A) (Bellin, Gallier, deGroote)
=?= Se(A) (below)
"Kingdom of A"
== k(A) (Girard)
== R3(A) (Regnier, Danos)
=?= Sk(A) (below)
The sequent empire Se(A) in a sequent proof of |- Gamma
is everything that can be permuted above A. The sequent
kingdom Sk(A) is everything that can't be permuted below A.
That is, the sequent empire Se(A) in a sequent proof of |- Gamma
is the entire proof if Gamma = A,Sigma for some Sigma.
If A is not an element of Gamma, permute the sequent proof so that
A becomes a top level formula as low as possible in the proof tree,
then call that proof branch (rooted at the point A becomes top level) Se(A).
The sequent kingdom Sk(A) is similar, except that you permute the
proof so that A is analyzed as high as possible in the proof tree,
then call that proof branch (rooted at the point A is analyzed) Sk(A).
Somewhat more formally,
Define Se(A) in a sequent proof P of |- Gamma to be the largest proof
branch ending in the largest multiset Delta containing A in a legal
permutation of P.
Define Sk(A) in a sequent proof P of |- Gamma to be the smallest proof
branch ending in the smallest multiset Delta containing A in a legal
permutation of P.
The standard cut-normalization steps of sequent calculus are all legal
permutations. Any par inference introducing (A par B) may legally be
permuted below any tensor or par introduction where (A par B) is not a
subformula of the principal formula. Any tensor introducing (A times B)
may legally be permuted below any other tensor where (A times B) is
not a subformula of the principal formula, etc. Of course, legal
permutations preserve the the conclusion of a proof.
(Details: Largest and smallest are defined for multisets based on the
number of connectives plus the number of propositions in the multiset,
not based on the number of elements in the multiset. I view a sequent
proof as a tree with conclusion sequent at the bottom, and axioms up
at the leaves. "A is an element of Gamma", "A is a top level formula
in Gamma", "Gamma contains A", and "Gamma = A,Sigma for some Sigma"
mean the same thing for this note. The equality of interest here
is (Sequentialize k(A)) =?= Sk(A))
If Sk(A) and Se(A) are correct, then they give another method of
calculating the kingdom and empire, although this would require
a complete sequent proof to begin.
Questions: Are Se(A) and Sk(A) correct?
What is R2(A) (Danos, Regnier) in the sequent calculus view?
Here is another reference for proof nets with quantifiers:
@misc(
Girard91,Author="Girard, J.-Y.",
Title="Quantifiers in linear logic II"
HowPublished="CNRS - Paris 7 Prepublications, No. 19,"
Year="1991",
Month= "January")
pdl.
---------------------
END