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?

  • $\begingroup$ My advice to make progress here is to exercise tons of examples until you gain an intuition what will happen in each of them (or find the counter-example you asked for). Then try to formulate the intuition into a proof or if you'll find it challenging post the examples and your findings in a new question. That will demonstrate your due diligence, move the work that has to be done to you from the readers that you ask for help. Hopefully this will also prevent negative comments from some knowledgeable readers that otherwise might help you :) $\endgroup$ – Łukasz Lew Feb 21 '19 at 5:11
  • $\begingroup$ @ŁukaszLew Just to be sure, from your comment you mean that you & others felt I didn't put enough work on the question? If that's the case, thanks for letting me know, I can delete it as I definitely don't want to sound demanding. But note I've been exploring this language for years and believe that is the case. You're right I never tried to write an actual proof, though. This is because I'm really bad with handwritten proofs (to be honest I don't get them) and I don't have an implementation of it in Agda or similar. I think I can try doing that now though. What do you think? $\endgroup$ – MaiaVictor Feb 21 '19 at 12:27
  • 1
    $\begingroup$ Hey Victor, I can only present my own opinion, I don't know about others. If I were to start working on solving the problem you presented. I start looking at more examples of let-recursive definitions and how they translate to graphs and why do the copy operation never escapes. Then whether that still is the case in mutually recursive definitions. Then I'd start looking at graphs where to copy operator does escape and think why these are not examples of recursive let definitions. If I'm stuck I'd select most illustrative examples and show them asking for more guidance. $\endgroup$ – Łukasz Lew Feb 21 '19 at 19:13
  • 1
    $\begingroup$ Also I think asking incomplete question is better than not asking it at all ! You definitely shouldn't be deleting anything. I'm enjoying this interaction. All I wanted to say is how I think the question can be improved to match the standards of some of the other members of our community. $\endgroup$ – Łukasz Lew Feb 21 '19 at 19:16
  • 2
    $\begingroup$ @ŁukaszLew I see, I appreciate your inputs and I see where you're getting at. I can definitely improve this question's quality, but I'll need some time for that. I'm right now implementing both EAL calculus and the abstract algorithm in Agda (something I should definitely have done already!). $\endgroup$ – MaiaVictor Feb 21 '19 at 19:39

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.

  • $\begingroup$ I'm not familiar what persistent upwards and downwards mean. I ignored that part of your description. I'm my experiments nodes could go through 'wiring' that would change their apparent direction, so 'upward/downward' distinction wasn't really useful for me so far. Perhaps some photos of hand drawn graphs would be illuminating to explain your intuitions. $\endgroup$ – Łukasz Lew Feb 21 '19 at 19:19

Your Answer

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

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