# How do you encode Lamping's abstract algorithm using interaction combinators?

Interaction combinators have been proposed 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 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?

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.