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 eas…
Speaking of Victor Taelin, what's the latest on https://higherorderco.com/ ? His work is really inspiring and amazing
Lambda Calculus – Animated Beta Reduction of Lambda Diagrams
11–12 of 12 posts
Re: Lambda Calculus – Animated Beta Reduction of Lambda Diagrams
#12There'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 eas…
> 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
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?ta...