<p>I am not aware of any implementation of Lamping's algorithm directly in the interaction combinators.  I do know that the presence of integer labels is a necessary feature of Lamping's algorithm, even for EAL-typable terms, because the labels reflect the nesting of so-called <em>exponential boxes</em> in proof nets, and Lamping's algorithm is essentially the execution of proof nets using the geometry of interaction, as first observed by <a href="http://dl.acm.org/citation.cfm?id=143172">Gonthier, Abadi and Lévy</a>.  So the question of implementing the algorithm in the interaction combinators boils down to representing exponential boxes in proof nets using the combinators. This is essentially what Mackie and Pinto did in their paper.</p>

<p>Of course, Mackie and Pinto's encoding adresses all $\lambda$-terms, which use full linear logic boxes, whereas EAL-typable terms use elementary linear logic boxes, which are simpler (they are so-called <em>functorial boxes</em>).  However, I do not believe that this simplification would have a notable impact on interaction combinator implementations.  This is because boxes are a global feature (they identify arbitrarily big subnets to be duplicated/erased), whereas the interaction combinators (as any interaction net system) are completely local (reduction only modifies bounded subnets), so the challenge is to represent such global features locally.  Now, global duplication/erasing in EAL is identical as in full linear logic, that is why I do not expect that an interaction combinator implementation of EAL would radically differ from the one proposed by Mackie and Pinto.</p>

CC BY-SA 3.0
2015-08-14T14:15:29.583Z
2015-08-14T14:15:29.583Z
Damiano Mazza
<p>Interaction combinators <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.9699">have been proposed</a> as a compile target for the λ-calculus before. That paper implements the full λ-calculus. It is also known that it is possible to <a href="http://dl.acm.org/citation.cfm?id=1131315">optimize interaction-net encodings of the λ-calculus</a> for the subset of λ-terms that is EAL-typeable. That paper implements that subset of the λ-calculus by translating EAL-typeable λ-terms to interaction nets that are arguably more complex than interaction combinators, since they use an infinite alphabet of labels to group duplicators. </p>

<p>I wonder if it is possible to combine both proposals. That is, is there any encoding for the abstract algorithm - that is, λ-terms that are EAL-typeable - as interaction combinators?</p>

<lambda-calculus><functional-programming><interaction-nets>
How do you encode Lamping's abstract algorithm using interaction combinators?
MaiaVictor
# How do you encode Lamping's abstract algorithm using interaction combinators?

(Asked by: username_0 on 2015-08-05)

Interaction combinators [have been proposed](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.9699) as a compile target for the λ-calculus before. That paper implements the full λ-calculus. It is also known that it is possible to [optimize interaction-net encodings of the λ-calculus](http://dl.acm.org/citation.cfm?id=1131315) for the subset of λ-terms that is EAL-typeable. That paper implements that subset of the λ-calculus by translating EAL-typeable λ-terms to interaction nets that are arguably more complex than interaction combinators, since they use an infinite alphabet of labels to group duplicators.

I wonder if it is possible to combine both proposals. That is, is there any encoding for the abstract algorithm - that is, λ-terms that are EAL-typeable - as interaction combinators?

**Tags:** lambda-calculus, functional-programming, interaction-nets

---

## 1 answers

### Answer by username_1 on 2015-08-14. Score: 7 | Accepted answer

I am not aware of any implementation of Lamping's algorithm directly in the interaction combinators. I do know that the presence of integer labels is a necessary feature of Lamping's algorithm, even for EAL-typable terms, because the labels reflect the nesting of so-called *exponential boxes* in proof nets, and Lamping's algorithm is essentially the execution of proof nets using the geometry of interaction, as first observed by [Gonthier, Abadi and Lévy](http://dl.acm.org/citation.cfm?id=143172). So the question of implementing the algorithm in the interaction combinators boils down to representing exponential boxes in proof nets using the combinators. This is essentially what Mackie and Pinto did in their paper.

Of course, Mackie and Pinto's encoding adresses all $\lambda$-terms, which use full linear logic boxes, whereas EAL-typable terms use elementary linear logic boxes, which are simpler (they are so-called *functorial boxes*). However, I do not believe that this simplification would have a notable impact on interaction combinator implementations. This is because boxes are a global feature (they identify arbitrarily big subnets to be duplicated/erased), whereas the interaction combinators (as any interaction net system) are completely local (reduction only modifies bounded subnets), so the challenge is to represent such global features locally. Now, global duplication/erasing in EAL is identical as in full linear logic, that is why I do not expect that an interaction combinator implementation of EAL would radically differ from the one proposed by Mackie and Pinto.


---

