I am looking for implementation of optimal reduction for λ-calculus based on interaction nets (McCarthy's amb allowed) in the spirit of "Token-Passing Nets: Call-by-Need for Free" by François-Régis Sinot. Implementations of optimal reduction that I am aware of either assume a specific strategy for the interaction net reduction, or involve non-pure graph reductions rather than just interaction rules.

The reason why I am interested in such implementation is that I already have a compiler for interaction nets which is based on interaction calculus, but is agnostic to any notion of interface, thus unable to follow any strategy while reducing a configuration simply represented as a queue of active pairs.

  • $\begingroup$ Eventually, I would like to replace the current evaluation strategy in my Web-based implementation codedot.github.io/lambda of the solution by François-Régis Sinot with optimal reduction. However, I could not find a suitable version of Lamping's algorithm yet. $\endgroup$ – Anton Salikhmetov Sep 22 '15 at 14:59
  • $\begingroup$ I managed to derive a token-passing net implementation of optimal reduction codedot.dreamwidth.org/174955.html by introducing a waiting construct. However it results in too much overhead and significantly worse overall performance than call-by-need implementation by Sinot. $\endgroup$ – Anton Salikhmetov Oct 20 '15 at 9:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.