6 ms·

Lambda Calculus – Animated Beta Reduction of Lambda Diagrams

150 points by perryprog 10mo ago

__grob 10mo ago
This is sick, loved the 2swap video on this. Happy to see more content visualizing lambda calculus and Tromp lambda diagrams.
ggm 10mo ago
The number of reduction steps in division.
Vosporos 10mo ago
Cheers, I love it!
tromp 10mo ago
You can enter (λn.n(λc.λa.λb.cb(λf.λx.f(afx)))Fn0)7 to compute the function Col' from [1] to 7, resulting in (3*7+1)/2 = 11. Unfortunately, this visualization is much less insightful than showing the 7 successive succ&swap operations: 7 0 0 8 8 1 1 9 9 2 2 10 10 3 3 11 [1] https://news.ycombinator.com/item?id=46022965 https://news.ycombinator.com/item?id=46022965
discovermsps 10mo ago
[dead]
killerstorm 10mo ago
There's a model of computation called 'interaction nets' / 'interaction calculus', which reduces in a more physically-meaningful, local, topologically-smooth way. I.e. you can see from these animations that LC reductions have some "jumping" parts. And that does reflect LC nature, as a reduction 'updates' many places at once. IN basically fixes this problem. And this locality can enable parallelism. And there's an easy way to translate LC to IN, as far as I understand. I'm a noob, but I feel like INs are severely under-rated. I dunno if there's any good interaction net animations. I know only one person who's doing some serious R&D with interaction nets - that's Victor Taelin.
- hmokiguess 10mo ago
  Speaking of Victor Taelin, what's the latest on https://higherorderco.com/ https://higherorderco.com/ ? His work is really inspiring and amazing
  - killerstorm 10mo ago
    He shares the progress on Twitter quite often. In the last year they shifted the focus away from raw performance (as beating existing stuff is rather daunting) and into rather unique stuff with code synthesis, perhaps relevant to formal verification of vibe-coded code, etc.
- tromp 10mo ago
  > there's an easy way to translate LC to IN While easy, it sadly doesn't preserve semantics. Specifically, when you duplicate a term that ends up duplicating itself, results will diverge. There exist more involved semantics preserving translations, using so-called croissants and brackets, or with the recent rephrased approach of [1]. [1] https://arxiv.org/abs/2505.20314 https://arxiv.org/abs/2505.20314
  - marvinborner 10mo ago
    > While easy, it sadly doesn't preserve semantics. There is actually an easy way that does preserve semantics at least to WHNF - it's called closed reduction. Mackie has worked on it a bunch (see some resources [1]). An even simpler implementation is Sinot's token passing. The problem with both of these approaches is the decreased amount of sharing and potential for parallelism, which is typically the reason for using interaction nets in the first place. [1] https://github.com/marvinborner/interaction-net-resources?tab=readme-ov-file#non-optimality https://github.com/marvinborner/interaction-net-resources?ta...
dloss 10mo ago
Some more example programs in Lambda Calculus here, including a compliant brainf#*k interpreter: https://justine.lol/lambda/ https://justine.lol/lambda/

150 points by perryprog 10mo ago

__grob 10mo ago

This is sick, loved the 2swap video on this. Happy to see more content visualizing lambda calculus and Tromp lambda diagrams.

ggm 10mo ago

The number of reduction steps in division.

Vosporos 10mo ago

Cheers, I love it!

tromp 10mo ago

You can enter (λn.n(λc.λa.λb.cb(λf.λx.f(afx)))Fn0)7 to compute the function Col' from [1] to 7, resulting in (3*7+1)/2 = 11. Unfortunately, this visualization is much less insightful than showing the 7 successive succ&swap operations: 7 0 0 8 8 1 1 9 9 2 2 10 10 3 3 11 [1] https://news.ycombinator.com/item?id=46022965 https://news.ycombinator.com/item?id=46022965

discovermsps 10mo ago

[dead]

killerstorm 10mo ago

There's a model of computation called 'interaction nets' / 'interaction calculus', which reduces in a more physically-meaningful, local, topologically-smooth way. I.e. you can see from these animations that LC reductions have some "jumping" parts. And that does reflect LC nature, as a reduction 'updates' many places at once. IN basically fixes this problem. And this locality can enable parallelism. And there's an easy way to translate LC to IN, as far as I understand. I'm a noob, but I feel like INs are severely under-rated. I dunno if there's any good interaction net animations. I know only one person who's doing some serious R&D with interaction nets - that's Victor Taelin.

hmokiguess 10mo ago
Speaking of Victor Taelin, what's the latest on https://higherorderco.com/ https://higherorderco.com/ ? His work is really inspiring and amazing
- killerstorm 10mo ago
  He shares the progress on Twitter quite often. In the last year they shifted the focus away from raw performance (as beating existing stuff is rather daunting) and into rather unique stuff with code synthesis, perhaps relevant to formal verification of vibe-coded code, etc.
tromp 10mo ago
> there's an easy way to translate LC to IN While easy, it sadly doesn't preserve semantics. Specifically, when you duplicate a term that ends up duplicating itself, results will diverge. There exist more involved semantics preserving translations, using so-called croissants and brackets, or with the recent rephrased approach of [1]. [1] https://arxiv.org/abs/2505.20314 https://arxiv.org/abs/2505.20314
- marvinborner 10mo ago
  > While easy, it sadly doesn't preserve semantics. There is actually an easy way that does preserve semantics at least to WHNF - it's called closed reduction. Mackie has worked on it a bunch (see some resources [1]). An even simpler implementation is Sinot's token passing. The problem with both of these approaches is the decreased amount of sharing and potential for parallelism, which is typically the reason for using interaction nets in the first place. [1] https://github.com/marvinborner/interaction-net-resources?tab=readme-ov-file#non-optimality https://github.com/marvinborner/interaction-net-resources?ta...

dloss 10mo ago

Some more example programs in Lambda Calculus here, including a compliant brainf#*k interpreter: https://justine.lol/lambda/ https://justine.lol/lambda/