[HN Gopher] Lambda Calculus Examples (2009) [pdf]
___________________________________________________________________
Lambda Calculus Examples (2009) [pdf]
Author : alphanumeric0
Score : 122 points
Date : 2021-06-27 05:32 UTC (1 days ago)
(HTM) web link (www.ics.uci.edu)
(TXT) w3m dump (www.ics.uci.edu)
| heinrichhartman wrote:
| Ha! This paper contains the definition of Y-Combinator:
|
| > Y combinator: Y = lt. (lx. t (x x)) (lx. t (x x))
|
| #TIL!
| louthy wrote:
| Which enables recursion
| Akronymus wrote:
| And applying the lambda to itself results in loops, afair.
|
| Edit: It was the Omega operator that did that.
| kmill wrote:
| omega = Y id
|
| where id = lx. x
|
| (though Y Y does not normalize either, infinite looping
| like omega)
| globular-toast wrote:
| 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!
| tromp wrote:
| Some more examples, together with graphical notation:
|
| https://tromp.github.io/cl/diagrams.html
| elric wrote:
| 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.
| selimthegrim wrote:
| 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.
| panzerklein wrote:
| 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
| jumanjisama wrote:
| 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.
| siraben wrote:
| 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
| l-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...
| dgb23 wrote:
| related: https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird
| louthy wrote:
| And the obligatory: https://dkeenan.com/Lambda/
| lisper wrote:
| Factorials in pure lambda calculus:
|
| https://flownet.com/ron/lambda-calculus.html
| benrbray wrote:
| 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....
| ashton314 wrote:
| _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 wrote:
| 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/
| siraben wrote:
| 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.
___________________________________________________________________
(page generated 2021-06-28 23:01 UTC)