Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

cs.cmu.edu

Post reply on HN
Print view View original

11–20 of 48 posts

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

#11

Post by mjh2539 »

dexwiz wrote: post #4

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…

I used it in a graduate course on formal semantics (https://www.wiley.com/en-us/Semantics+in+Generative+Grammar-... after I graduated I wanted to learn how to program so I googled "lambda calculus programming language" and found Haskell. That was ten years ago. Though I rarely use Haskell anymore, the lambda calculus still holds a special place.

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

#12

Post by _delirium »

an-allen wrote: post #3

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 “info…

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.

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

#13

Post by DonaldPShimoda »

dexwiz wrote: post #4

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 directly will allow you to appreciate functions ("abstractions") and use them more effectively; you can reason about their computation and composition.

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

#14

Post by eddd-ddde »

tombert wrote: post #6
dexwiz wrote: post #4

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…

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.

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

#15

Post by catgary »

jvanderbot wrote: post #10
tombert wrote: post #6

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 use the deep theory experience a ton when designing software or systems. But I don't do an actual proof hardly ever. Being able to reason about a problem and intuit the extent of what's technologically possible to solve is insanely useful. But in most places that I work everyone around me can do that too, so we're constantly battling program managers and C suite guys / gals who just don't see why everything is so s…

Yeah, I’m currently an ML scientist but I regularly run into shit where I have no clue how you’d solve the problem without having a compilers/functional programming background.

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

#16

Post by renonce »

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

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

#17

Post by tombert »

eddd-ddde wrote: post #14
tombert wrote: post #6

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.

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 about neural networks yet (though I really need to get on that), but I have noticed the other two examples you mentioned as well; recursion is more or less applied inductive proofs, a lot of crypto boils to number theory.

My dream is to some day convince a manager to give me budget to spend a few weeks designing a new system and proving correctness with TLA+. I'm not saying it's terribly likely, but a man can dream.

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

#18

Post by andoando »

DonaldPShimoda wrote: post #13
dexwiz wrote: post #4

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…

I dont quite think of functions and abstractions as the same. Abstractions seem to do more with having a self referential property. Though I suppose that can be seen as the identity function f->f.

IIRC Church was heavily influenced by Turing and vice versa.

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

#19

Post by andoando »

tombert wrote: post #8
hnoyrnndd wrote: post #7

Earlier quoted context omitted.

A friend of mine worked at Rockwell Collins and wrote proofs, and theorem provers, all day. If you work on webshit like me you won’t get to use these skills much. (On the other hand, recursing over the structure of JSON-like data often feels like 80% of the job, so I think the skills come into play at least a tiny bit).

I work on web-adjacent-shit, mostly data processing stuff in Kafka that eventually ends up on the web. I don't get to recurse over JSON, occasionally I get to design a system from scratch and that's more fun, but it's usually not more complicated than "draw boxes that point to other boxes and/or cylinders on screen". Sometimes I draw a picture of cloud. I like my job just fine, it's a decent job, and I like my manage…

Yeah I am at the same place. Considering going for a phd because at this point I cant muster any kind of interest in corporate tech.

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

#20

Post by andoando »

_delirium wrote: post #12
an-allen wrote: post #3

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 “info…

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 red…

Interesting thought. Perhaps we'll discover a language that is in some way of higher order than Turing complete.
Post reply on HN