Some more examples, together with graphical notation:
Lambda Calculus Examples (2009) [pdf]
11–19 of 19 posts
Re: Lambda Calculus Examples (2009) [pdf]
#12What's a good way for someone without much of a background in maths to start grokking this? I've had had several encounters with the lambda calculus over the years (including a coworker who is absolutely in love with it), but it's never really clicked for me in any meaningful way.
I have good experience with this book: An Introduction to Functional Programming Through Lambda Calculus https://www.amazon.com/Introduction-Functional-Programming-C...
It starts with the general rules of lambda calculus, then build up some basic functions (like in the PDF linked in this thread) and continues to build data types like Natural Numbers, List, String, Tree and operators for manipulating them. The book also explains about the evaluation methods as well as covering how ML and LISP uses lambda calculus.
Re: Lambda Calculus Examples (2009) [pdf]
#13What's a good way for someone without much of a background in maths to start grokking this? I've had had several encounters with the lambda calculus over the years (including a coworker who is absolutely in love with it), but it's never really clicked for me in any meaningful way.
There's an older book by Smullyan - To Mock a Mockingbird but the style is extremely abstract. Edit: I see another commenter has mentioned it as well.
Re: Lambda Calculus Examples (2009) [pdf]
#14Another good reference, that also introduces some PLT notation, is Loh 2001, "Introduction to the Dependently-Typed Lambda Calculus" [1], as well as the textbook by Pierce [2], which has a formally-verified spiritual successor [3]. [1] http://www.cs.ru.nl/~wouters/Publications/Tutorial.pdf [2] https://www.cis.upenn.edu/~bcpierce/tapl/ [3] https://softwarefoundations.cis.upenn.edu/plf-current/index....
Types and Programming Languages by Pierce is an amazing book. I'm still far from finishing it, but if anyone is looking for a good introduction to the field, this is it. I consider it to be kind of like the SICP of PL. :)
Edit: Ah, and the Software Foundations books are amazing. I did a little course on formal verification during 2020 and learned a ton. Now every time I work with some kind of type system, I feel frustrated that I can't express everything that I want to in my type system.
Re: Lambda Calculus Examples (2009) [pdf]
#15Another good reference, that also introduces some PLT notation, is Loh 2001, "Introduction to the Dependently-Typed Lambda Calculus" [1], as well as the textbook by Pierce [2], which has a formally-verified spiritual successor [3]. [1] http://www.cs.ru.nl/~wouters/Publications/Tutorial.pdf [2] https://www.cis.upenn.edu/~bcpierce/tapl/ [3] https://softwarefoundations.cis.upenn.edu/plf-current/index....
Types and Programming Languages by Pierce is an amazing book. I'm still far from finishing it, but if anyone is looking for a good introduction to the field, this is it. I consider it to be kind of like the SICP of PL. :) Edit: Ah, and the Software Foundations books are amazing. I did a little course on formal verification during 2020 and learned a ton . Now every time I work with some kind of type system, I feel fru…
Another alternate is "Practical Foundations for Programming Languages" by Bob Harper [1]. It is a bit more broad than TAPL (imo).
Re: Lambda Calculus Examples (2009) [pdf]
#16Another good reference, that also introduces some PLT notation, is Loh 2001, "Introduction to the Dependently-Typed Lambda Calculus" [1], as well as the textbook by Pierce [2], which has a formally-verified spiritual successor [3]. [1] http://www.cs.ru.nl/~wouters/Publications/Tutorial.pdf [2] https://www.cis.upenn.edu/~bcpierce/tapl/ [3] https://softwarefoundations.cis.upenn.edu/plf-current/index....
Programming Languages Foundations is an excellent book. Of course it assumes familiarity with Coq (which Logical Foundations covers). Formal proofs about PLs are often boring and tedious to carry out on paper, especially if the property they're stating is clearly obvious, so doing them in an interactive theorem prover is a win-win for checking your work and making the concepts more palatable.
Re: Lambda Calculus Examples (2009) [pdf]
#17Not covered in this PDF but extremely important is the notion of substitution. This is the only computational operation of the lambda calculus, and is the reason why lambda calculus is Turing-complete. Substitution is also hard to get right, but here's how it would work with "fresh" variables[0]. Alternatively one may avoid names altogether and use de Bruijn indices[1], however there's a significant performance cost in doing so. See λ-calculus cooked four ways[2] for more information.
[0] https://en.wikipedia.org/wiki/Lambda_calculus#Capture-avoidi...
[1] https://en.wikipedia.org/wiki/De_Bruijn_index
[2] https://raw.githubusercontent.com/steshaw/lennart-lambda/mas...