Name
Abstract | ||
|---|---|---|
The purpose of this paper is to demonstrate how Lafont's interaction combinators, a system of three symbols and six interaction rules, can be used to encode linear logic. Specifically, we give a translation of the multiplicative, exponential, and additive fragments of linear logic together with a strategy for cut-elimination which can be faithfully simulated. Finally, we show briefly how this encoding can be used for evaluating λ-terms. In addition to offering a very simple, perhaps the simplest, system of rewriting for linear logic and the λ-calculus, the interaction net implementation that we present has been shown by experimental testing to offer a good level of sharing in terms of the number of cut-elimination steps (resp. β-reduction steps). In particular it performs better than all extant finite systems of interaction nets. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1006/inco.2002.3163 | Inf. Comput. |
Keywords | Field | DocType |
interaction nets,extant finite system,additive fragment,interaction net,linear logic,interaction rule,cut-elimination step,cut-elimination,reduction step,interaction combinators,λ-calculus,experimental testing,good level | Discrete mathematics,Lambda calculus,Interaction nets,Linear system,Multiplicative function,Combinatory logic,Rewriting,Linear logic,Mathematics,Encoding (memory) | Journal |
Volume | Issue | ISSN |
176 | 2 | Information and Computation |
Citations | PageRank | References |
13 | 0.69 | 12 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ian Mackie | 1 | 13 | 0.69 |
| Jorge Sousa Pinto | 2 | 160 | 23.19 |