Is your use of colors for different duplication nodes ok?

[phischu]

Dear Victor,

In "An Algorithm for Optimal Lambda Calculus Reduction" on page 5 Lamping writes "An obvious idea is to label the fans in the graph, with fans paired if and only if they have identical labels." He then goes on to explain problems with this "obvious approach" which I don't understand.

As far as I understand this "obvious approach" is what you are doing. What could go wrong? Inefficiency? Correctness? Do you limit the class of nets or terms your algorithm can handle? How?

Others argue that using an infinite family of nodes is cheating but I don't care about that.

How do you assign colors to nodes? Does every duplication node you generate get a fresh color? Can we do better?

Thank you, keep up the good work!

[VictorTaelin]

Yes, for each duplication node I generate a fresh color. So, I'm not really using interaction combinators, but an extension of the idea with an infinite set of different nodes (0 = con, 1 = dup, 2 = dup_b, 3 = dup_c...), but the same rules.

There are problems with this obvious approach. Not efficiency, but correctness - there are many terms for which this approach simply won't work, i.e., reading back from the reduced net won't give you the normal form of the original term. "Fixing" that problem involves extending the system with oracles, which is a separated machinery which keeps track of levels in a more sophisticated way than labels. There are many papers trying to come up with better oracles, but my observation is that those oracles always come up with a harsh performance penalty. Moreover, we only have satisfactory efficiency proofs for that obvious approach.

Since this was a quest for elegance, I've just assumed terms which can't be reduced with the simpler approach are defective, and started exploring the class of λ-terms that can, to see if it is "good enough" for "normal programming". I've used Caramel and Optlam for that, and learned that:

1. Yes, there are many specific programs (say, quicksort) that you would write "normally" that fail to reduce.
2. Yet, for any problem you're trying to solve (sorting itself), once you think enough, it seems to always be the case that there is also a very elegant term that works.

It also has been proven that any EAL-typeable term can be reduced this way, so it includes all elementary functions, which certainly includes everything I define as "normal programming". Also, this is all w.r.t compiling the λ-calculus to interaction combinators; interaction combinators are still a perfect compilation target for interaction-nets based languages, which are also very interesting and deserve more exploration.

---

Finally, on the elegance of colors themselves. The colors separate "layers" of duplications; for example, if you have 2 colors, interaction combinators are equivalent to 2-stack machines; this is true for any N. Often, if you're clever, you can find ways to use much less colors than one per dup. For example, if you reduce the exponentiation of church-numbers, you'll come up with "compact" nets with many dups having the same color in a very symmetric way. I might eventually make an infographic showing the most compact representation of all natural numbers. I suspect there are many incredibly beautiful programs that make use of this phenomena, but finding them is quite hard while I don't gain a higher understanding of those things. Finally, it is easy and direct to emulate those colors on interaction combinators themselves (say, if you didn't implement them and have only the original system restricted to 2 different nodes).

[phischu]

Thank you for this clear and comprehensible answer. Now I need to understand what EAL-typeable means. Your last sentence

Finally, it is easy and direct to emulate those colors on interaction combinators themselves (say, if you didn't implement them and have only the original system restricted to 2 different nodes).

I don't understand. If this is "easy" why don't you (and others) do it? How does it work?

I am asking because (as I told you on reddit) I see an obvious connection to linear sequent calculus with explicit contraction and weakening. But this obvious connection is not so obvious if you have multiple different sharing nodes.

Are all morte programs (calculus of constructions) EAL typeable?

[VictorTaelin]

Are all morte programs (calculus of constructions) EAL typeable?

No... I really wish that was the case since I'm looking for a dependently typed core language which can be reduced with interaction combinators. On the other hands, Morte is somewhat annoying for the lack of fix-points, so it can't express the Scott Encoding, which obviously is essential for a ton of functional algorithms. Since the termination argument of EAL relies on how much you can replicate stuff, you can actually have fix-points without losing strong normalization. I'm really noob on those things, though, but I guess if we could extend this (from the "On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy") we'd have a Morte-like language with Scott encodings and great computational properties.

I don't understand. If this is "easy" why don't you (and others) do it? How does it work?

On the original interaction combinators paper, there is an explanation on how to emulate any interaction net system using combinators. A simple approach would be to use his compilation algorithm to compile a interaction net system with N duplication nodes to combinators. This comes with a constant-time slowdown at most. I suspect there is a more efficient way to do this, but I need to investigate. And the reason I didn't do this is that it was much easier to just use an int label on each node, and I was still unsure philosophically if infinite nodes are really less elegant than just two.

But this obvious connection is not so obvious if you have multiple different sharing nodes.

So interaction combinators aren't actually proof nets for the multiplicative fragment of the sequent calculus?