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?


1 Answer 1


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. 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.