Title :
Linear logic with boxes
Author_Institution :
Ecole Polytech., Palaiseau, France
Abstract :
Interaction nets provide a graphical paradigm of computation based on net rewriting. By encoding the cut-elimination process of linear logic they have proved successful in understanding the dynamics of reduction in the λ-calculus. G. Gonthier et al. (1992) gave an optimal infinite system of interaction nets for linear logic by removing the global boxes. However efficient implementations of optimal reduction have had to break away from the interaction net paradigm. Here we give an efficient new finite interaction net encoding of linear logic which is not optimal, but overcomes many of the inefficiencies caused by the bookkeeping operations in the implementations of optimal reduction. We code the global operations on boxes (contraction, weakening, dereliction, commutative cut) in a local way, keeping the box structure, which results in a system allowing a great deal of sharing with an extremely low overhead. We believe that this implementation is the most faithful of all the extant interaction net encodings of linear logic
Keywords :
formal logic; lambda calculus; rewriting systems; bookkeeping operations; boxes; cut-elimination process; finite interaction net encoding; interaction nets; lambda calculus; linear logic; net rewriting; optimal infinite system; Application software; Computational efficiency; Computer science; Ear; Encoding; Geometry; Lamps; Logic; Read only memory;
Conference_Titel :
Logic in Computer Science, 1998. Proceedings. Thirteenth Annual IEEE Symposium on
Conference_Location :
Indianapolis, IN
Print_ISBN :
0-8186-8506-9
DOI :
10.1109/LICS.1998.705667