David Beazley - Lambda Calculus from the Ground Up - PyCon 2019

"Speaker: David Beazley
These days, programming style guides are all the rage. However, what if your style guide was so restrictive that it only gave you single-argument functions and nothing else? No modules, no classes, no control flow, no data structures, and not even any primitives like integers or regular expressions. Just functions. Could you actually program anything at all? Surprisingly, the answer is yes. In this tutorial, you'll learn how as you work through a ground-up derivation of the lambda calculus in Python.
You will learn nothing practically useful in this tutorial. No packaging. No tools. No libraries. No deployment. No magic Python programming techniques. And certainly learn nothing you would ever want to apply to a real project. You will, on the other hand, have a lot of fun, be completely amazed, and learn some foundational computer science that is a jumping off point for further explorations of functional programming, type theory, programming languages, and more.
Slides can be found at: speakerdeck.com/pycon2019 and github.com/PyCon/2019-slides"

[@TheEntireUniverse]

He should do a tutorial on how to customize his environments to do this stuff.

[@PGouges35]

I live for these tutorials. David Beazley is my personal Jesus

[@CucuExploziv]

I'd compare him to Moses - spliting the fog of your mind!

[@jiamingsun1701]

The talk continues at 1:43:50

[@pahvalrehljkov]

its official, im gonna search whole web for david beazleys videos...

[@m.h.7121]

Yoo, i am not joking at all, David beazley should be nominated as a lord of the python universe. No way the amount of knowledge he has. I am not surprised at all since he started programming at something around 11 years old. What an absolute legend. I always wished i knew programming at an early age of my life. Hopefully, i am still in my 20's. Holy Jesus freak, this guy is the lord of the rings. Anyway, i hope y'all doing great during this shitty pandemic time and shit. Have a good day/night.

[@gpk6458]

Man, this was so much fun to follow along to. I don't think my brain will be done processing this for a while. That kid with the high-pitched voice is very annoying, though.

[@plectro3332]

Hands down best Lambda Calculus tutorial out there

[@malikrumi1206]

"... have a lot of fun, be completely amazed, and learn some foundational computer science that is a jumping off point for further explorations of functional programming..." IS practical and useful !!!

[@SKyrim190]

For some reason his intonation cracks me up!

[@x87-64]

This was totally insane. He is a brilliant teacher.

[@MatthiasBlume]

To me the best way to understand what that R function is goes as follows: Suppose you have some slightly crappy version of factorial, call it crappyfact that only works for arguments 0 ... N for some number N, but not for arguments bigger than N. Then R(crappyfact) returns a slightly improved version of factorial - slightly less crappy, because it will work for arguments up to N+1. The actual perfect fact is a fixpoint of R because R cannot improve it further. As a matter of fact (no pun intended), this fixpoint is the so-called LEAST fixpoint. It is the "least crappy" version of factorial that cannot be further improved by R.

[@thanasiosmetallidis5642]

The most interesting video I have ever seen. With this we can build a whole UNIVERSE starting to define the NOTHING ( The emptyness ). Am I write when I say that the definition of NOTHING is the begin of all there is. And that the execution ( instance ) of NOTHING is the creation of ALL

[@matthewblott]

I've watched the first hour and my mind is blown.

[@freddupont3597]

Have not had so much fun in some time; mind suitably, and delightfully blown! :-) An afternoon well spent, thank you Mr Beazley!

[@cheaterman49]

Some things are really subtle AF: >>> THREE(FOUR)(incr)(0) 64 >>> THREE(FOUR(incr))(0) 12 I got stuck a while when implementing multiplication. It makes a lot of sense but is very hard to wrap your head around!!! EDIT: Explanation (to the best of my understanding...) - in the first case, we're creating a function that will call three times the "call four times" operator so that's 4*4*4 calls applied to the function, while in the second one we're creating a function that will call four times incr and then we call that function three times, so 4+4+4 calls. EDIT2: Also, to the best of my understanding, there's no easy/good way to reuse ADD to implement MUL - but I'd love to be corrected with an example. :-) EDIT3: Well Tenchi below did it :-) I do stand corrected!

[@StefanoBorini]

This lecture broke my brain

[@billcolak5253]

david beazley is my spirit animal.

[@varunpatkar501]

I came here after i failed to solve a codewars question about this topic and now i'm really interested about this

[@x87-64]

You just started the journey into the deepest rabbit hole

[@2xhTenchi]

When following the course and trying to implement things before David shows how to do them, I came up with a multiply that doesn't involve an F and makes more sense to me: MUL = lambda x: lambda y: y(ADD(x))(ZERO) We repeat y times "ADD(x)" to ZERO

[@jlhidalgo]

The "easy" way for me to understand natural numbers in lambda calculus, that makes all this much simpler, is to think that we are defining "once", "twice", "thrice" etc. and using those concepts to represent "one", "two", "three", etc. Then "sum a b" actually means "do a and then do b", as in "do twice and then once more to the result", which equals "do tree times". And "mul" is "do a to b, and then apply it", like in "do twice to twice, and apply that", which equals "do four times". Thus the additional lambda in David's definition of mul is (somehow) obvious.

[@cheaterman49]

Hehehe, I was looking for this, thanks!

[@x87-64]

I came up with the same. We can do Power in a similar way. POW = lambda n: lambda m: m(MUL(n))(ONE)

[@mikelezhnin8601]

The recursion magic broke me.

[@SKyrim190]

That was really insightful, specially the way he described the Y-combinator. It made complete sense. I would suggest anyone who already knows basic lambda calculus to jump to around 2:30:00 though

[@boomiboom3900]

Wuuuuuut This is like the most amazing math thing ive ever seen.

[@oxereviscerator]

Incredible.

[@amelemara4615]

Damn, that's some really out there python.

[@calebgindelberger3046]

I'm almost glad I wasn't there, guessing my yelling "zero is false!" Wouldn't have gone well

[@MatthiasBlume]

Simplification: You don't have to modify ISZERO and you can use the normal TRUE and FALSE. You would still pass thunks as second and third arguments to ISZERO, and then you invoke the thunk at the end after ISZERO returns: lambda n : ISZERO(n)(lambda dummy: ONE)(lambda dummy: MUL(n)(FACT(PRED(n))))(TRUE) (The last TRUE is the dummy argument and could be anything.)

[@DeanLa]

How does he do the code with slide next to it?

[@_intruder]

I've never felt so excited to implement a SUCC, let me tell you.

[@michellethalakottur9328]

awesommeee

[@freddupont3597]

ISZERO(CONS(2)(3)) --> ) too.

[@aaronhall8039]

Very large gap from 1:20:00 to 1:42:00

[@section9999]

anybody know where that mind blown meme is from in the image @1:09:00? Its so common I kind of want to see the original video. Was it for like a mediation guru thing or something like that?

[@mehoyminoy9224]

Tim and Eric's "The Universe"

[@section9999]

@@mehoyminoy9224 Dude awesome, thank you. 😜

[@raghavatreya4533]

Presentation material link??

[@rohithill]

What setup is he using? What is he writing his code in along with presentation?

[@StankyPickle1]

Is it Christmas already?!

[@kurianbenoy9369]

Low audio

[@caballopalido]

WHATEVER GENIUS WAS IN CHARGE OF THE DYNAMIC RANGE OF THIS RECORDING... A CURSE ON YOUR FAMILY

[@allenstevens4216]

As soon as you can build a not gate with a function, you can build all circuits, as soon as you can build all circuits you can build a computer, etc etc etc. I don't know how many people minecraft before, but you can build entire computers that run code and software and decision trees inside the game, with nothing more than a not gates, thousands of them. So.... I'm done screaming at the video... But I see where this is going.

[@calebgindelberger3046]

You get NOR and NAND really early, so full logic is easy and proveable

[@omega82718]

Minecraft is Turing-complete so yeah

[@clementdato6328]

This is not what the video means. When you are talking about binary coding, you talk about an external interpretation of the binary code. In the intrinsic fashion, the ONE defined in there is fundamentally different from the one the you build by stacking up a computer based on the logical gates that he made. The one is the only one, the ONE in that universe. That’s also why the iszero does not work. True False cannot be intrinsically determined. Equality and so on relies on an external interpretation.

[@poojanpatel2437]

that stupid guy at 30:00

[@gpk6458]

He's very annoying all the way through. He's listening to a talk on lambda calculus and how to do logic using nothing but functions and thinks to himself "I wonder if this guy knows about truth tables?" Something you learn in day one of computer science...

[@cronaut5429]

I don't remember the last time I actually wanted to punch someone in the face, but, somehow, he evoked this feeling in me without me ever seeing that face.

[@MrHaste12]

@@gpk6458 The way he comments on every single thing is like he thinks he's got a private lesson with Beazley

[@amyfalconer1660]

@@MrHaste12 That guy is killing me right now. His commentary totally breaks the flow. I'm not trying to be mean, as I'm sure he'd feel awful reading this, but geez louise.

[@sssveny]

He’s so rude at 1:51:10 basically saying “i don’t find this interesting, can you move on?”

[@jeffschlarb4965]

github.com/PyCon/2019-slides is 404

[@jungjunk1662]

He is confused a bit

[@CrapE_DM]

That's not how an electrical switch works... The middle one supplies the power, and the switch decides which of the two sides receives the power.

[@crimsun7186]

That's only if the switch is a SPDT switch. What David is probably thinking of a SPST switch, which only has two contacts.