Lambda Calculus Examples (2009) [pdf] | Hacker News Reader

Lambda Calculus Examples (2009) [pdf]

ics.uci.edu

144 pointsalphanumeric018 comments

Another 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.

Another alternate is "Practical Foundations for Programming Languages" by Bob Harper [1]. It is a bit more broad than TAPL (imo).

[1] https://www.cs.cmu.edu/~rwh/pfpl/

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.

Not 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...

What'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.

Here's one great introduction - A Flock of Functions: Lambda Calculus and Combinatory Logic in JavaScript | Gabriel Lebec @ DevTalks

https://www.youtube.com/watch?v=6BnVo7EHO_8

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.

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.

For someone fluent in Python, David Beazley gives a brilliant introduction to lambda calculus here: https://www.youtube.com/watch?v=pkCLMl0e_0k This is great fun to follow through on a rainy afternoon!

Ha! This paper contains the definition of Y-Combinator:

> Y combinator: Y = λt. (λx. t (x x)) (λx. t (x x))

#TIL!

Which enables recursion

And applying the lambda to itself results in loops, afair.

Edit: It was the Omega operator that did that.

omega = Y id

where id = λx. x

(though Y Y does not normalize either, infinite looping like omega)

Factorials in pure lambda calculus:

https://flownet.com/ron/lambda-calculus.html

Some more examples, together with graphical notation: