DocumentCode :
1956494
Title :
Linear logic with boxes
Author :
Mackie, Ian
Author_Institution :
Ecole Polytech., Palaiseau, France
fYear :
1998
fDate :
21-24 Jun 1998
Firstpage :
309
Lastpage :
320
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 1998. Proceedings. Thirteenth Annual IEEE Symposium on
Conference_Location :
Indianapolis, IN
ISSN :
1043-6871
Print_ISBN :
0-8186-8506-9
Type :
conf
DOI :
10.1109/LICS.1998.705667
Filename :
705667
Link To Document :
بازگشت