Lambda Calculus in 383 Bytes (2022)
23 comments
·January 13, 2025exikyut
kccqzy
The best way to wrap your mind around the core concept and internalize them into a mental model is writing an interpreter yourself. It's been abundantly clear to me since young that for anything involving math, you don't internalize it if you merely passively let someone else explain it, whether that's reading a textbook/blog or attending a professor's lecture or watching a YouTube video. You have to do the exercises.
Lambda calculus is the same. You can easily define the data structure to represent a program in untyped lambda calculus and then write an interpreter for it. Then go implement some interesting concepts such as the Y combinator or the Omega combinator. If you find lambda calculus too difficult to do things like arithmetic or linked lists, you don't have to stick with Church numerals or Scott encodings. Just introduce regular natural numbers and lists as ground types; when you later have a better understanding, write programs to transform regular numerals from and to Church numerals and bask in the fact that they are isomorphic.
prakashrj
[dead]
WorldMaker
I think the most ELI5 approach is Alligator Eggs [0] which was built for 8-year-olds to play like a game. You can find a lot of the advanced concepts outside of the core also explained in terms of Alligator Eggs and some software visualizers, but there's also something to be said about hands on learning and about printing it out yourself on some cardstock or cardboard paper, cutting it out, personalizing it with crayons, and playing it with a child or at least your inner child.
joseda-hg
It's too basic for what you need but the video from eyesomorphic [1], is a wonderful conceptual introduction
tromp
> Whilst it certainly isn't a contender for modern programming languages
Yet all that separates the λ-calculus from one modern programming language, Haskell, is a layer of syntactic sugar on top, and a runtime that effectuates its pure IO actions. We can in fact compile Haskell programs using just stdin/stdout for IO into terms of the untyped lambda calculus, as wonderfully demonstrated in Ben Lynn's IOCCC entry [1], or equivalently, into BLC programs.
JadeNB
> Yet all that separates the λ-calculus from one modern programming language, Haskell, is a layer of syntactic sugar on top, and a runtime that effectuates its pure IO actions. We can in fact compile Haskell programs using just stdin/stdout for IO into terms of the untyped lambda calculus, as wonderfully demonstrated in Ben Lynn's IOCCC entry [1].
That's what Turing completeness means, though; you can do the same thing with C, with the same provisos. (Conal Elliott has an amusing satire on this: http://conal.net/blog/posts/the-c-language-is-purely-functio... .) It's not that the lambda calculus isn't sufficiently expressive, just that it's not a language in which humans want to write.
JadeNB
"To mock a mockingbird" (https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird) is a wonderful introduction to something that's sufficiently more abstract than lambda calculus that you'll probably find the latter pleasingly concrete afterwards, but it takes only tiny, bite-sized steps (err, mixed metaphors) to get you to understanding.
Joker_vD
Does anyone have a gentle introduction on binary λ-calculus? I've tried reading other pages on this site but it goes a bit too fast for me understand what the hell is going on with it.
shayansm1
I found this helpful https://brilliant.org/wiki/lambda-calculus/
memming
"our 521 byte virtual machine is expressive enough to implement itself in just 43 bytes" whaat!
johnisgood
The 43-byte implementation might define only a subset of the functionality provided by the full VM, enough to "bootstrap" into the full implementation, most likely.
In fact, if the VM is Turing complete, it can theoretically emulate any computation, including its full implementation, even from a small subset of operations.
The point is that the 43-byte implementation does not need to encode the entire VM explicitly. For example, if the VM has built-in primitives for looping, branching, and memory management, the minimal implementation can leverage these to rebuild the remaining functionality.
tromp
My IOCCC entry [1] explains exactly what the 43-byte program is. It's a self-interpreter for BLC8, the byte based version of Binary Lambda Calculus.
The 521 byte interpreter on the other hand is written in x86 assembly, a language much less suitable for writing BLC8 interpreters than BLC8 itself.
Btw, with my latest lambda compiler, the BLC8 self interpreter is only 42 bytes:
λ 1 ((λ 1 1) (λ (λ λ λ 1 (λ λ λ 2 (λ λ λ (λ 7 (10 (λ 5 (2 (λ λ 3 (λ 1 2 3)))
(11 (λ 3 (λ 3 1 (2 1))))) 3) (4 (1 (λ 1 5) 3) (10 (λ 2 (λ 2 (1 6))) 6))) 8)
(λ 1 (λ 8 7 (λ 1 6 2)))) (λ 1 (4 3))) (1 1)) (λ λ 2 ((λ 1 1) (λ 1 1))))
Dansvidania
thanks, this is helping me understand the whole article a bit better.
johnisgood
Yeah, I just took a real look now. It uses a metacircular evaluator? I didn't look at the link provided just yet though! :D
bjourne
Does it handle alpha-renaming? Most of the golfed interpreters I've seen over the years does not and hence does not handle the full untyped lambda calculus.
tromp
Binary Lambda Calculus uses de-Bruijn indices [1], thereby avoiding the need for alpha renaming.
null
rizky05
Does not work on mac:
> { printf 0010; printf 0101; } | ./lambda.com; echo
zsh: done { printf 0010; printf 0101; } |
zsh: segmentation fault ./lambda.com
I've been attracted to this - along with 2D cellular automata - a bit like a moth to a flame for some time. I find the little machine visualisations mesmerising, the heavily parenthesized Greek representation charming (they look like standing orders written in an alien language, looking for all the world like space invaders) and the tiny code sizes magical.
But I can't quite wrap my mind around the core concepts and internalize them into a mental model. It's too different from the simple world of imperative C or scripting languages I guess I call home. So I'm left watching das blinkenlights from the outside, as my attention span chokes on the layers of computer science incorporated into typical explanations. *shrug*
I'd be very interested if anyone knows of an ELI5-style alternate path I could walk to break each of the concepts down one at a time. (I ask because I think this is (currently) the kind of thing I think ChatGPT would struggle to present as effectively as a human.)