Extending EAL with recursion makes it incompatible with the abstract algorithm?

Question

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?

Answer 1

The term that you gave does have one duplication, i.e.: ones is used in the body and returned in form of a free variable. The following example illustrates the same effect but is smaller:

loop = λ_. loop

To make the graph structure clear, let's make sure that each identifier is used exactly twice (_ represents connected erasing node):

C[loop, loop_rec] = λ[_, loop_rec]

EAL gives you termination proof if you can stratify all the terms. I don't see how you can stratify this one. If the level of loop_rec is $n$ then the level of whole λ is also $n$. And after the contraction the level of both loop and loop_rec should be $n-1$ which gives you contradiction.

On the other hand you are right that this copy can't escape the definition (assuming 1 and cons are closed), so it is equal to an actual infinite list. Yet I don't see how to generalize this into an argument about arbitrary recursive let statements.