Lambda Calculus Interactive Tutorial | Hacker News Reader

Lambda Calculus Interactive Tutorial

blog.klipse.tech

83 pointsviebel30 comments

I really enjoyed A Tutorial Introduction to Lambda Calculus by Raul Rojas. Apparently he released a new version last year: https://arxiv.org/abs/1503.09060

Enjoyed it also.

Oh wow, I printed an older version and have been reading it during my commutes for past few days. So happy that there's a newer version.

I'm probably showing my profound ignorance, but what has lambda calculus done for me lately? It seems to be an abstract formalism of some sort, but I've yet to see any real use of it, the examples are baby step type stuff with obfuscated syntax.

CS seems overburdened with jargon and trendy crap (IMO) so is this just the latest thing coming down the pike that everyone needs to give lip service to in order to seem smart to their peers?

Here is how you can use the lambda calculus to compute factorials in non-geological time:

http://www.flownet.com/ron/lambda-calculus.html

There is also this article about Y-combinator implemetation in clojure: http://www.viksit.com/tags/clojure/practical-applications-y-...

OMG, that's insane (in a bad way). Stacks exploding, hours of optimization, all for a simple factorial (toy problem). Exciting I suppose for a few souls in academia who spend their lives writing papers about theoretical stuff (not that there's anything wrong with that).

Oh dear, I have failed. The whole point of that paper was supposed to be that all this theory stuff actually has practical applications. The same techniques that worked on that toy problem can be used on real problems and produce similar results.

I did some follow-up work after that paper to implement binary arithmetic in the lambda calculus, and using that, of course, you can compute "real" factorials. Here it is computing the factorial of 100 in under a second:

  ? (time (pbn (bn_fact (bn 100))))
  (PBN (BN_FACT (BN 100)))
  took 942,269 microseconds (0.942269 seconds) to run.
        64,791 microseconds (0.064791 seconds, 6.88%) of which was spent in GC.
  During that period, and with 4 available CPU cores,
       878,343 microseconds (0.878343 seconds) were spent in user mode
       111,475 microseconds (0.111475 seconds) were spent in system mode
   759,285,088 bytes of memory allocated.
   504 minor page faults, 0 major page faults, 0 swaps.
  93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000

This is he expanded code:

  ((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
   (λ f
    (λ n
       (λ nil
          (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) n)
            (λ dummy ((λ (l r s) (s l r)) (λ (_t e) _t) (λ s (λ (_t e) _t))))
            (λ dummy
               (((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
                 (λ f
                    (λ (n1 n2 r)
                       (λ nil
                          (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) n1) (λ dummy r)
                            (λ dummy
                               (f
                                ((λ (l)
                                    (λ nil
                                       (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                         (λ dummy (λ s (λ (_t e) _t))) (λ dummy ((λ p (p (λ (l r) r))) l)))
                                        (λ x x))))
                                 n1)
                                ((λ (l r s) (s l r)) (λ (_t e) e) n2)
                                (((λ (l)
                                     (λ nil
                                        (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                          (λ dummy (λ (_t e) e)) (λ dummy ((λ p (p (λ (l r) l))) l)))
                                         (λ x x))))
                                  n1)
                                 (((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
                                   (λ f
                                      (λ (n1 n2 c)
                                         (λ nil
                                            (((λ (c _t e) (c _t e))
                                              ((λ (p q) (p q (λ (_t e) e))) ((λ p (p (λ (l r) (λ (_t e) e)))) n1)
                                               ((λ p (p (λ (l r) (λ (_t e) e)))) n2))
                                              (λ dummy
                                                 (c ((λ (l r s) (s l r)) (λ (_t e) _t) (λ s (λ (_t e) _t)))
                                                  (λ s (λ (_t e) _t))))
                                              (λ dummy
                                                 ((λ (l r s) (s l r))
                                                  ((λ (b1 b2 c)
                                                      (b1 (b2 c ((λ c (c (λ (_t e) e) (λ (_t e) _t))) c))
                                                       (b2 ((λ c (c (λ (_t e) e) (λ (_t e) _t))) c) c)))
                                                   ((λ (l)
                                                       (λ nil
                                                          (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                                            (λ dummy (λ (_t e) e)) (λ dummy ((λ p (p (λ (l r) l))) l)))
                                                           (λ x x))))
                                                    n1)
                                                   ((λ (l)
                                                       (λ nil
                                                          (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                                            (λ dummy (λ (_t e) e)) (λ dummy ((λ p (p (λ (l r) l))) l)))
                                                           (λ x x))))
                                                    n2)
                                                   c)
                                                  (f
                                                   ((λ (l)
                                                       (λ nil
                                                          (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                                            (λ dummy (λ s (λ (_t e) _t)))
                                                            (λ dummy ((λ p (p (λ (l r) r))) l)))
                                                           (λ x x))))
                                                    n1)
                                                   ((λ (l)
                                                       (λ nil
                                                          (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                                            (λ dummy (λ s (λ (_t e) _t)))
                                                            (λ dummy ((λ p (p (λ (l r) r))) l)))
                                                           (λ x x))))
                                                    n2)
                                                   ((λ (b1 b2 c) (b1 (b2 (λ (_t e) _t) c) (b2 c (λ (_t e) e))))
                                                    ((λ (l)
                                                        (λ nil
                                                           (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                                             (λ dummy (λ (_t e) e))
                                                             (λ dummy ((λ p (p (λ (l r) l))) l)))
                                                            (λ x x))))
                                                     n1)
                                                    ((λ (l)
                                                        (λ nil
                                                           (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) l)
                                                             (λ dummy (λ (_t e) e))
                                                             (λ dummy ((λ p (p (λ (l r) l))) l)))
                                                            (λ x x))))
                                                     n2)
                                                    c)))))
                                             (λ x x))))))
                                  n2 r (λ (_t e) e))
                                 r))))
                           (λ x x))))))
                n
                (f
                 (((λ f ((λ g (g g)) (λ (h x) ((f (h h)) x))))
                   (λ f
                      (λ n
                         (λ nil
                            (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) (λ (_t e) e)))) n) (λ dummy n)
                              (λ dummy
                                 (λ nil
                                    (((λ (c _t e) (c _t e)) ((λ p (p (λ (l r) l))) n)
                                      (λ dummy
                                         (((λ p (p (λ (l r) (λ (_t e) e)))) ((λ p (p (λ (l r) r))) n))
                                          (λ s (λ (_t e) _t))
                                          ((λ (l r s) (s l r)) (λ (_t e) e) ((λ p (p (λ (l r) r))) n))))
                                      (λ dummy ((λ (l r s) (s l r)) (λ (_t e) _t) (f ((λ p (p (λ (l r) r))) n)))))
                                     (λ x x)))))
                             (λ x x))))))
                  n))
                (λ s (λ (_t e) _t)))))
           (λ x x))))))"

I didn't write that all by hand, of course. I built it up in pieces and my "compiler" assembled it for me. But start to finish that took be about an hour.

If we were playing the Hot and Cold game you would be getting colder.

Are you telling me that the most efficient means of generating factorials is via LC? That no other method can touch it in terms of real time?

No, of course not. Factorial are just an illustrative example.

My goal was to dispel the myth that the lamdba calculus is nothing more than an intellectual curiosity. It is much, much more than that, not because you can use it to compute factorials, but because the techniques that you use to compute factorials in LC are generally applicable. If you really want to master the craft there are a few things you really need to know how to do: write your own compiler, your own editor, your own implementation of the Hindley-Milner type system. Writing an efficient factorial in LC is like that. It's not useful in and of itself, but for what you learn simply by going through the process.

Your initial words were "Here is how you can use the lambda calculus to compute factorials in non-geological time" which led me to believe you were claiming LC was a very (the most?) efficient route to factorial calculation. Which would make me sit up and take notice were that the case.

I'm sorry to say that your factorial example just seems painful and pointless to me, and doesn't encourage me to expand my mind via LC at all.

:-(

> LC was a very (the most?) efficient route to factorial calculation

It is, because it is a standard model for computation. To put it in layman terms, every programming language is lambda calculus in disguise. You have absolutely no idea of computability theory. That is the theory in which the P=NP conjecture is formulated, which has massive implications e.g. on cryptography.

You seem frustrated for not understanding at all what's going on here and you try to provoke answers. I know what I'm talking about, because I don't grok LC either and I get furious quickly when I'm hungry, tired or overworked. You are paranoid.

> trendy crap

> 80 year old concept that has spanned dozens of programming languages.

I don't even disagree with you, the "throwback to the roots" thing is not very useful most of the time, except for intellectual curiosity.

lambda calculus is still extremely useful for Prog lang theory, though, because that's the simplest thing you can imagine. If you want to prototype your fancy new type system or weird new execution model, you always design it on the lambda calculus first.

>so is this just the latest thing coming down the pike that everyone needs to give lip service to in order to seem smart to their peers?

Lambda calculus was created by Alonzo Church in the 1930s. Alongside the work of Alan Turing, it forms a large part of the mathematical basis for modern computer science[0][1], and the implementation of many, if not most, modern programming languages.

[0]https://en.wikipedia.org/wiki/Lambda_calculus

[1]https://en.wikipedia.org/wiki/Church-Turing_thesis

Hacker News, was written in a Lisp. Lisp was developed as a language for more closely describing programs in the manner Lambda Calculus describes algorithms in contrast to languages for describing programs more closely to the manner in which Turing Machines describe algorithms.

So as recently as now, it might be argued that the Lambda Calculus has helped waste time reading this here comment. Whether that's something it's done for anyone or undone is a matter of perspective.

I think there are two interpretations and @dewster probably wants to refer to only one of them:

- Knowledge that is implicitly contained in larger objects or concepts, but there is no need for users of those larger objects/concepts to know them. That is the vast majority of all knowledge and encompasses the things we don't even know we don't know yet. You can use a hammer on a nail without knowing anything about what is holding that hammer together or about Newton's laws.

- Explicit knowledge that you use directly. The comment is about this. Meaning, a response that lambda calculus is with us here and now implicitly falls into the first category above and is not what is meant, but why would you be better off knowing the concept directly apart from intellectual curiosity - which we can fulfill on only an insignificantly tiny fraction of the things we do.

Each time people want to add to the curriculum "you absolutely must know this!" they seem to be missing this distinction.

Given the incredibly amount of knowledge and how each and every piece of it is somehow important - but almost always only implicitly - I prefer a mindset that strives to reduce the amount I want other people to learn. Saying "no, you don't have to know/learn this" seems to be a better goal than trying to list ever more stuff. Also, the "need to know" should be much more targeted - "every programmer needs to know" is probably wrong for a lot of (most?) stuff that is labeled thus.

Thank you for expressing that better than I could ever do. Outside of JS sucking but being saved by extensibility, and academic interests, I've never heard a concrete reason why LC is important in a practical sense to most programmers. Can't swing a dead cat on the internet without hitting an LC article lately, and I really don't get the sudden interest and insistence that we all must learn it.

Looking into LC I was led to Curry's Paradox, the natural language version being "If this sentence is true, then Germany borders China" which (again, I'm probably just an idiot) doesn't strike me as paradox material.

This isn't some random reverse snobbery rant, I'm all for digging deep and really understanding things (I do this all the time, probably more than most engineers). But I can't see the Emperor's clothes everyone seems to be admiring, and it isn't for lack of looking.

"If this sentence is true, <false thing>" is a paradox like "this sentence is false". Implication is trivially true when the condition is false. But that would make the condition true and the sentence false.

So once again I try to interpret OP:

I think it's clear that this is a paradox in the field of logic - but only there. Few people not trained and/or thinking of "logic" (that math thing) will find this sentence paradoxical, more like "useless/meaningless". Normal people use paradox more for things like the "French paradox" (the French are health despite eating "unhealthily"). Which isn't a paradox in any logical sense, and even on a human level I myself see the paradox more in the fact that some people see a paradox at all instead of just admitting that what they think is true about nutritional science just isn't (that French phenomenon can be shown to be true in statistics, it's not just imagination).

> Normal people use paradox more for things like the "French paradox"

Maybe. Certainly, common use (and traditional use, e.g. Zeno's Paradox) include things that are not strictly a logical paradox. But I think that most people (and certainly overwhelmingly most programmers) consider "this sentence is false" to be a paradox - which is part of why I picked it as a point of reference.

As others have noted, LC is hardly trendy crap and you might say that 80% of CS is just trying to find more natural names for LC.

But what I'll say is that LC has done a lot for you lately. It, alongside Turing Machines, formed the basis for pretty much all of CS research and programming language design since the beginning of the 20th century. It has heavily influenced the design of probably every programming language you've ever used.

LC pretty much defines the notion of lexical scope. It pretty much defines the notion of constant and nearly defines the idea of variable as used in most languages. It gives a quick proof that recursion arises naturally even in very simple linguistic situations. In fact, it even gives the name of the very website you're reading right now.

LC is a huge force for how people are have been forming new ideas around Functional Programming over the last few decades and how they continue to now.

LC is hugely important. You don't have to learn it because it's already been pre-digested into everything you do in programming. But to not know it is to miss out on seeing the core of how your tools work.

Again, I'm most likely an idiot, but I'm just not seeing it in any of the examples I've encountered. Not trying to be dense, I realize the onus is mostly on me here, and I really am interested in fundamentals. Just wondering if there is a better example of why I should go out of my way to understand lambda calculus, cause this one ain't cutting it. LC may well indeed form the basis of everything CS - if so why doesn't it seem very impressive at first (and second, and third) sight?

If you work in a big company making internal web apps for HR to manage payroll, then no, the lambda calculus will never be useful to you.

However, if you want to do research, it is an invaluable model of how computation works. It's simplicity allows for reasoning about complex ideas while minimizing the cognitive overhead of the model.

It may also help you understand why certain functional styles behave the way they do or how to better implement programming languages.

If none of those things interest you, then yes, it is not useful. But a large crowd here IS interested in computer science theory and programming language theory and functional programming so they are interested.

As a final analogy, you might consider this the 'Standard Model' of computation much like there is the Standard Model in particle physics. If you are a civil engineer, it will never be useful. If you are a chemist, it might be useful only in passing. But if you are the physicist, it is invaluable.

> why doesn't it seem very impressive at first (and second, and third) sight?

That's a super interesting question. Pretty much the entire challenge of LC is coming to understand why it's interesting. From our perspective, so far past the consequences of this discovery, it will all seem too obvious to state. The interestingness of LC comes out of it being so austere and so powerful.

Frankly, this page's intro to it is sort of terrible. Clojure is too powerful and clunky to point directly at LC and show why it's interesting.

LC is a language with three constructors

    var[x]         reference a name
    lam[x](...)    create a scope where x is *known*
    app(f, v)      when f is lam[x], give 
                   meaning to x within its body

Forget ideas of functions or anything else you know from CS. Just think about what these three constructors mean. To give them real meaning we have to define one more thing: the reduction step. It's what you think it is

    app(lam[x](body), value) ==> body{x -> value}

where the right side means that we replace all instances of "x" within "body" with "value".

So imagine that to be the definition of a programming language---the whole thing. It seems a bit silly. It doesn't obviously have any of

    - numbers
    - if-the-else
    - for loops
    - recursion
    - mutation
    - data types

It doesn't even seem to have any way of talking about how it instructs a machine on what to do. It's truly austere.

So the magic, of course, is that it actually does have all of the above. Those 3 constructors and one rule are powerful enough already to generate all of that.

That's what's remarkable.

The best answer to this is the success of JavaScript. JavaScript historically has been a deeply flawed language. However, it was able to become one of the most widely used languages precisely because, despite all its warts, it implements the core foundations from the lambda calculus correctly (lambda functions, first class functions and closures). This allowed JS programmers enormous power to overcome these warts. Here are two examples:

JavaScript historically has no way to do namespacing. In most languages this would be a deal breaker. But because JavaScript has lambda functions, closures and first class functions a solution could be crafted from scratch! Immediately-Invoked Function Expressions (IIFE) were one of the most powerful early techniques to create scopes on the fly in JavaScript. Without these tools from the lambda calculus you would normally have to rely on language level changes to allow these problems to be fixed.

The other early challenge of JavaScript was the need for asynchronous callbacks. Often these require passing around data that you might not have access to when a function is written. Lambda functions allow programmers to quickly write ad hoc logic. First class functions allow programmers to pass around this logic. And most importantly closures allow you to create functions on the fly based on data that is not known until an asynchronous callback is applied. Again without the core ideas of the lambda calculus in place this type of power would require significant language-level design changes.

10 years ago JavaScript was a hideous language, with many major issues. But because in this mess was contained the power of the lambda calculus the language was able to be salvaged and extended to a wide range of uses.

> it was able to become one of the most widely used languages precisely because, despite all its warts, it implements the core foundations from the lambda calculus correctly

You think that's why Javascript is widely used? I think it's widely used because it was already useable within the browser and people just kept going with it.

This tutorial is about Boolean Algebra in Lambda Calculus.

Here is the first part of the tutorial (about arithmetics) http://blog.klipse.tech/lambda/2016/07/24/lambda-calculus-1....

I didn't like this tutorial. I don't think that using Lisp clarifies what is going on.

They claim to show how numbers are created in lambda calculus, by defining some lisp functions that call take a function and call it on itself n times (starting from... what?). And then they just use the builtin lisp function "inc" and claim this somehow shows how numbers are represented.

That doesn't make any sense to me. They haven't shown how 45 is represented in lambda calculus. Is it just represented as "inc" called 45 times, starting from the number 0? If so, why is zero special? What is the connection between "inc" and representation of numbers in lambda calculus? I'm a mathematician and this is similar to one way to define integers, so I may be filling in blanks that aren't there.

Then they try to show equality between numbers (which doesn't exactly work "because Lisp") by showing that the two functions generated by this process are equal... of course they are! You started with two numbers which were already equal, this isn't a proof of anything!

Basically this gave me no insight into lambda calculus but I learned a couple of lisp functions.

> We are using clojure for the code snippets - as it belongs to the LISP family, and LISP is founded on top of lambda calculus.

The lambda calculus doesn't have functions of more than one argument, which is itself a variable standing for a lambda term (satisfying additional restrictions, depending on your choice of reduction strategy). If you want functions of more arguments, you need to curry them. If you want arguments to have arbitrary structure, you need to Church-encode them.

The lambda calculus doesn't have macros or any other means to analyze its own syntax. The only thing you can do with a lambda abstraction is apply it. That's precisely why it's called lambda abstraction: you don't get to peek into its internals. Which is why it's a theorem, and not a triviality, that the lambda calculus is as expressive as Turing machines. (As long as you only care about computability, that is.)

The lambda calculus doesn't have pretty-printing. If you want it, it has to be an external facility (say, of the REPL), not a first-class operation internal to the system. Warning: pretty-printing lambda terms can cause psychological trauma.

For obvious reasons, nobody uses the lambda calculus as a serious programming language. But there are several actual implementations floating around the Interwebs. And, if you don't want to use those, implementing the lambda calculus on your own isn't even hard. So, if your goal is to teach the lambda calculus, why not actually implement and actually use the lambda calculus?

Reply on news.ycombinator.com