[HN Gopher] Lambda Calculus in 383 Bytes (2022)
___________________________________________________________________
Lambda Calculus in 383 Bytes (2022)
Author : MrBuddyCasino
Score : 211 points
Date : 2025-01-13 01:53 UTC (2 days ago)
(HTM) web link (justine.lol)
(TXT) w3m dump (justine.lol)
| memming wrote:
| "our 521 byte virtual machine is expressive enough to implement
| itself in just 43 bytes" whaat!
| johnisgood wrote:
| 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 wrote:
| 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: l 1 ((l 1 1)
| (l (l l l 1 (l l l 2 (l l l (l 7 (10 (l 5 (2 (l l 3 (l 1 2
| 3))) (11 (l 3 (l 3 1 (2 1))))) 3) (4 (1 (l 1 5) 3)
| (10 (l 2 (l 2 (1 6))) 6))) 8) (l 1 (l 8 7 (l 1 6
| 2)))) (l 1 (4 3))) (1 1)) (l l 2 ((l 1 1) (l 1 1))))
|
| [1] https://www.ioccc.org/2012/tromp/
| johnisgood wrote:
| 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
| cess11 wrote:
| "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.
| Dansvidania wrote:
| thanks, this is helping me understand the whole article a
| bit better.
| rizky05 wrote:
| Does not work on mac: > { printf 0010; printf
| 0101; } | ./lambda.com; echo zsh: done {
| printf 0010; printf 0101; } | zsh: segmentation fault
| ./lambda.com
| tromp wrote:
| 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)
| freehorse wrote:
| No it does not (I opened the x86 version of the terminal with
| rosetta and run the commands and get the same error).
| freehorse wrote:
| 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.
| exikyut wrote:
| 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.)
| joseda-hg wrote:
| 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
| tromp wrote:
| > Whilst it certainly isn't a contender for modern
| programming languages
|
| Yet all that separates the l-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
| JadeNB wrote:
| > Yet all that separates the l-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.
| tromp wrote:
| 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).
| JadeNB wrote:
| > 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.
| dunham wrote:
| 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/
| nakedneuron wrote:
| video author is using 3b1b's manim
| (https://github.com/3b1b/manim). wonderful presentation.
| JadeNB wrote:
| "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.
| kccqzy wrote:
| 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.
| WorldMaker wrote:
| 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/
| nakedneuron wrote:
| sorry for not providing explanations, but check this out:
| https://tromp.github.io/cl/diagrams.html
|
| did you see https://news.ycombinator.com/item?id=42256394 (The
| Art and Mathematics of Genji-Ko 172 points, by olooney, 49 days
| ago, 10 comments)? very tangentially related, but also
| mesmerizing stuff, i think..
| bjourne wrote:
| 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 wrote:
| Binary Lambda Calculus uses de-Bruijn indices [1], thereby
| avoiding the need for alpha renaming.
|
| [1] https://en.wikipedia.org/wiki/De_Bruijn_index
| Joker_vD wrote:
| Does anyone have a gentle introduction on binary l-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 wrote:
| I found this helpful https://brilliant.org/wiki/lambda-
| calculus/
| lucasoshiro wrote:
| 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
| Joker_vD wrote:
| Sorry, I meant _binary_ l-calculus specifically. I can 't
| quite wrap my head around what the hell it even does with its
| I/O.
| tromp wrote:
| If the IOCCC description [1] doesn't make it clear enough,
| perhaps this explanation [2] does it better? I also link to
| a Pi Day 2023 talk trying to explain it on my lambda
| playground page [3].
|
| [1] https://www.ioccc.org/2012/tromp/
|
| [2] https://gist.github.com/tromp/86b3184f852f65bfb814e3ab0
| 987d8...
|
| [3] https://tromp.github.io/cl/cl.html
| mason_mpls wrote:
| Lisp is fairly similar and easy to pick up
| stackghost wrote:
| I feel like I've accidentally stumbled into /r/VXJunkies with
| some of the terminology being thrown around in here.
| dang wrote:
| Discussed at the time (but before it shrank):
|
| _Lambda Calculus in 400 Bytes_ -
| https://news.ycombinator.com/item?id=30493713 - Feb 2022 (63
| comments)
___________________________________________________________________
(page generated 2025-01-15 23:00 UTC)