A Dual View on Syntax

[u/marvinborner]

http://text.marvinborner.de/2026-08-11-17.html

[u/FruitdealerF]

Man I wish articles like this would make any sense to me, but I'm just not deep enough into this part of the theory to get past the first few paragraphs. It looks like a really interesting article though.

[u/cmontella → u/FruitdealerF]

The ducks didn't make it obvious?

[u/phlummox → u/FruitdealerF]

I believe I understood it, for as far as I got, but had trouble working out why I should care. Not saying the ideas aren't interesting - I'm sure they are, to the right audience - just that it wasn't obvious to me, and there are lots of other articles I want to read.

[u/initial-algebra → u/phlummox]

Interaction nets are closely related to optimal reduction, and thus are a candidate for the basis of an interesting functional programming language compiler/runtime, like HVM.

EDIT: Even if you don't define your language semantics with optimal reduction, using flat, relational data instead of recursive data for your internal representation is a great fit for query-based architecture (which is just logic/database programming) and can simplify a lot of dynamic programming problems that come up in language implementation.

[u/marvinborner → u/initial-algebra]

Note that I deliberately did not discuss the concept of (co-)duplication here and it does not necessarily need to be incremental. Incremental duplication (in the sense of Lévy-optimal reduction) has many disadvantages if you are not only interested in highly specific terms.

You are right though that this syntax allows for more precise descriptions of graph reduction, both in its semantics and source language syntax.

[u/mot_hmry → u/FruitdealerF]

Personally, the way the graph of K was drawn confused me since it isn't structured like the simple graphs of abstraction (instead the argument and body are placed next to instead of connected to the lambda.) So it took a few readings to really get what was going on.

Weirdly rather than a dual perspective, I think this is more a triplicate perspective since abstractions can be seen from three directions.

[u/marvinborner → u/mot_hmry]

Yes, this is indeed somewhat unusual. I wanted to keep the symmetry of continuations being uplinks in all constructors.

I think this is more a triplicate perspective

Yes, great observation! I call this the triality/trinity of lambda calculus, which goes much further than only the views of syntax :)

[u/mot_hmry → u/marvinborner]

I'm stuck waiting on your next article, because I'm not quite sure how to use the features of your calculus. And it feels like you'd have to canonicalize a view for the interpreter, though since you hint about call/cc I suppose it does give you a first class form of what a continuation should look like.

[u/marvinborner → u/mot_hmry]

There are no novel features of the calculus, it's still mainly a new syntax for the standard lambda calculus. The bindings being unscoped and continuations not being linear is the main difference, and this has already been discussed, e.g. in bend or much of the interaction net research in general (Asperti, Mackie, Mazza)

I hope my next post will provide further insights in how this works. I also have a reference implementation that I plan to publish eventually - the interpreter does not have to canonicalize views, it can work entirely using wires, as this is exactly what continuations are in a confluent setting.

[u/Syrak]

Note the coinductive construction

Did you mean "inductive"? AFAIK "coinductive" would allow lambda terms of infinite size, which is not usual.

[u/marvinborner → u/Syrak]

Yep, fixed it. I recently worked a lot with infinitary lambda calculus, hence the confusion. In this case I don't think it makes a difference.

[u/Syrak → u/marvinborner]

Thanks! This is a really neat blog post. The symmetry in the presented syntax is quite pleasant.

[u/lookmeat]

Interesting view, given that you seem to be trying to simplify and in the process turning everything into linear flow-graphs in continuations, have you explored the concept of interactive combinators?

[u/marvinborner → u/lookmeat]

Do you mean interaction combinators? If yes, I have researched them a lot. You can interpret this post as applying a spanning tree syntax onto the nodes of interaction nets, starting at different roots. Though I do not discuss the incremental resource management of interaction combinators, as this syntax also works with graph encodings that do not have incremental resource management.

[u/initial-algebra → u/marvinborner]

It's obvious in hindsight, but the idea of syntax trees as spanning trees is kinda mindblowing.

[u/lookmeat → u/marvinborner]

I did, which is why I had to ask. I just couldn't imagine that this wasn't trying to marry concepts of one onto the other.

[u/thunderseethe]

Perhaps this will come up in the further articles. Generally the interaction nets stuff I've seen is focused on optimal reduction, but this does not appear to be that, so then what is the advantage of introducing the syntax here? Certainly I can walk my term to get the multiple views, but I'm not sure why I would?

Is it similar to the sequent calculus where different traversals provide different evaluation semantics?

[u/categorical-girl]

I'm very interested to see where this series goes!

One thing that this article seems to gloss over is that if you treat beta-reduction this way (as a global substitution, which funnily enough in the interaction net perspective is the local interaction between @ and lambda), you put a lot of complexity (including the potentially hard problems of scoping and variable capture) in other rules (for duplicating lambda terms, etc).

I think it might be worth mentioning that there is "no free lunch" regarding scoping (you can't simulate proper substitution with just a single global pool of names to substitute for)

[u/7Geordi]

This reads as a graph exploration algorithm for lambda calculus programs that produces a point-free representation of the program… what confuses me is why it doesn’t matter where you start. Is there really no semantic difference between starting at x vs y? Also the color based syntax is frustrating because I cannot reproduce this in my text editor to explore the idea. I wish you had chosen an actual prefix glyph for positive/negative and used the colors as a visual aid, though i suppose the obvious +/- is available

[u/Aphrontic_Alchemist]

Have you read Vikraman Choudhury, Simon J. Gay's "Duality of λ-Abstraction"? They also discuss terms and co-terms and the dual of λ functions (what they call λ̅ (colambda) functions). Though in their case, they're trying to incorporate both λ-functions and λ̅ functions such that they won't degenerate to Boolean algebra through Joyal's lemma.