A few years ago, I've asked if Elementary Affine Logic can be used as the core type system of a practical programming language. The accepted answer argues that, yes, although such language would be awkward to use because you can not iterate over terms that were themselves produced as the result of an iteration. EAL calculus is compatible with Lamping's abstract algorithm because, due to its stratification condition, substitution doesn't alter the level of the substituted term. As such, by using the label approach to mark fan nodes with their levels, and only duplicating terms of higher levels, we'll never have an unsound reduction. If we, though, add recursion in the form of recursive let-bindings, then this argument shouldn't be affected at all. Take the infinite list of ones, for example:
ones = λcons. λnil. (cons 1 ones)
This term doesn't duplicate λ-bound variables and, as such, doesn't require boxes at all. It can be seen as no different than writing a very huge list at the level 0. From the interaction net perspective, its only fan-node is pointing downwards, i.e., it is not pointing upwards towards the variable slot of a λ-node, so it obviously can't interact with a fan-node with the same label coming from a different duplication process. Am I wrong in concluding that, thus, extending the EAL calculus with mutually recursive
let shouldn't make it incompatible with the label approach of optimal reduction?