Programming with Math | The Lambda Calculus

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.
Background music: 'Reminisce', composed by Caleb Peppiatt.

― Further Reading ―

Types and Programming Languages, by Benjamin C. Pierce (Book)

― Corrections ―

At 4:35, the word 'comptuter' should obviously be 'computer', sorry about that!

An entry to #SoMEPi

[eth]

The phrase "we know it's correct because it type checks" has blown my mind. I must learn more about Curry-Howard correspondence now

[vivada]

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.

[little-ork]

halfway through the video I suddenly understood Haskell

[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

[AlLiberali]

Years of fp propaganda from my friends; And it is this video that finally convinces me it is in fact worth the effort

[neoplumes]

Wait, this was released 10 days ago? I swear I come back to watch this every 6 months

[himanshutripathi]

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.

[tjperkins]

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.

[tessimago]

that's nice, now print "hello world"

[blaz]

Lambda Calculus seems like the Functional version of a Turing Machine. Very interesting.

[codeguru]

7:30 "This method...is named currying after the magician Haskell Curry." I'm sure advanced mathematics seems to be magic to some people.

[Ploofles]

so what your saying is i can write every single python program in one line

[amritawasthi]

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.

[gerocastano]

As a computer science student that studied functional programming and mathematics, I absolutely love this video. Please keep going!

[shadamethyst]

11:00 - "there aren't any y in M"
If only Coq would accept this as a proof every time this one detail comes up...

[joaoguerreiro]

We need more channels like this. Great Computer Science content mate!! Instant subscribe 🙏🏼

[GlortMusic]

You summed up most of the Theory of Computation, Complexity and Logic course that I attended at university. Kudos to you Eyesomorphic! 👏🏼

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