My current plan is to programming with interaction nets directly, and to view Lamping's "optimal lambda calculus reduction" as an example.
I have not read Lamping's paper yet. But if it uses "Interaction Combinators", maybe I can not even do it in my implementation.
Because there are two version of inet:
(1) Lafont's 1990 paper "Interaction Nets"
(2) Lafont's 1997 paper "Interaction Combinators"
I implemented (1) where a port has a sign (input port v.s. output port). Given two ports, I can only connect them when they have opposite signs.
In (2) there is no input port v.s. output port, ports are not signed (Lafont called the signed version "directed" in (2)).
"Interaction Combinators" uses self interaction (rule about a node interacting with itself), it is not possible in signed version of inet.
Because one node only has one principle port, thus can not connect to it's own principle port, because the same principle port has the same sign, not opposite signs.
------
I said "programming with interaction nets directly", because it seems already a more practical language than lambda calculus, for we do not need lambda encoding to express datatype and pattern matching, we can define rules case by case directly.