[Prev][Next][Index][Thread]

paper announcement for linear mailing list


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]


The following paper is available by anonymous ftp boole.logique.jussieu.fr    

SUBNETS OF PROOF-NETS IN MULTIPLICATIVE LINEAR LOGIC WITH MIX

                      by GIANLUIGI BELLIN
             (Equipe de Logique -- Universite' de Paris 7) 

ABSTRACT: The paper studies the properties of the subnets of a proof-net for
first order Multiplicative Linear Logic without propositional constants (MLL-),
extended with the rule of Mix:

                      |- Gamma      |- Delta
                      -----------------------
                          |- Gamma, Delta

Asperti's correctness criterion and its interpretation in terms of concurrent
processes are extended to the first order case.
The notion of *kingdom* and *empire* of a formula are extended from MLL- to
MLL- + MIX. A new proof of the sequentialization theorem is given.
As a corollary, a system of proof-nets is given for De Paiva and Hyland's
Full Intuitionistic Linear Logic with Mix; this result gives a general method
to translate Abramsky-style term assignments into proof-nets, and viceversa.

To appear in Mathematical Structures in Computer Science. 

                              ---- * ----

TO OBTAIN THE PAPER: 
ftp boole.logique.jussieu.fr    
login anonymous

cd pub/distrib/bellin
get mix.dvi.gz        or      mix.ps.gz 

                              ---- * ----

COMMENTS: This papers concludes a project of research on MLL + MIX conducted
in different occasions and in the interaction with several researchers,
especially those acknowledged below.  At the same time, it gives the
background for such new directions of research as non-commutative proof-nets
and Arnaud Fleury's work on the Exchange Rule: the paper by G.Bellin and
A.Fleury ``Braided Proof-nets for multiplicative Linear Logic with MIX'' is
also available by anonymous ftp from the same site, same directory. 
(get ncmix.dvi.gz        or       ncmix.ps.gz) 

The introduction discusses at length the significance of the MIX
rule and its uses in proof-theory, concurrency theory and category theory.
A more general theory (such as that of proof-nets for MLL + MIX) helps to 
understand the specific properties of the standard theory for MLL. 
Moreover, the results given or summarized in this papers show that MLL + MIX
formalizes certain specific features of *classical* systems, in a better way 
than the system without MIX. In particular, MLL + MIX seems ``the right
theory'' from the point of view of *concurrent* logical computations. 

ACKNOWLEDGEMENTS: 
The technique used in the sequentialization theorem goes back to the author's
thesis (1990), which was motivated in an essential way by Jussi Ketonen's
direct logic.

The study of kingdoms and empires is a natural continuation of the work on
MLL- conducted with Jacques van de Wiele, Paris VII. 

The work by Andrea Asperti has given convincing evidence of the significance
and independent value of MLL with MIX, especially form the point of view of
*concurrent* logical computation.

Proof-nets for FILL with Mix were motivated by the work by the Cambridge team
to find the appropriate syntactic formulation of the term calculus for it.
The system FILL has raised some interesting questions on the relations between 
classical and intuitionistic systems of linear logic. 

                              ---- * ----

The paper is dedicated to Silvia Baraldini, an Italian citizen sentenced in
the USA to long term imprisonment in a politically sensitive trial. The
Italian government and public opinion have been trying to obtain her
repatriation for several years.