Light linear logic (Q1271560): Difference between revisions

From MaRDI portal
Added link to MaRDI item.
Import240304020342 (talk | contribs)
Set profile property.
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank

Revision as of 02:46, 5 March 2024

scientific article
Language Label Description Also known as
English
Light linear logic
scientific article

    Statements

    Light linear logic (English)
    0 references
    0 references
    3 May 1999
    0 references
    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.
    0 references
    Light Linear Logic
    0 references
    Elementary Linear Logic
    0 references
    exponentials of Linear Logic
    0 references
    proof-nets
    0 references
    complexity of cut-elimination
    0 references
    expressive power of a logical system
    0 references
    polytime functions
    0 references
    functions representable in a logical system
    0 references
    naive set theory
    0 references
    logical approach to complexity
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references