5 ms·

Lambda Calculus Examples (2009) [pdf]

144 points by alphanumeric0 5y ago

benrbray 5y ago
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 http://www.cs.ru.nl/~wouters/Publications/Tutorial.pdf [2] https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/ [3] https://softwarefoundations.cis.upenn.edu/plf-current/index.html https://softwarefoundations.cis.upenn.edu/plf-current/index....
- ashton314 5y ago
  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.
  - shadowfox 5y ago
    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/ https://www.cs.cmu.edu/~rwh/pfpl/
- siraben 5y ago
  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.
dgb23 5y ago
related: https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird
- louthy 5y ago
  And the obligatory: https://dkeenan.com/Lambda/ https://dkeenan.com/Lambda/
heinrichhartman 5y ago
Ha! This paper contains the definition of Y-Combinator: > Y combinator: Y = λt. (λx. t (x x)) (λx. t (x x)) #TIL!
- louthy 5y ago
  Which enables recursion
  - Akronymus 5y ago
    And applying the lambda to itself results in loops, afair. Edit: It was the Omega operator that did that.
    - kmill 5y ago
      omega = Y id where id = λx. x (though Y Y does not normalize either, infinite looping like omega)
elric 5y ago
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.
- panzerklein 5y ago
  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 https://www.youtube.com/watch?v=6BnVo7EHO_8
- jumanjisama 5y ago
  I have good experience with this book: An Introduction to Functional Programming Through Lambda Calculus https://www.amazon.com/Introduction-Functional-Programming-Calculus-Mathematics/dp/0486478831/ 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.
- selimthegrim 5y ago
  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.
globular-toast 5y ago
For someone fluent in Python, David Beazley gives a brilliant introduction to lambda calculus here: https://www.youtube.com/watch?v=pkCLMl0e_0k https://www.youtube.com/watch?v=pkCLMl0e_0k This is great fun to follow through on a rainy afternoon!
lisper 5y ago
Factorials in pure lambda calculus: https://flownet.com/ron/lambda-calculus.html https://flownet.com/ron/lambda-calculus.html
tromp 5y ago
Some more examples, together with graphical notation: https://tromp.github.io/cl/diagrams.html https://tromp.github.io/cl/diagrams.html
siraben 5y ago
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-avoiding_substitutions https://en.wikipedia.org/wiki/Lambda_calculus#Capture-avoidi... [1] https://en.wikipedia.org/wiki/De_Bruijn_index https://en.wikipedia.org/wiki/De_Bruijn_index [2] https://raw.githubusercontent.com/steshaw/lennart-lambda/master/top.pdf https://raw.githubusercontent.com/steshaw/lennart-lambda/mas...

144 points by alphanumeric0 5y ago

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 http://www.cs.ru.nl/~wouters/Publications/Tutorial.pdf [2] https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/ [3] https://softwarefoundations.cis.upenn.edu/plf-current/index.html https://softwarefoundations.cis.upenn.edu/plf-current/index....

ashton314 5y ago
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.
- shadowfox 5y ago
  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/ https://www.cs.cmu.edu/~rwh/pfpl/
siraben 5y ago
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.

dgb23 5y ago

related: https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird

louthy 5y ago
And the obligatory: https://dkeenan.com/Lambda/ https://dkeenan.com/Lambda/

heinrichhartman 5y ago

Ha! This paper contains the definition of Y-Combinator: > Y combinator: Y = λt. (λx. t (x x)) (λx. t (x x)) #TIL!

louthy 5y ago
Which enables recursion
- Akronymus 5y ago
  And applying the lambda to itself results in loops, afair. Edit: It was the Omega operator that did that.
  - kmill 5y ago
    omega = Y id where id = λx. x (though Y Y does not normalize either, infinite looping like omega)

elric 5y ago

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.

panzerklein 5y ago
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 https://www.youtube.com/watch?v=6BnVo7EHO_8
jumanjisama 5y ago
I have good experience with this book: An Introduction to Functional Programming Through Lambda Calculus https://www.amazon.com/Introduction-Functional-Programming-Calculus-Mathematics/dp/0486478831/ 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.
selimthegrim 5y ago
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.

globular-toast 5y ago

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

lisper 5y ago

Factorials in pure lambda calculus: https://flownet.com/ron/lambda-calculus.html https://flownet.com/ron/lambda-calculus.html

tromp 5y ago

Some more examples, together with graphical notation: https://tromp.github.io/cl/diagrams.html https://tromp.github.io/cl/diagrams.html

siraben 5y ago

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-avoiding_substitutions https://en.wikipedia.org/wiki/Lambda_calculus#Capture-avoidi... [1] https://en.wikipedia.org/wiki/De_Bruijn_index https://en.wikipedia.org/wiki/De_Bruijn_index [2] https://raw.githubusercontent.com/steshaw/lennart-lambda/master/top.pdf https://raw.githubusercontent.com/steshaw/lennart-lambda/mas...