10 ms·

Church's λ-Calculus (2023) [pdf]

155 points by jstrieb 2y ago

ashton314 2y ago
I've got Harper's Practical Foundations for Programming Languages and it's a great book—he writes clearly and succinctly. Knowing the lambda calculus helped me one time when I was working as a software engineer: I had just added functions to a little DSL interpreter that was going to make it easy to customize behavior of our product to different customers. (It wasn't ever going to be used by customers directly; it was primarily a tool for the internal team.) It was at this point that I realized we needed some kind of execution time-out: since we could encode functions, we could write down e.g. the Y combinator or the omega combinator and we could get non-terminating programs in this DSL. Now I work as a programming languages researcher, so the lambda calculus has direct application to my day job. Those curious might be interested in ISWIM, [1,2] which is an extension of the lambda calculus with an arbitrary set of operators. Like the lambda calculus, this is an abstract language. However, you can add numbers and other operators, and ISWIM-like languages are often used to illustrate new ideas in programming languages. Syntax is incidental. Boil the syntax away from languages and reduce them to their distilled semantics to get out the essential differences—this is the kind of thing that the lambda calculus makes easy. I highly recommend reading Landin's The Next 700 Programming Languages [2] as it is a great, short, clear read. [1]: https://en.wikipedia.org/wiki/ISWIM https://en.wikipedia.org/wiki/ISWIM [2]: https://www.cs.cmu.edu/~crary/819-f09/Landin66.pdf https://www.cs.cmu.edu/~crary/819-f09/Landin66.pdf
- trueismywork 2y ago
  Can you read Harpers book without knowing lambda calculus?
  - rkrzr 2y ago
    You can learn the lambda calculus in a few hours. If you read just the first page of the linked paper and work through a few examples, you will likely already know enough about it to read the book. It's really just like equational reasoning in mathematics.
- JonChesterfield 2y ago
  It appears there are a few like the opening post, e.g. https://www.cs.cmu.edu/~rwh/courses/oplss/tlc-semeq.pdf https://www.cs.cmu.edu/~rwh/courses/oplss/tlc-semeq.pdf. This suggests the book will be worth the time, thank you for mentioning it.
an-allen 2y ago
When I took Fundamentals of Programming Languages 20 years ago - I nearly failed the class. Lambda calculus was simply too esoteric for me to appreciate and much less understand intuitively. Fast forward 20 years, and I see the fundamentals of Alonzo Church’s system in every computation problem I encounter. It’s one of those concepts that age like wine. The only other concept I put on the same level is Shannons “informational entropy” and maybe Wolfram’s Ruliad.
- _delirium 2y ago
  It's kind of interesting that the history is in the order it is. I could completely imagine it being reversed: first, 1000 programming languages are invented, then later, in an attempt to put order to this madness, and understand whether some of them are in a fundamental sense equivalent to others or not, you invent minimalist languages like Turing machines or the lambda calculus, and start developing a theory of reductions. Kind of odd that the Turing machines and lambda calculus predate almost all the others! I mean there are good reasons for it, especially if you try to put yourself in a 1930s mathematics mindset (which is why it actually happened that way), but it is, I'd submit, a bit surprising to learn from a 2020s perspective if you didn't already know it.
  - andoando 2y ago
    Interesting thought. Perhaps we'll discover a language that is in some way of higher order than Turing complete.
    - Zambyte 2y ago
      There are certain concurrent properties that cannot be modeled with a Turing machine: https://en.wikipedia.org/wiki/Unbounded_nondeterminism https://en.wikipedia.org/wiki/Unbounded_nondeterminism There is also a very interesting intersection between the history of the Actor Model and Lambda Calculus: https://research.scheme.org/lambda-papers/ https://research.scheme.org/lambda-papers/
    - mindcrime 2y ago
dexwiz 2y ago
There has to be some programmer rite of passage involving learning lambda calculus. I went through this a few years ago when something similar was posted. I learned the notation, marveled at its dual simplicity and completeness, and and did a few exercises. But I came out the other side none the wiser. I think I was looking for some great epiphany on the nature of computation. Alas, it eluded me in the end. It was fun but ultimately useless for me.
- somat 2y ago
  You will probably be wanting unlambda then. an implementation of the lambda calculus without the lambda forms. http://www.madore.org/~david/programs/unlambda/ http://www.madore.org/~david/programs/unlambda/
- tombert 2y ago
  I love theory, and I also really like lambda calculus, but I feel like this sentiment applies to most theory, particularly stuff after undergrad. I spent a not-insignificant amount of time learning how to do proofs with Isabelle. I learned a lot about inductive proofs, set theory, meta-logic, and challenged myself to prove a lot of the stuff I had previous taken for granted (e.g. proving that different sorts refine each other). I enjoyed it, and similarly was convinced that this was going to be some life-changing thing that changes my career trajectory and... Nothing changed. No one in charge of companies gives a shit about theory. They all claim that they love theory, they claim that they are very research focused, they claim that they value all the time you spent learning this stuff, but in reality they really just want you to change the color of buttons, or change the format of dates, or add a field to a JSON. It sometimes feels like no software engineer but me actually wants to learn any math, and will refuse to touch anything even resembling it. And I'm not picking on Isabelle here; I've had similar results trying to pitch TLA+ and Coq and Agda for some of the more error-prone parts of the codebase, with different sales-pitches, and without fail the managers will always say that they "will look into it", and promptly do absolutely nothing. The first two times a manager said that, I believed them, but after that I realized that they're just trying to shut me up and tell me "no" politely. It was enough to depress me, and it still kind of does. I still think learning stuff for fun is worth it, but I'd be lying if I told you if I knew why.
renonce 2y ago
One invention that drew me to this topic was Binary Lambda Calculus, invented by John Tromp (“Tromp” as in Tromp-Taylor Rules). It’s just a direct binary encoding of a lambda calculus term, but it gives you a concrete and concise representation which is useful for evaluating the complexity of an expression. I encountered it when viewing https://codegolf.stackexchange.com/questions/6430/shortest-terminating-program-whose-output-size-exceeds-grahams-number https://codegolf.stackexchange.com/questions/6430/shortest-t... and found that this language was the one that could write the most precise representation of a very large number with the fewest bits possible. I later learned that Graham’s number could be encoded in 120 bits (maybe 3~4 less), much more concise than equivalent mathematical language, and I’ve since been drawn into the field of googology. It was fascinating.
- tromp 2y ago
  That Stack Exchange thread shows you can exceed Graham's number with the 49 bit lambda term (λ 1 1) (λ 1 (1 (λ λ 1 2 (λ λ 2 (2 1))))), or graphically ┬─┬ ┬─┬────────── └─┤ │ │ ──┬────── │ │ │ ┬─┼────── │ │ │ └─┤ ┬─┬── │ │ │ │ ┼─┼─┬ │ │ │ │ │ ├─┘ │ │ │ │ ├─┘ │ │ │ ├─┘ │ │ ├───┘ │ ├─┘ └─┘ Related: https://oeis.org/A333479 https://oeis.org/A333479
  - renonce 2y ago
    Yeah but it’s not representing a known number - I would rather say it is a proof that the busy beaver function for BLC at 49 bits is higher than Graham’s number. The fact that it represents known numbers concisely is more interesting to me.
    - tromp 2y ago
      Then you'll be more interested in the 114 bit representation (λ (λ 2 1 (λ 1 (λ λ 1 2 (λ 1)) (λ λ 5 (2 1)) 3) 1) (λ λ 2 (3 2 1))) (λ λ 2 (2 (2 1))) of Graham's number [1]. [1] https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/graham.lam https://github.com/tromp/AIT/blob/master/fast_growing_and_co...

155 points by jstrieb 2y ago

I've got Harper's Practical Foundations for Programming Languages and it's a great book—he writes clearly and succinctly. Knowing the lambda calculus helped me one time when I was working as a software engineer: I had just added functions to a little DSL interpreter that was going to make it easy to customize behavior of our product to different customers. (It wasn't ever going to be used by customers directly; it was primarily a tool for the internal team.) It was at this point that I realized we needed some kind of execution time-out: since we could encode functions, we could write down e.g. the Y combinator or the omega combinator and we could get non-terminating programs in this DSL. Now I work as a programming languages researcher, so the lambda calculus has direct application to my day job. Those curious might be interested in ISWIM, [1,2] which is an extension of the lambda calculus with an arbitrary set of operators. Like the lambda calculus, this is an abstract language. However, you can add numbers and other operators, and ISWIM-like languages are often used to illustrate new ideas in programming languages. Syntax is incidental. Boil the syntax away from languages and reduce them to their distilled semantics to get out the essential differences—this is the kind of thing that the lambda calculus makes easy. I highly recommend reading Landin's The Next 700 Programming Languages [2] as it is a great, short, clear read. [1]: https://en.wikipedia.org/wiki/ISWIM https://en.wikipedia.org/wiki/ISWIM [2]: https://www.cs.cmu.edu/~crary/819-f09/Landin66.pdf https://www.cs.cmu.edu/~crary/819-f09/Landin66.pdf

trueismywork 2y ago
Can you read Harpers book without knowing lambda calculus?
- rkrzr 2y ago
  You can learn the lambda calculus in a few hours. If you read just the first page of the linked paper and work through a few examples, you will likely already know enough about it to read the book. It's really just like equational reasoning in mathematics.
JonChesterfield 2y ago
It appears there are a few like the opening post, e.g. https://www.cs.cmu.edu/~rwh/courses/oplss/tlc-semeq.pdf https://www.cs.cmu.edu/~rwh/courses/oplss/tlc-semeq.pdf. This suggests the book will be worth the time, thank you for mentioning it.

an-allen 2y ago

When I took Fundamentals of Programming Languages 20 years ago - I nearly failed the class. Lambda calculus was simply too esoteric for me to appreciate and much less understand intuitively. Fast forward 20 years, and I see the fundamentals of Alonzo Church’s system in every computation problem I encounter. It’s one of those concepts that age like wine. The only other concept I put on the same level is Shannons “informational entropy” and maybe Wolfram’s Ruliad.

_delirium 2y ago
It's kind of interesting that the history is in the order it is. I could completely imagine it being reversed: first, 1000 programming languages are invented, then later, in an attempt to put order to this madness, and understand whether some of them are in a fundamental sense equivalent to others or not, you invent minimalist languages like Turing machines or the lambda calculus, and start developing a theory of reductions. Kind of odd that the Turing machines and lambda calculus predate almost all the others! I mean there are good reasons for it, especially if you try to put yourself in a 1930s mathematics mindset (which is why it actually happened that way), but it is, I'd submit, a bit surprising to learn from a 2020s perspective if you didn't already know it.
- andoando 2y ago
  Interesting thought. Perhaps we'll discover a language that is in some way of higher order than Turing complete.
  - Zambyte 2y ago
    There are certain concurrent properties that cannot be modeled with a Turing machine: https://en.wikipedia.org/wiki/Unbounded_nondeterminism https://en.wikipedia.org/wiki/Unbounded_nondeterminism There is also a very interesting intersection between the history of the Actor Model and Lambda Calculus: https://research.scheme.org/lambda-papers/ https://research.scheme.org/lambda-papers/
  - mindcrime 2y ago

dexwiz 2y ago

There has to be some programmer rite of passage involving learning lambda calculus. I went through this a few years ago when something similar was posted. I learned the notation, marveled at its dual simplicity and completeness, and and did a few exercises. But I came out the other side none the wiser. I think I was looking for some great epiphany on the nature of computation. Alas, it eluded me in the end. It was fun but ultimately useless for me.

somat 2y ago
You will probably be wanting unlambda then. an implementation of the lambda calculus without the lambda forms. http://www.madore.org/~david/programs/unlambda/ http://www.madore.org/~david/programs/unlambda/
tombert 2y ago
I love theory, and I also really like lambda calculus, but I feel like this sentiment applies to most theory, particularly stuff after undergrad. I spent a not-insignificant amount of time learning how to do proofs with Isabelle. I learned a lot about inductive proofs, set theory, meta-logic, and challenged myself to prove a lot of the stuff I had previous taken for granted (e.g. proving that different sorts refine each other). I enjoyed it, and similarly was convinced that this was going to be some life-changing thing that changes my career trajectory and... Nothing changed. No one in charge of companies gives a shit about theory. They all claim that they love theory, they claim that they are very research focused, they claim that they value all the time you spent learning this stuff, but in reality they really just want you to change the color of buttons, or change the format of dates, or add a field to a JSON. It sometimes feels like no software engineer but me actually wants to learn any math, and will refuse to touch anything even resembling it. And I'm not picking on Isabelle here; I've had similar results trying to pitch TLA+ and Coq and Agda for some of the more error-prone parts of the codebase, with different sales-pitches, and without fail the managers will always say that they "will look into it", and promptly do absolutely nothing. The first two times a manager said that, I believed them, but after that I realized that they're just trying to shut me up and tell me "no" politely. It was enough to depress me, and it still kind of does. I still think learning stuff for fun is worth it, but I'd be lying if I told you if I knew why.

renonce 2y ago

One invention that drew me to this topic was Binary Lambda Calculus, invented by John Tromp (“Tromp” as in Tromp-Taylor Rules). It’s just a direct binary encoding of a lambda calculus term, but it gives you a concrete and concise representation which is useful for evaluating the complexity of an expression. I encountered it when viewing https://codegolf.stackexchange.com/questions/6430/shortest-terminating-program-whose-output-size-exceeds-grahams-number https://codegolf.stackexchange.com/questions/6430/shortest-t... and found that this language was the one that could write the most precise representation of a very large number with the fewest bits possible. I later learned that Graham’s number could be encoded in 120 bits (maybe 3~4 less), much more concise than equivalent mathematical language, and I’ve since been drawn into the field of googology. It was fascinating.

tromp 2y ago
That Stack Exchange thread shows you can exceed Graham's number with the 49 bit lambda term (λ 1 1) (λ 1 (1 (λ λ 1 2 (λ λ 2 (2 1))))), or graphically ┬─┬ ┬─┬────────── └─┤ │ │ ──┬────── │ │ │ ┬─┼────── │ │ │ └─┤ ┬─┬── │ │ │ │ ┼─┼─┬ │ │ │ │ │ ├─┘ │ │ │ │ ├─┘ │ │ │ ├─┘ │ │ ├───┘ │ ├─┘ └─┘ Related: https://oeis.org/A333479 https://oeis.org/A333479
- renonce 2y ago
  Yeah but it’s not representing a known number - I would rather say it is a proof that the busy beaver function for BLC at 49 bits is higher than Graham’s number. The fact that it represents known numbers concisely is more interesting to me.
  - tromp 2y ago
    Then you'll be more interested in the 114 bit representation (λ (λ 2 1 (λ 1 (λ λ 1 2 (λ 1)) (λ λ 5 (2 1)) 3) 1) (λ λ 2 (3 2 1))) (λ λ 2 (2 (2 1))) of Graham's number [1]. [1] https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/graham.lam https://github.com/tromp/AIT/blob/master/fast_growing_and_co...