[Prev][Next][Index][Thread]
Preliminary Announcement
SLICING THE ADDITIVE BOXES
Preliminary Announcement
Gianluigi Bellin and Janice Hudgings
(Oxford University)
Abstract: In Multiplicative and additive linear logic (without
constant) the problem of deciding whether an arbitrary family of
slices is the slicing of a sequent derivation, is polynomial in the
size of the the data.
---------------------------------------------------------------------------
Comments: Slices for MALL- (MALL without weakening for \bottom) are
defined like multiplicative proof-structures, but with `plus' links
and *one-premise* `with' links.
Part (i)
Given a sequent derivation D in MALL- (or the corresponding proof-net
with additive boxes) we can associate a set Sl(D) of additive slices;
such a representation of MALL- proofs satisfies the Church-Rosser
property. E.g.,
|- A,-A |- A,-A |- A,-A |- A,-A
& ---------------- & ----------------
|- A&A, -A |- A, -A&-A
cut -------------------------------
|- A&A, -A&-A
is sliced into four copies of
------ -------
A -A A -A
--- -------- -----
A&A cut -A&-A
The cardinality of the set of slices is determined by the following rule.
If | Sl(D1) | = n and | Sl(D2) | = m, then
* if D comes from D1, D2 by a with-rule, then | Sl(D) | = n+m
* if D comes from D1, D2 by a times-rule, then | Sl(D) | = n.m
Part (ii)
Consider the inverse problem, given an arbitrary family of slices
{Q1,...,Qn} to decide whether there is a sequent derivation D such
that
{Q1,...,Qn} = Sl(D).
Clearly, all the Qi must satisfy the conditions for multiplicative
proof-nets; by a result of Danos, this is quadratic in the size of
Q1,...,Qn.
In addition, we would like to have a non-trivial condition which
guarantees that the we could transform {Q1,...,Qn} into a proof-net
with boxes. We show that the problem of deciding whether or not a set
of multiplicatively correct slices {Q1,...,Qn} can be sequentialized
is quadratic in the size of {Q1,...,Qn}.
We modify the decision procedure for sequent derivations in MALL- by
Galmiche and Perrier: starting with the conclusions Gamma, the same in
all slices, we construct a sequent derivation upwards by breaking
links in the following order: (1) par, (2) with, (3) plus, (4) times.
Step (4) involves finding a splitting times in each slice; this is
done by testing the empires of the premises of times link. Testing
each empire is linear in the size of the slice, therefore the process
of finding a sequent derivation, if it exists, is at worst quadratic
in the size of {Q1,...,Qn}.
In the process we obtain a *classification* of the slices; we increase
the number of classes whenever
* a formula is conclusion of an axiom link in some slices, not in others
A B
* at step (2), in different slices we break links --- , ---, with A not= B;
A&B A&B
A B
* at step (3), in different slices we break links --- , ---, with A not= B;
A+B A+B
* at step (4), in different slices the splitting times are different
formulas.
Finally, we need check whether the *classification* can be refined to
an appropriate *partition* of the slices (notice that in the case of a
&-link with conclusion A&A, as in our example, when we proceed upwards
we do not have enough information to refine our classification).
Starting from the axioms, we proceed *downwards* as described in part
(i) to check that ``there is the right number of slices of the
appropriate form''. Since this involves only testing the data once
more, the process remains quadratic, as claimed.
(Final remarks)
The representation of proofs in MALL- by slicing
* is the only representation (we know) having the Church-Rosser
property;
* has a natural interpretation in abstract languages for parallelism,
e.g., in R.Milner's pi-calculus;
* has a feasible correctness condition, i.e., polynomial time
sequentializability.
It is of course true that sequentializability is not an *interesting*
correctness condition. The result, however, is itself interesting,
since by a result of Lincoln and Winkler, sequentializability for MALL
(MALL- with the \bottom rule) is NP-complete.
References:
J-Y.Girard, Linear Logic, 1987, Section 6.
Galmiche and Perrier, Automated Deduction in Additive and Multiplicative
Linear Logic, in International Symposium on Logical
Foundations of Computer Science: Logic at TVER,
Tver Region, Russia 1992 (galmiche@loria.crin.fr)
P.Lincoln and T.Winkler, Constant-only Multiplicative Linear Logic
is NP-Complete, Preprint.
(Thanks L.Egidi for conversations on complexity.)