[Prev][Next][Index][Thread]
Kingdoms, empires, etc
Date: Thu, 14 Nov 91 02:47:43 GMT
To: linear@cs.stanford.edu
In relation to the message by jean@saul.cis.upenn.edu:
-----------------------------------------------------------------------------
In my thesis (Mechanizing Proof Theory: Resource-aware logics and
proof-transformations to extract implicit information, Stanford, June 1990)
and in a paper (Proof Nets for Multiplicative and Additive Linear Logic)
the inductive definition of empire e+ is studied in detail. In particular,
it is shown that e+ can be used to give following necessary and sufficient
conditions for sequentialization:
(1) for each tensor node (A tensor B), A not in e+(B) and B not in e+(A);
same for cut nodes;
(2) for each par node (A par B), A in e+(B) and B in e(A);
same for conclusions of the proof-structure.
-----------------------------------------------------------------------------
I also considered how to extend the notion e+(A) in the case of the additives
(system MALL). The case of `plus' is clear. In the case of a `with' box,
any auxiliary door C of the box, together with the corresponding conclusions
C' and C'' of the substructures inside the box, forms a contraction link.
It is interesting that the case of `with', as well as of such contractions,
is similar to that of `par'. Thus:
if Bi not= A, (B0 plus B1) is in e+(A) iff Bi is;
if B0 not= A not= B1, then (B0 with B1) is in e+(A) iff B0 and B1 are in e+(A);
if C' not= A not= C'', then C is in e+(A) iff C' and C'' are in e+(A).
Then we can remove the `with' boxes, by using restricted contraction links.
The contraction links are `flagged', by associating each of them to
exactly one `with' link; each premise C0 or C1 of a contraction link
is associated with one premise B0 or B1 of exactly one `with' link.
To obtain necessary and sufficient conditions for sequentialization
in MALL, we need to add only the following condition to (1) and (2):
(3) for every with node (B0 with B1), the side doors of e+(Bi) are exactly
the premises Ci of some contraction node, where Ci is associated with Bi.
The following is a set of conditions alternative to (3):
For each with node (B0 with B1) and every premise Ci of contraction
associated with Ci:
(3'a) Ci is in e+(Bi) and Bi is in e+(Ci);
(3'b) B0 is not in e+(B1) and B1 is not in e+(B0);
(3'c) for every with node (D0 with D1) different from (B0 with B1),
Dj in e+(Bi) implies Bi not in e+(Dj).
--------------------------------------------------------------------------
Finally, I have considered the notion of slicing of the additive boxes
(cfr. Girard [1987], pp. 93-97); we need to identify formula-occurrences
living in different slices, i.e., we work with equivalence classes [X].
I considered the notion of empire e[A] in a family of slices
(modulo identifications).
There may be several correct ways of making such identifications; it is
clear how to identify the lowermost occurrences of a family, but a choice
has to be made otherwise, corresponding here to the flaggings in the previous
representation. Fortunately the notion of a family of slices as such
is Church-Rosser, as explained in Girard [1987].
In this representation, only the condition corresponding to (3'a) is needed:
For each with node (B0 with B1) and every premise Ci of contraction
associated with Ci:
(3''a) [Ci] is in e+[Bi] and [Bi] is in e+[Ci].
-----------------------------------------------------------------------------
So far these results have been unnoticed, but recently R.Milner,
Phil Scott and others have shown interest in them.
I'll be happy to send copy of the paper, if anyone wants it.
The thesis contains also facts about Herbrand's theorem for linear logic
and an application to the unwinding of the infinite Ramsey Theorem
(which are also published in ``Logic and Computation'',
Contemporary Mathematics 106, AMS, 1990).
I can send the thesis, but the department here charges for it.
You can also obtain the thesis as a Stanford CS report.
Gianluigi Bellin,
LFCS, King's Buildings,
University of Edinburgh,
Edinburgh EH9 3JZ,
Scotland UK