alt.hn

1/13/2025 at 1:53:18 AM

Lambda Calculus in 383 Bytes (2022)

 https://justine.lol/lambda/

by MrBuddyCasino

1/15/2025 at 2:31:56 PM

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.)

by exikyut

1/15/2025 at 3:54:45 PM

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.

by kccqzy

1/16/2025 at 2:10:14 AM

Mathematics is not a spectator sport.

I had the luck of reading that quote while I was an undergrad. I did not actually pursue a career in pure math, but it certainly helps me every time I want to understand some math in order to apply it. (Lambda calculus, type systems, Fourier/Laplace/z-transform, ...)

by anyfoo

1/15/2025 at 4:39:50 PM

I agree that you have to do the exercises instead of expecting others to explain and walk you through it.

https://www.youtube.com/watch?v=LXhsutNKhec

Just one programming book was able to help my son, who is 12 yrs old, learn lambda calculus and write a meta circular evaluator.

by prakashrj

1/15/2025 at 4:10:59 PM

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.

[0] https://worrydream.com/AlligatorEggs/

by WorldMaker

1/15/2025 at 2:53:02 PM

It's too basic for what you need but the video from eyesomorphic [1], is a wonderful conceptual introduction

[1] https://www.youtube.com/watch?v=ViPNHMSUcog

by joseda-hg

1/15/2025 at 3:42:45 PM

> 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.

[1] https://www.ioccc.org/2019/lynn/index.html

by tromp

1/15/2025 at 3:46:05 PM

> 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.

by JadeNB

1/15/2025 at 3:51:37 PM

I wasn't just claiming Turing completeness of Haskell. I was pointing out that every language construct, every subexpression in Haskell, directly represents a corresponding lambda term, with corresponding semantics (e.g. laziness).

by tromp

1/15/2025 at 7:05:36 PM

> I wasn't just claiming Turing completeness of Haskell. I was pointing out that every language construct, every subexpression in Haskell, directly represents a corresponding lambda term, with corresponding semantics (e.g. laziness).

I was referring to the Turing completeness of the lambda calculus, not of Haskell. But, again, I think that trying to work directly with lambda expressions everywhere, even if it is possible and, as you say, straightforward for "vanilla" Haskell, quickly shows why we put some semantic sugar over it. That is to say, it's certainly true that, in an obvious sense, the layer of semantic sugar is thinner for Haskell than for C, but it's still "just" semantic sugar, and still just as conceptually important, in both cases.

by JadeNB

1/15/2025 at 8:01:58 PM

For anyone who's interested - Ben Lynn also has a series of articles that explain the creation of that compiler and add further enhancements:

https://crypto.stanford.edu/~blynn/compiler/

by dunham

1/15/2025 at 3:45:00 PM

"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.

by JadeNB

1/16/2025 at 2:11:20 AM

You might find my practical introduction to lambda calculus and combinatory logic based on javascript helpful. [1]

Its mostly based on other introductory resources but I tried to write it from a practical step by step perspective I found most useful for myself.

[1]: https://static.laszlokorte.de/combinators/

by laszlokorte

1/16/2025 at 10:30:45 AM

Spending time with pure functional programming (languages like Haskell) will open up these concepts in a real-world programming environment. Obviously languages like Haskell are more complex than this, but they're all fundamentally based on lambda calculus. That could be the first step away from the imperative thinking you describe.

(That was certainly my way in to this world anyway!)

by louthy

1/16/2025 at 12:45:33 AM

Author here. If anyone wants to see an example of an awesome program you can run on the 520 byte version of my lambda calculus virtual machine (Blc) then check out https://github.com/woodrush/lambdalisp If you run the command in that project, it'll download my VM from the blog post, build a 20kb lambda expression you can pipe into it, and BOOM a fully object-oriented LISP REPL will appear in your terminal. It's like magic. For an example expression, try typing (+ 2 3) and hit enter. Then type (let ((a 2) (b 3)) (+ a b)) and hit enter. You need an x86 linux machine to do this right now.

by jart

1/16/2025 at 6:50:37 AM

Justine - thanks so much for all these amazing projects. You're an inspiration.

One thing I saw you write recently is that chasing the newest fads is a distraction. That makes sense, but if you don't mind me asking, what do you think one should focus on instead? Which are the classic languages, tools, mindsets, and CS concepts that one must master?

by troad

1/16/2025 at 9:08:43 AM

Hi troad, I read your book: https://justine.lol/sectorlisp2/troades.html

I don't remember saying that. You might be thinking about https://justine.lol/ape.html where I said we should be focusing on the old things that matter which aren't going away, like UNIX magic numbers, C libraries, and computer science. But I've got nothing against the new. I think AI for example is exciting. Ultimately you should focus on whatever summons your passion and curiosity. Since if you're tapped into that divine energy within, then you can make anything work, and others will agree. Even if it's just boring old numbers.

by jart

1/15/2025 at 3:37:42 PM

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.

by Joker_vD

1/15/2025 at 5:08:05 PM

I don't know if it will work for you, but I wrote a Quicksort using lambda calculus in Python, and I explained the process of writing it here:

https://lucasoshiro.github.io/software-en/2020-06-06-lambdas...

Please note that I'm not an expert in lambda calculus, just a curious nerd and it won't explain everything, like the reductions, combinators and so on. But there I explain how to implement simple types (int, boolean, pairs and lists) using Church encoding, let expressions and recursion using the Y combinator (yay, I finally used the expression "Y combinator" on HN!). Everything that we need to implement a quicksort (which is a relatively complex algorithm) using the almost nothing that we have in lambda calculus.

Another point is that it's all implemented in Python, using the Python notation instead of the lambda calculus notation, so you can run the code in your machine and play with the examples

by lucasoshiro

1/15/2025 at 5:14:40 PM

Sorry, I meant binary λ-calculus specifically. I can't quite wrap my head around what the hell it even does with its I/O.

by Joker_vD

1/15/2025 at 11:20:12 PM

In case the other answers aren't sufficient, the first step is to understand the λ-calculus[0]. Then, De Bruijn indices[1]. Now, observe that the language we have only has (you need familiarity with the λ-calculus to understand those terms (… pun unintended)) 1/ applications, 2/ abstractions, 3/ integers representing variables [introduced by abstractions]. For example:

    (λ (λ 1 (λ 1)) (λ 2 1))
Binary λ-calculus is then merely about finding a way to encode those three things in binary; here's how the author does it (from the blog post):

    00      means abstraction   (pops in the Krivine machine)
    01      means application   (push argument continuations)
    1...0   means variable      (with varint de Bruijn index)
The last one isn't quite clear, but she gives examples in `compile.sh`:

      s/9/11111111110/g
      s/8/1111111110/g
      s/7/111111110/g
      s/6/11111110/g
      s/5/1111110/g
      s/4/111110/g
      s/3/11110/g
      s/2/1110/g
To check your understanding, you may want to try to manually convert some λ-expressions using those encoding rules, starting with simple ones, and check what you have with what `compile.sh` yields.

[0]: https://www.irif.fr/~mellies/mpri/mpri-ens/biblio/Selinger-L...

[1]: https://en.wikipedia.org/wiki/De_Bruijn_index

by mbivert

1/16/2025 at 12:37:32 AM

I never would have been able to understand lambda calculus well enough to write the blog post if I started with [0]. I say just pull out the shell and start coding things. Then read [0] later to appreciate things on a deeper level.

by jart

1/16/2025 at 1:29:41 AM

I think I must agree: while I went through [0] to build a λ-calculus interpreter, I already had a fair amount of practice with Church encoding (list, bool, int) using an arbitrary functional language, which retrospectively must have helped greatly to make Selinger's notes clearer.

by mbivert

1/15/2025 at 5:48:46 PM

Lisp is fairly similar and easy to pick up

by mason_mpls

1/13/2025 at 3:10:06 AM

"our 521 byte virtual machine is expressive enough to implement itself in just 43 bytes" whaat!

by memming

1/15/2025 at 2:06:34 PM

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.

by johnisgood

1/15/2025 at 2:13:53 PM

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))))
[1] https://www.ioccc.org/2012/tromp/

by tromp

1/15/2025 at 2:18:16 PM

thanks, this is helping me understand the whole article a bit better.

by Dansvidania

1/15/2025 at 2:16:28 PM

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

by johnisgood

1/15/2025 at 2:19:48 PM

"For example, its metacircular evaluator is 232 bits. If we use the 8-bit version of the interpreter (the capital Blc one) which uses a true binary wire format, then we can get a sense of just how small the programs targeting this virtual machine can be."

From TFA. I think it's a very good article.

by cess11

1/15/2025 at 6:31:33 PM

I feel like I've accidentally stumbled into /r/VXJunkies with some of the terminology being thrown around in here.

by stackghost

1/16/2025 at 8:31:18 AM

>nine="λλ [1 [1 [1 [1 [1 [1 [1 [1 [1 0]]]]]]]]]"

Looks like Brainfuck in disguise :)

by kgeist

1/16/2025 at 5:04:19 AM

Anytime i see a Justine post it’s a banger — i had not read this one.

by jkrubin

1/16/2025 at 3:39:16 PM

Very interesting. Is it possible to imagine implementing an OS based on this ? I have been interested by lambda calculus for a while (implemented a lambda calculus interpreter in haskell) and was always wondering if people were working on "functional computers" and if it makes sense

Cheers,

by octagen

1/15/2025 at 2:37:40 PM

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.

by bjourne

1/15/2025 at 2:12:35 PM

Does not work on mac:

  > { printf 0010; printf 0101; } | ./lambda.com; echo
  zsh: done                { printf 0010; printf 0101; } |
  zsh: segmentation fault  ./lambda.com

by rizky05

1/15/2025 at 2:48:41 PM

It doesn't work on modern Apple Silicon macs with M1-4 chips (although Rosetta [1] might be able to handle it somehow), but it works fine on my older x86 based iMac.

[1] https://en.wikipedia.org/wiki/Rosetta_(software)

by tromp

1/15/2025 at 3:51:07 PM

No it does not (I opened the x86 version of the terminal with rosetta and run the commands and get the same error).

by freehorse

1/15/2025 at 10:32:18 PM

If the downvotes are because I am somehow wrong and it can run in rosetta I would be interested to learn how to actually get to run it.

by freehorse

1/16/2025 at 12:48:46 AM

Go on vast.ai and rent an x86 linux machine for an hour. It's worth it for this.

by jart

1/16/2025 at 2:37:53 AM

Moar upboats plz!

by jsmo