Programming with Math | The Lambda Calculus
121,400
Published 2024-06-14
After a brief tour of a simple type system, we'll see why the Lambda Calculus has some surprising applications in the field of mathematical logic, and how the implications of this relationship could alter the way that we study mathematics forever.
― Timestamps ―
0:00 - Intro
0:42 - Definition
5:30 - Multiple Inputs
8:10 - Booleans and Conditionals
13:11 - Simple Types
16:32 - Curry-Howard Correspondence
20:58 - Outro
― Credits ―
All animation and voiceover created by Eyesomorphic.
Lean4 proof of infinitude of primes taken from mathlib4 under Apache 2.0 license: github.com/leanprover-community/mathlib/blob/maste…
Background music: 'Reminisce', composed by Caleb Peppiatt.
― Further Reading ―
Types and Programming Languages, by Benjamin C. Pierce (Book)
Category Theory and Why We Care, by Eyesomorphic (Lecture series): • Category Theory and Why We Care
― Corrections ―
At 4:35, the word 'comptuter' should obviously be 'computer', sorry about that!
An entry to #SoMEPi
All Comments (21)
-
The phrase "we know it's correct because it type checks" has blown my mind. I must learn more about Curry-Howard correspondence now
-
This video is super good. Multiple times throughout the video, I was like "ok this does not make any sense" and then immediately after saying that, you said "That seems confusing. Let's look at an example."
-
as someone who loves both maths and programming, this is probably my favourite math video I've ever seen
-
One of the things I took away from reading Gödel, Escher, Bach (mumble, mumble) years ago was that computer languages don't differ in their ability only in their expressiveness . In other words, any language (of at least λ-calculus complexity) can do what any other language can. It's just easier to express in some.
-
This video is amazing! I encourage everyone to watch the video, and then grab a pen and paper and rewatch the video, trying to get ahead of what is being shown. I tried that and realized that I hadn’t actually understood many of the things in the video, like the notation. Videos like these are so well explained that you often feel like you understood everything. But then when you grab pen and paper you realize that there’s many details that you missed. And by the end of it, you feel like you truly understood 90% of it
-
halfway through the video I suddenly understood Haskell
-
This is why i pay for internet. Thank you very much. I did not pay much attention in class , but if the class was explained like this it would have been awesome.
-
Lambda Calculus seems like the Functional version of a Turing Machine. Very interesting.
-
I’m a linguist, not particularly mathematically inclined, and honestly, I can’t believe I understood half of it. Incredibly simple yet intuitive. I love the visuals too! Please keep up the good work! :))
-
so what your saying is i can write every single python program in one line
-
7:30 "This method...is named currying after the magician Haskell Curry." I'm sure advanced mathematics seems to be magic to some people.
-
As a computer science student that studied functional programming and mathematics, I absolutely love this video. Please keep going!
-
Years of fp propaganda from my friends; And it is this video that finally convinces me it is in fact worth the effort
-
And if you've ever had the privilege of writing Haskell code, it uses the same kind of type checker using an algorithm developed by Milner and Hindley to prove that your program is 100% type-safe, which actually means that if your code compiles, there's a decent chance it's correct. And if it's not, then your toe definitions aren't robust enough.
-
Wait, this was released 10 days ago? I swear I come back to watch this every 6 months
-
Great timing! I've always wanted to share this with my friends but I find it extremely hard to explain. It's nice that you made it accessible to others without much experience in math.
-
You summed up most of the Theory of Computation, Complexity and Logic course that I attended at university. Kudos to you Eyesomorphic! 👏🏼
-
that's nice, now print "hello world"
-
Alice is so obsessed with Java.
-
I knew about your channel since I watched the videos about category theory. I don't know how i didnt subscribe this channel. This video popped up and i was amazed by it. It's so wonderful in all sense. I watched this and saw that I hadn't subscribed to this channel.