A Short Introduction to the Lambda Calculus (2004) [pdf] 166 points by kumaranvpl on Dec 7, 2016 | hide | past | favorite | 18 comments

 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...[Edit: I know this is an old work - but I'm very fond of it!]
 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:
 I have fond memories of playing Alligator Eggshttp://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.
 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/.
 While the linked explanation makes obvious parallels between the lambda calculus and other programming languages, I think Rojas is even yet more accessible:
 Why is it a calculus and not an algebra?Relational algebra is an algebra for example.
 "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.
 > 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.
 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.
 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...
 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.
 Interestingly, the SKI calculus is an algebra.
 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) is declarative.
 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?
 λ 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.
 > 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!
 No, because I got stuck on question 3 :)Also, I find questions like 8.7 to be really uninteresting - it seems like busywork.
 The Y combinator is explained on page 7 :)

Search: