[Prev][Next][Index][Thread]
LINEAR logic forum; proofnets and kingdoms
Patrick Lincoln <lincoln@Theory.Stanford.EDU> has started a linear logic
email forum, linear@cs.stanford.edu. We agreed that, for the time being,
LINEAR will function as part of TYPES. Namely, LINEAR email will be
forwarded and moderated by me as TYPES mail. To avoid duplication, LINEAR
email will NOT be sent to the LOGIC forum. (FYI: It is possible to
subscribe to LINEAR without subscribing to TYPES.)
In the first few days of this arrangement there has already been an
interesting exchange concerning proof nets which is concatenated below.
Yours truly,
Prof. Albert R. Meyer
MIT Lab. for Computer Science
Moderator: types@theory.lcs.mit.edu
logic@theory.lcs.mit.edu
---------------------
Date: Sun, 10 Nov 91 20:43:49 -0800
Subject: about sequentialisation of multiplicative proof-nets
>From Laurent Regnier & Vincent Danos.
By proof-net we mean:
multiplicative proof-nets with n-ary axiom links (n>=1) and without neutral
elements (so proof-nets of LLM according to the notation of Scedrov).
Let R be a proof-net and A a (occurrence of) formula in R.
Any time you have a notion of R(A) a proper subnet of R with conclusion A
you can prove the sequentialisation theorem of Girard:
because both R(A) and R\R(A) (i.e., R minus the links and non-terminal
formulas of R(A) plus an n-ary axiom over the conclusions of R(A)
(that's why we allow general axioms)) are smaller proof-nets
(that's why R(A) should be a proper subnet of R)
hence are by induction sequentialisable and you just glue
together their two sequential proofs in the obvious way to build one
for R.
Two known examples (where l(A) is the link of R under A if there is one):
-- the girardian notion of empire:
R1(A)= the intersection of all correction subgraphs of R\l(A) containing A;
-- our notion of:
R2(A)= the union of all correction subgraphs of R\l(A) containing A.
Here is a new one and natural.
Let R3(A)= the intersection of all proper subnets of R containing A
which is indeed a proof-net (this needs some reasoning) with conclusion A.
(by the way the union of two intersecting subnets of R is also a subnet of R).
It's natural because R3(A) is by definition the smallest subnet of R
proving A.
An equivalent concrete way to define R3(A):
iterate (*) and (**) starting from R:
(*) erase any terminal PAR (distinct from A)
(** )if there is a splitting TIMES (distinct from A) just keep
the component containing A.
Equivalence with the abstract definition is shown
for example by sequentialisation.
---------------
Date: Mon, 11 Nov 91 20:14:44 -0800
Subject: Re: about sequentialisation of multiplicative proof-nets
From: chirimar@saul.cis.upenn.edu
>Let R3(A)= the intersection of all proper subnets of R containing A
>which is indeed a proof-net (this needs some reasoning) with conclusion A.
>(by the way the union of two intersecting subnets of R is also a subnet of R).
>It's natural because R3(A) is by definition the smallest subnet of R
>proving A.
This is an interesting remark as this is precisely the definition I use
to show the sequentialization theorem for the Multiplicatives and
Quantifiers for Linear Logic.
But the resualt of computing R3(A) coincides with Girard's notion of
empires. At least that's what I get. Are there any differences ?
-jawahar
-------------
Date: Mon, 11 Nov 91 20:28:14 -0800
Subject: a reply to danos/regnier
R3(A) is very natural and exciting ; i propose to call it kingdom
since it is smaller than the empire. The main idea is that the kingdom
of A might not cross a times link. Technically speaking the notion
has the enormous advantage of being -unlike empires- stable under
normalisation. However remains an important technical problem :
eA can be computed in linear time ; what about kA ?
jeanyves girard
----------------
Subject: Re: about sequentialisation of multiplicative proof-nets
Date: Tue, 12 Nov 91 07:32:06 +0100
From: Jean-Yves Girard <girard@margaux.inria.fr>
answer to chirimar
let P be a pf-net ending with B,A
let Q be a pf-net ending with C,notB
let R be the result of a cut between P and Q
in R we can compute both eA and kA (kingdom = R3(A))
eA = R
kA is included in P
jeanyves
----------
Subject: Kingdoms, empires, etc
Date: Tue, 12 Nov 91 11:52:15 EST
From: jean@saul.cis.upenn.edu
Philippe de Groote and I have had strongly related ideas.
We tried to give natural closure properties in order to define:
Given a proof structure satisfying D-R (Danos and Regnier's conditions,
of course)
(1) The largest sub proof net containing A as a conclusion.
(2) The smallest subproof net containing A as a conclusion.
It seems that R3 corresponds to (2) and that (1) corresponds to Girard's
empires. We have the following result and conjecture:
Consider the graph spanned by the least set of nodes e+(A) satisfying the
closure conditions e+:
A is in e+(A)
If B atomic, then B is in e+(A) iff B^perp is in e+(A)
If (B tensor C) is in e+(A) then both B and C are in e+(A)
If (B par C) is in e+(A) then both B and C are in e+(A)
If B or C is in e+(A), B not= A, C not= A, then B tensor C is in e+(A)
If B and C are in e+(A), B not= A, C not= A, then B par C is in e+(A)
Note, these conditions are the imperialistic properties.
Fact: e+(A) = e(A) the empire of Girard. This is shown using
sequentialization.
Consider the graph spanned by the least set of nodes e-(A) satisfying the
closure conditions e-:
A is in e-(A)
If B atomic, then B is in e-(A) iff B^perp is in e-(A)
If (B tensor C) is in e-(A) then both B and C are in e-(A)
If (B par C) is in e-(A) then both B and C are in e-(A)
If B and C are in e-(A), B not= A, C not= A, then B tensor C is in e-(A)
conjecture: e-(A) is the least nontrivial proof net having
A has an exit, and it corresponds to R3.
It would seem that this yields a polynomial-time algorithm to compute
e-(A).
-- Jean H. Gallier & Philippe de Groote
By the way, it seems that the structure of the subproof nets
ordered by graph inclusion is interesting. It may be worth to
investigate it.
------------------
Subject: Re: about sequentialisation of multiplicative proof-nets
Date: Tue, 12 Nov 91 17:12:06 EST
From: chirimar@saul.cis.upenn.edu
Yes.
I was confused by the terminology and was actually thinking in
terms of the intersection of all graphs obtained by choosing
switchings of the original proof-net, which is what I had used.
-jawahar
-------------
Subject: Re: Kingdoms, empires, etc
Date: Wed, 13 Nov 91 00:11:50 +0100
From: Jean-Yves Girard <girard@margaux.inria.fr>
answer to Jean H. GALLIER and to PdG
polytime clearly, but linear time less obvious ; in fact empires are
linear time but also with a nice algo, which selects switches so
as to minimise the component. It would be nice to get such a natural
algo for kA.
Your definition of e-(A) is obviously wrong : it doesn't even define
a pf-net : one should easily construct a countexample involving
a formula A times (B par C) with A B and C all in e-(D), but no way
to get B par C in eA.
In general i think that one should also study these questions in the
qfr case.
jeanyves GIRARD