31–40 of 48 posts
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 wa…
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 fu…
The "utility" of the lambda calculus, in my opinion, comes down to Church's original choice of terminology. He did not call the things denoted by lambda "functions"; rather, they were abstractions . What makes the lambda calculus so cool is that it lets us see that abstraction is the root of all computation, at least through one perspective (as opposed to the Turing point of view). Learning the lambda calculus direct…
Earlier quoted context omitted.
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 e…
I did a lot of math before I began learning programming. This was my experience: Recursion? Oh you mean proof by induction? Cryptography? Oh you mean number theory? Neural networks? Oh you mean calculus? Almost everything I learn while programming can be associated with some theory I learnt before for math.
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-t... and found that th…
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
Earlier quoted context omitted.
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
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.
[1] https://github.com/tromp/AIT/blob/master/fast_growing_and_co...
Earlier quoted context omitted.
I did a lot of math before I began learning programming. This was my experience: Recursion? Oh you mean proof by induction? Cryptography? Oh you mean number theory? Neural networks? Oh you mean calculus? Almost everything I learn while programming can be associated with some theory I learnt before for math.
That's kind of what annoys me though; it's almost like the word "math" is toxic to people. When I try explaining a correspondence between something that they're doing via code, and how maybe learning a bit of the mathematics behind it might be useful, people kind of just roll their eyes, acting like I asked them to go get three PhDs, and acting like it's just one of those weird "Tombert things". I don't know anything…
Compare with all the moaning and complaining that comes from some people when you talk about functional programming and how it might relate to computer science.[1] Then you might have a better chance inventing ad hoc words for basics like “map” (preferably very prosey) and claiming that Martin Fowler invented it.
[1] This goes triply for anything having to do with proofs, at least proof software associated with FP.
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 wa…
Can you read Harpers book without knowing lambda calculus?
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.
Earlier quoted context omitted.
I did a lot of math before I began learning programming. This was my experience: Recursion? Oh you mean proof by induction? Cryptography? Oh you mean number theory? Neural networks? Oh you mean calculus? Almost everything I learn while programming can be associated with some theory I learnt before for math.
See also: https://en.wikipedia.org/wiki/Curry-Howard_correspondence