[Prev][Next][Index][Thread]
paper availbale by ftp
PROOF-NETS : THE PARALLEL SYNTAX FOR PROOF-THEORY
One year ago I announced essential progresses on additives, both on
proof-nets and on geometry of interaction. The paper on GOI was
quickly written, but the paper on proof-nets was postponed, since I
found a bug when I wrote the details. Recently I discovered the two
systems with constant cut-elimination complexity, ELL and LLL. I
tried to make a proof with old fashioned methods, i.e. sequent
calculus. This was extremely painful (difficult to avoid the nonsense
of double layer sequents, difficult to provide a natural size for
proofs etc.) In fact -assuming that I had the patience to cope with
these minor technicalities, the reader would have got a symmetric
problem, i.e. to find out what is the central idea in this
bureaucratic mess. The use of sequents here was nothing but a
childish game of encryption/decryption.
This is why I decided to do it with proof-nets. The problem is that
additives play an important role in LLL (not that much in ELL), and
that I was never satisfied with the extant notion of proof-net. But
it turns out that the extant notion (equipped with a lazy
cut-elimination) normalizes in linear time, and that's enough for
what I wanted to do. This is the reason why I decided to write a
survey paper concerning proof-nets. Its aim is to provide an
alternative syntax, in case one wants to do elegant proof-theory or
achieve subtle aims, or simply protect forests...
The paper mainly deals with additive proof-nets, for which the best
known solution is presented, and their lazy normalization. The
discussion about possible improvements and the description of the
full procedure are postponed to an appendix. The paper proceeds with
the unproblematic extension to quantifiers (which look like
oversimplified additives), and the treatment of exponentials, for
which we restrict to weakening and contraction : the other rules,
e.g. the rules for LLL or ELL, will be considered in a forthcoming
paper. The weakening rule is also slightly problematic, but this is a
rather minor question.
The paper is available by anonymous ftp
lmd.univ-mrs.fr
directory : \pub\girard
files : proofnets.ps.Z and proofnets.dvi.Z
Happy Christmas and New Year
---
Jean-Yves GIRARD
Directeur de Recherche
CNRS, Laboratoire de Mathematiques Discretes
163 Avenue de Luminy, case 930
13288 Marseille cedex 9
<girard@lmd.univ-mrs.fr>
(33) 91 82 70 25
(33) 91 82 70 26 (Mme Bodin, secretariat)
(33) 91 82 70 15 (Fax)