← Back to context

Comment by Joker_vD

3 days ago

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.

8 comments

Joker_vD

Reply
lucasoshiro  3 days ago

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

mbivert  3 days ago

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

  • jart  3 days ago

    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.

    • mbivert  3 days ago

      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.