[Prev][Next][Index][Thread]
paper announcement
Announcement of a paper:
Proof Nets ans Typed Lambda Calculus
I. Empires and Kingdoms
by
G.Bellin and J.van de Wiele
(Oxford University - Universite' de Paris VII)
Abstract:
This paper is the first part of a study of Proof Nets and of Natural
Deduction derivations as graphs with different forms of orientations.
Results reached so far include a representation of linear lambda terms
as oriented Chinese Characters Diagrams, arising in the study of
Vassiliev invariants in knot theory; a translation preserving
normalization of natural deduction for linear logic into oriented
proof-nets; conditions for orientability of proof-nets yielding
the inverse translation. In the present paper, extending previous
unpublished results by Girard, Danos, Gonthier, Joinet, Regnier,
we provide a system of first order proof-nets without boxes for
the full system of linear logic and we investigate the structure
of the subnets of a proof-net.
-------
The paper ``Proof Nets ans Typed Lambda Calculus I. Empires and Kingdoms''
is available by anonymous ftp from
theory.doc.ic.ac.uk
in the directory
/papers/Bellin
in the files
king.dvi.Z king.ps
use uncompress king.dvi.Z to obtain the dvi-file king.dvi.
-------
Comments: The reader can use this (rather long) paper in several ways.
1. in the preface we discuss the motivations for the project and give
an outline of some results;
2. in the section on multiplicative proof nets we develop the theory of
the subnets of a multiplicative proof net, based on Danos and Regnier's
correctness condition;
3. in the Appendix II we give equivalent correctness conditions for the
multiplicative fragment;
4. in the sections on the additives and the exponentials we generalize
Danos and Regnier's method to the whole system of linear logic;
we also discuss these results as a contribution to the ``elimination
of boxes'';
5. we consider the computational complexity of some constructions;
6. in the section on the problem of irrelevance (Weakening boxes)
we recall and discuss systems of Direct Logic, namely, Linear Logic
with the rule of Mix (Mingle).
We made a special effort to give proper credit for the results;
unfortunately, omission of relevant results and/or credits is always
possible and will be corrected; please let us know.