Programming with Math | The Lambda Calculus

121,400
0
Published 2024-06-14
The Lambda Calculus is a tiny mathematical programming language that has the same computational power as any language you can dream of. In this video, we'll first explore this calculus before seeing how we can flesh it out into a functional programming language.

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)
  • @eth3792
    The phrase "we know it's correct because it type checks" has blown my mind. I must learn more about Curry-Howard correspondence now
  • @vivada2667
    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."
  • @darqed
    as someone who loves both maths and programming, this is probably my favourite math video I've ever seen
  • @AnOldGreyDog
    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.
  • @AndresFirte
    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
  • 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.
  • @blaz2892
    Lambda Calculus seems like the Functional version of a Turing Machine. Very interesting.
  • @alicagank
    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! :))
  • @Ploofles
    so what your saying is i can write every single python program in one line
  • @codeguru5024
    7:30 "This method...is named currying after the magician Haskell Curry." I'm sure advanced mathematics seems to be magic to some people.
  • @gerocastano8
    As a computer science student that studied functional programming and mathematics, I absolutely love this video. Please keep going!
  • @AlLiberali
    Years of fp propaganda from my friends; And it is this video that finally convinces me it is in fact worth the effort
  • @andrew_ray
    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.
  • @neoplumes
    Wait, this was released 10 days ago? I swear I come back to watch this every 6 months
  • @tjperkins2323
    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.
  • @GlortMusic
    You summed up most of the Theory of Computation, Complexity and Logic course that I attended at university. Kudos to you Eyesomorphic! 👏🏼
  • 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.