Comment by fnord77

2 months ago

What is this about? A pointer to a tutorial or a wiki link would be nice for someone who has no idea what this is. Thank you

I don't know much about any of this, and I'm far from an expert on the lambda calculus. But I skimmed paper by OP, which is informative: https://arxiv.org/abs/2505.20314

The lambda calculus is an alternate model of computation created by Alonzo Church in the 1930s. It's basically a restricted programming language where the only things you can do are define anonymous functions, and apply those anonymous functions to input variables or the output of other functions.

The Lambda calculus statement And = λp.λq.p q p is more conventionally notated as And(p, q) = p(q(p)).

You can reduce lambda expressions -- basically, this is "Simplifying this program as far as possible" what you expect a good optimizing compiler to do.

When there are multiple possible simplifications, which one should you pick? This is a complicated problem people basically solved years ago, but the solutions are also complicated and have a lot of moving parts. OP came up with a graph-based system called ∆-Nets that is less complicated and more clearly explained than the older solutions. ∆-Nets is a lot easier for people to understand and implement, so it might have practical applications making better performance and tooling for lambda-calculus-based programming languages. Which might in turn have practical benefits for areas where those languages are used (e.g. compilers).

The linked simulation lets you write a lambda calculus program, see what it looks like as a ∆-Net graph, and click to simplify the graph.

It's only tangentially related to OP, but YouTube channel 2swap recently had an interesting video about lambda calculus that you don't have to be an expert to enjoy: https://www.youtube.com/watch?v=RcVA8Nj6HEo

Cosign, 10 hours in and comments are exclusively people who seemingly know each other already riffing on top of something that's not clear to an audience outside the community, or replying to a coarser version of request with ~0 information. (some tells: referring to other people by first name; having a 1:1 discussion about the meaning of a fork by some other person)