6 ms·

Lambda Calculus Interactive Tutorial

83 points by viebel 10y ago

viebel 10y ago
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.html http://blog.klipse.tech/lambda/2016/07/24/lambda-calculus-1....
- unfamiliar 10y ago
  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.
teamhappy 10y ago
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 https://arxiv.org/abs/1503.09060
- viebel 10y ago
  Enjoyed it also.
- splintercell 10y ago
  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.
dewster 10y ago
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?
- lisper 10y ago
  Here is how you can use the lambda calculus to compute factorials in non-geological time: http://www.flownet.com/ron/lambda-calculus.html http://www.flownet.com/ron/lambda-calculus.html
  - viebel 10y ago
    There is also this article about Y-combinator implemetation in clojure: http://www.viksit.com/tags/clojure/practical-applications-y-combinator-clojure/ http://www.viksit.com/tags/clojure/practical-applications-y-...
  - dewster 10y ago
    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).
    - lisper 10y ago
      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.
catnaroek 10y ago
> 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?

83 points by viebel 10y ago

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.html http://blog.klipse.tech/lambda/2016/07/24/lambda-calculus-1....

unfamiliar 10y ago
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.

teamhappy 10y ago

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 https://arxiv.org/abs/1503.09060

viebel 10y ago
Enjoyed it also.
splintercell 10y ago
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.

dewster 10y ago

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?

lisper 10y ago
Here is how you can use the lambda calculus to compute factorials in non-geological time: http://www.flownet.com/ron/lambda-calculus.html http://www.flownet.com/ron/lambda-calculus.html
- viebel 10y ago
  There is also this article about Y-combinator implemetation in clojure: http://www.viksit.com/tags/clojure/practical-applications-y-combinator-clojure/ http://www.viksit.com/tags/clojure/practical-applications-y-...
- dewster 10y ago
  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).
  - lisper 10y ago
    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.

catnaroek 10y ago

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