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

21–30 of 48 posts

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

#21

Post by JonChesterfield »

ashton314 wrote: post #2

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…

It appears there are a few like the opening post, e.g. 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.

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

#22

Post by tombert »

andoando wrote: post #19
tombert wrote: post #8

Earlier quoted context omitted.

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.

From experience, that has its own share of frustrations as well. You get to work in theory and that’s fun, but if you decide to do a PhD while also working a desk job, I recommend you do not tell your employers.

I made the mistake of telling an employer, and whenever I made any mistake in my work, no matter how small, the employer would immediately say that the PhD work is distracting me, and my focus not BigCo.

My PhD is on an indefinite hiatus right now, because it’s something I am questioning the utility of right now.

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

#23

Post by dexwiz »

andoando wrote: post #18
DonaldPShimoda wrote: post #13

Earlier quoted context omitted.

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.

Turning was Church’s student.

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

#24

Post by yobbo »

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.

Those things are not equivalent.

But schools typically teach these things as a "theory part" and as "practice/application part" (for example by "syncing/sequencing" courses if possible) which helps with both relevance and "getting it".

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

#25

Post by andoando »

tombert wrote: post #22
andoando wrote: post #19

Earlier quoted context omitted.

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.

From experience, that has its own share of frustrations as well. You get to work in theory and that’s fun, but if you decide to do a PhD while also working a desk job, I recommend you do not tell your employers. I made the mistake of telling an employer, and whenever I made any mistake in my work, no matter how small, the employer would immediately say that the PhD work is distracting me, and my focus not BigCo. My P…

That sucks. I cant imagine trying to work a job and do a phd at the dame time. That would take out any joy of it for me.

I can definitely see a lot of utility depending on what you do research in. I bet a lot of ML doctoretes are making big bucks, but that's relatively niche.

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

#26

Post by tromp »

renonce wrote: post #16

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

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

#27

Post by thesz »

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

Before LC there were combinators [1].

[1] https://en.wikipedia.org/wiki/Combinatory_logic

These are even more primitive.

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

#28

Post by tromp »

dexwiz wrote: post #23
andoando wrote: post #18

Earlier quoted context omitted.

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.

Turning was Church’s student.

It's amazing how often Turing gets miss-spelled as Turning. Is that because of overzealous spell checkers?

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

#29

Post by Zambyte »

andoando wrote: post #20
_delirium wrote: post #12

Earlier quoted context omitted.

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.

There are certain concurrent properties that cannot be modeled with a Turing machine: 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/

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

#30

Post by NotCamelCase »

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…

Funny that you bring this up -- I feel exactly the same way and I even had more math background than average SW person.

Being on the engineering side of things without much knowledge/focus on programming languages theory and the mathematical nature of computation, one feels as if all the niceties we have in popular PLs are just laws of nature that we just had to discover, whereas in reality they too had to be derived, tried, improved first. But then you study something like this and expect to be able to finally connect the dots and yet, it's still not immediately obvious how we arrived here!

Post reply on HN