Light linear logic (Q1271560): Difference between revisions

This paper draws the main ``boulevards'' of a logical approach to complexity, based on the idea that the expressive power of a logical system is the complexity of its cut-elimination procedure. A very careful handling of Linear Logic (LL) exponentials leads the author to define a weak LL (the ``Light Linear Logic'' LLL), for which he proves the following outstanding result: A function \(f\) is representable in LLL if and only if \(f\) is polytime. The search for a cut-elimination procedure with ``light'' complexity leads the author to look for a system \(S\) (a variant of the system \(PN_2\) of LL proof-nets) for which the cut-elimination bounds do not depend on the cut-formulas. The methodological intuition of the author is that naive set theory will be consistent with such a system \(S\): this is because adding naive set theory to \(S\) will not prevent the cut-elimination procedure from terminating. It is then by expressing in LL the paradoxes of naive set theory that the author realizes that the depth of a proof-net of \(S\) (i.e. the maximum nesting number of boxes in this proof-net) should not change during cut-elimination. This is one of the main ingredients leading to the ``light'' exponentials of LLL. The technical part of the paper (the proof of the main theorem) relies on much of the work done by the author in the last years (including an improvement of the syntax of the additives). It is highly technical and not easy to understand. More recent works of Asperti, Danos, Joinet, Kanovitch, Lafont and others indicate that several simplifications are possible: LLL seems to be \textit{one} among the possible solutions, and rather a research theme than a logical system. This work seems to be a true breakthrough, and several questions and problems arise from it. Among them, one can mention the possibility of formulating arithmetic in LLL (which would then be a ``feasible'' arithmetic), and the search of a denotational semantics suitable for LLL. Such a semantics should give a criterion to choose among the several variants of LLL, and \dots{} last (but definitely not least!) it might yield new and deep insights into complexity problems.