5 ms·

A Short Introduction to the Lambda Calculus (2004) [pdf]

166 points by kumaranvpl 10y ago

astrobase_go 10y ago
While the linked explanation makes obvious parallels between the lambda calculus and other programming languages, I think Rojas is even yet more accessible: http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf
0xdeadbeefbabe 10y ago
Why is it a calculus and not an algebra? Relational algebra is an algebra for example.
- virmundi 10y ago
  I believe it comes down to procedural vs declarative. Relational Algebra is fairly procedural (do X, then Y, then Z). Where as Relational Calculus(https://www.tutorialcup.com/dbms/relational-calculus.htm https://www.tutorialcup.com/dbms/relational-calculus.htm) is declarative.
- tel 10y ago
  "Algebra" and "calculus" are often used for historical reasons rather than technical ones. But as it were, LC cannot be expressed as a universal algebra. Not quite. The lambda terms introduce local binding which throws off an algebraic representation. The best you can do is have a (sorted) representation which includes free variables and then have a quotient of that algebra be LC. Even that doesn't quite work, though, since `x` is not a valid LC term.
  - 0xdeadbeefbabe 10y ago
    > The lambda terms introduce local binding which throws off an algebraic representation. Doesn't rho for renaming in relational algebra also have local binding? It's good to know the reasons are historical though.
    - tel 10y ago
      Could be that the relational algebra isn't so much an algebra either. Also could be that the renaming isn't really part of the "core" algebra. I'm not in particular familiar with the relational algebra, though.
- mkehrt 10y ago
  I'm not sure "calculus" has a technical meaning in the same sense "algebra" does, and, as mentioned by tel, the use is mostly historical. But note that other historical simple languages such as combinator systems are often referred to as calculi, like the SKI-calculus. In modern programming language theory, formal models of languages are informally referred to as "calculi" as well, mostly as a reference to the lambda calculus.
  - tel 10y ago
    Interestingly, the SKI calculus is an algebra.
- fmap 10y ago
  Barendregt, in his famous book on the lambda calculus has a great justification: once you look at models for the lambda calculus you are forced to introduce notions from analysis, such as continuity. The arguments and proofs would feel right at home in a book on classical analysis. So it's the models that put the calculus in lambda calculus. :) Of course the real answer is probably history, but it's much more interesting to say that you can simply find connections to calculus if you look hard enough...
arethuza 10y ago
I had to vote this up as it referenced a work by Greg Michaelson who did a splendid job of teaching me about lambda calculus back in the 1980s and who really got my attention when he explained about S and K combinators. Another excellent work from that same time is The Implementation of Functional Programming Languages by Simon Peyton Jones which is available online for free: http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/ http://research.microsoft.com/en-us/um/people/simonpj/papers... [Edit: I know this is an old work - but I'm very fond of it!]
- jlarocco 10y ago
  The Greg Michaelson book is a really great intro, and he's made the postscript sources (without index) available on his website http://www.macs.hw.ac.uk/~greg/books/ http://www.macs.hw.ac.uk/~greg/books/.
- futtetennista 10y ago
  Another (old) gem that I feel like suggesting to anyone interested in this topic is 'Introduction to Functional Programming' by Philip Wadler and Richard Bird, which is also available online for free: https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Introduction%20to%20Functional%20Programming.1ed.pdf https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Intro...
- iflowfor8hours 10y ago
  I have fond memories of playing Alligator Eggs http://worrydream.com/AlligatorEggs/ http://worrydream.com/AlligatorEggs/ With some of my older family members and a couple of mildly intoxicated friends who vaguely understood the theory. It's well worth playing with to learn the lambda calculus.
monkpit 10y ago
Are there answers to the exercises? I'm kind of stuck on 3b in section 8. Should I evaluate from right to left - normalize 'y' lambda given a y-value of 5? Then, in that case, there is only one argument (const 10) to pass to the 'fx' lambda and I guess you end up with a partial or something? Or should the 'y' lambda and the constant 5 be considered the 2 parameters passed to the 'fx' lambda? In which case I guess the answer comes to be const 20?
- icen 10y ago
  λ calculus is left associative - that is, a sequence of applications A B C is interpreted as (A B) C, so we first reduce (λf x. f (f x)) (λy.* 2 y), yielding λx . (λy. * 2 y) ((λy.2 * y) x), and only then apply 5 to it, which finally lets us unravel everything and get 20.
- tromp 10y ago
  > I'm kind of stuck on 3b in section 8. So you managed to do exercise 8.7 ? I wonder if there is an answer shorter than 22 symbols... Nice instance of lambda golfing!
  - monkpit 10y ago
    No, because I got stuck on question 3 :) Also, I find questions like 8.7 to be really uninteresting - it seems like busywork.
amelius 10y ago
The Y combinator is explained on page 7 :)

166 points by kumaranvpl 10y ago

While the linked explanation makes obvious parallels between the lambda calculus and other programming languages, I think Rojas is even yet more accessible: http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf

0xdeadbeefbabe 10y ago

Why is it a calculus and not an algebra? Relational algebra is an algebra for example.

virmundi 10y ago
I believe it comes down to procedural vs declarative. Relational Algebra is fairly procedural (do X, then Y, then Z). Where as Relational Calculus(https://www.tutorialcup.com/dbms/relational-calculus.htm https://www.tutorialcup.com/dbms/relational-calculus.htm) is declarative.
tel 10y ago
"Algebra" and "calculus" are often used for historical reasons rather than technical ones. But as it were, LC cannot be expressed as a universal algebra. Not quite. The lambda terms introduce local binding which throws off an algebraic representation. The best you can do is have a (sorted) representation which includes free variables and then have a quotient of that algebra be LC. Even that doesn't quite work, though, since `x` is not a valid LC term.
- 0xdeadbeefbabe 10y ago
  > The lambda terms introduce local binding which throws off an algebraic representation. Doesn't rho for renaming in relational algebra also have local binding? It's good to know the reasons are historical though.
  - tel 10y ago
    Could be that the relational algebra isn't so much an algebra either. Also could be that the renaming isn't really part of the "core" algebra. I'm not in particular familiar with the relational algebra, though.
mkehrt 10y ago
I'm not sure "calculus" has a technical meaning in the same sense "algebra" does, and, as mentioned by tel, the use is mostly historical. But note that other historical simple languages such as combinator systems are often referred to as calculi, like the SKI-calculus. In modern programming language theory, formal models of languages are informally referred to as "calculi" as well, mostly as a reference to the lambda calculus.
- tel 10y ago
  Interestingly, the SKI calculus is an algebra.
fmap 10y ago
Barendregt, in his famous book on the lambda calculus has a great justification: once you look at models for the lambda calculus you are forced to introduce notions from analysis, such as continuity. The arguments and proofs would feel right at home in a book on classical analysis. So it's the models that put the calculus in lambda calculus. :) Of course the real answer is probably history, but it's much more interesting to say that you can simply find connections to calculus if you look hard enough...

arethuza 10y ago

I had to vote this up as it referenced a work by Greg Michaelson who did a splendid job of teaching me about lambda calculus back in the 1980s and who really got my attention when he explained about S and K combinators. Another excellent work from that same time is The Implementation of Functional Programming Languages by Simon Peyton Jones which is available online for free: http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/ http://research.microsoft.com/en-us/um/people/simonpj/papers... [Edit: I know this is an old work - but I'm very fond of it!]

jlarocco 10y ago
The Greg Michaelson book is a really great intro, and he's made the postscript sources (without index) available on his website http://www.macs.hw.ac.uk/~greg/books/ http://www.macs.hw.ac.uk/~greg/books/.
futtetennista 10y ago
Another (old) gem that I feel like suggesting to anyone interested in this topic is 'Introduction to Functional Programming' by Philip Wadler and Richard Bird, which is also available online for free: https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Introduction%20to%20Functional%20Programming.1ed.pdf https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Intro...
iflowfor8hours 10y ago
I have fond memories of playing Alligator Eggs http://worrydream.com/AlligatorEggs/ http://worrydream.com/AlligatorEggs/ With some of my older family members and a couple of mildly intoxicated friends who vaguely understood the theory. It's well worth playing with to learn the lambda calculus.

monkpit 10y ago

Are there answers to the exercises? I'm kind of stuck on 3b in section 8. Should I evaluate from right to left - normalize 'y' lambda given a y-value of 5? Then, in that case, there is only one argument (const 10) to pass to the 'fx' lambda and I guess you end up with a partial or something? Or should the 'y' lambda and the constant 5 be considered the 2 parameters passed to the 'fx' lambda? In which case I guess the answer comes to be const 20?

icen 10y ago
λ calculus is left associative - that is, a sequence of applications A B C is interpreted as (A B) C, so we first reduce (λf x. f (f x)) (λy.* 2 y), yielding λx . (λy. * 2 y) ((λy.2 * y) x), and only then apply 5 to it, which finally lets us unravel everything and get 20.
tromp 10y ago
> I'm kind of stuck on 3b in section 8. So you managed to do exercise 8.7 ? I wonder if there is an answer shorter than 22 symbols... Nice instance of lambda golfing!
- monkpit 10y ago
  No, because I got stuck on question 3 :) Also, I find questions like 8.7 to be really uninteresting - it seems like busywork.

amelius 10y ago

The Y combinator is explained on page 7 :)