Church's λ-Calculus (2023) [pdf] • Hacker News Board

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

#41

Post by tombert » Sat, Apr 20, 2024, 4:20 PM UTC

andoando wrote: post #25

tombert wrote: post #22

Earlier quoted context omitted.

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.

The PhD I was doing was in formal methods, specifically in regards to timing semantics. I think it’s super neat, but sadly I am in a minority.

ML is cool but I was never able to get super into it. I use ChatGPT but I never had a ton of desire to get into the guts of it. I was always more interested in discrete math and formal logic.

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

#42

Post by agumonkey » Sat, Apr 20, 2024, 4:24 PM UTC

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 Y combinator (npi) was also a very mind opening exercise. Even recreating pairs was quite fun.

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

#43

Post by mindcrime » Sat, Apr 20, 2024, 4:25 PM UTC

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.

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

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

#44

Post by richk449 » Sat, Apr 20, 2024, 6:05 PM UTC

keybored wrote: post #37

tombert wrote: post #17

Earlier quoted context omitted.

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…

An unwelcome comparison: For certain people you can’t just teach Buddhist meditation using Buddhist terminology and context because that’s “woo”. However if you dress it up in vaguely “neuroscience” terms then it’s fine. And preferably you have some scientific studies at hand to prove that meditation has an effect. (Although no one demands biomechanic studies from their intro tennis teacher.) Compare with all the moa…

Interesting point. One difference:

It is easy to tell if a tennis instructor is giving “good” instruction, where good means instructions that help you be a better tennis player. You just look at their students. If you want to know if they give good fundamentals for long term growth, you look at their much older students.

How do you know if a meditation teacher is giving good instructions? Seems much harder to me.

It is interesting that many of the traditional religions have hard to quantify benefits. Buddhism offers a personal inward help, and the abrahamic religions often benefit communities.

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

#45

Post by xanderlewis » Sat, Apr 20, 2024, 8:47 PM UTC

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.

By the way: logicians sometimes pedantically draw a distinction between ‘recursion’ and ‘induction’: induction is for proving things; recursion is for defining things.

And it’s not just terminological: the difference becomes very important when you realise one needs to prove that recursion is possible (that is, function definitions by recursion on a well-ordered set are well-defined) by induction. So one actually comes logically before the other.

I guess to truly determine whether they’re distinct concepts you’d have to exhibit some model of set theory that supports recursion but not induction, or something. But that’s beyond me.

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

#46

Post by andoando » Sat, Apr 20, 2024, 11:41 PM UTC

tombert wrote: post #41

andoando wrote: post #25

Earlier quoted context omitted.

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.

The PhD I was doing was in formal methods, specifically in regards to timing semantics. I think it’s super neat, but sadly I am in a minority. ML is cool but I was never able to get super into it. I use ChatGPT but I never had a ton of desire to get into the guts of it. I was always more interested in discrete math and formal logic.

That sounds interesting, can you tell me a bit more? What does formal methods in regards to timing semantics mean?

Im in the same boat. I like abstract logic/math and ML never caught much of my interest.

I want to start applying but Im not even sure how to find departments that would fit what Im looking for. Maybe I need to take this more seriously and start reading papers and self study.

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

#47

Post by DrFalkyn » Sun, Apr 21, 2024, 5:05 AM UTC

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.

Neural networks seem more linear algebra than calculus

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

#48

Post by eddd-ddde » Tue, Apr 23, 2024, 3:50 AM UTC

DrFalkyn wrote: post #47

eddd-ddde wrote: post #14

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.

Neural networks seem more linear algebra than calculus

Yeah it's also lots of linear algebra. Which also reminds me, graphics programming? Linear algebra everywhere.