Programming with Math | The Lambda Calculus

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

[@tylerfusco7495]

if you want to go really far into it, look into languages with this taken to the logical extreme, like Lean4. people have written a huge amount of math as code, and *the fact that it type checks* means that all of those proofs are correct.

[@warmooze]

Absolutely insane

[@MrSamwise25]

Just a warning: the treatments I've seen of the CH correspondence (e.g. Girard's Proofs and Types) have either been frustrating in key technical points or too vague to get a deep understanding. This isn't to dissuade you, but to reassure you that it isn't you, it's the text.

[@MrSamwise25]

What's your favorite first-order logic system? Mine is Fitch-style proofs, and I found it easier to just go through the correspondence myself with that system.

[@jawad9757]

wait until you hear about dependently typed programming languages

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

[@Eyesomorphic]

That's very reassuring, I'm glad you enjoyed it :)

[@darqed]

as someone who loves both maths and programming, this is probably my favourite math video I've ever seen

[@sadsongs7731]

I mean, to claim that Lambda calculus can replace any programming language is like saying assembly can replace any programming language. True in theory but GOOD LUCK trying to get anywhere.

[@tylerfusco7495]

@@sadsongs7731 i mean, thats literally what functional programming languages are. Lisp, Haskell, OCaML, Lean, Clojure, etc. Are all pretty widely used, and are literally built on top of nothing but lambda calculus (but in practice are optimized or compiled to speed up evaluation).

[@sadsongs7731]

@@tylerfusco7495 Those languages offer far more conveniences than what lambda calculus notation provides. They may be "built on top of" but they are not just lambda calculus. That was my point with assembly. You technically don't need anything else, but it's a pain in the behind to write compared to a higher level programming language. These languages offer abstractions that take time to learn and, sure, would be better if you didn't have to learn them but they are there because raw lambda, like raw assembly, is not user friendly.

[@tylerfusco7495]

@@sadsongs7731 well yeah, nobody is advocating for lambda calculus being the actual thing you program in. that's like thinking a video outlining how assembly language works is advocating for assembly language to replace higher level languages. that's not the point, the point is that the higher level abstractions can all be built on top of and formalized using the lower level ones.

[@Darkon10199]

if you love both math and cs i really recommend type theory. it's the math field that studies this stuff, lambda calculus is the starting point, but it's some of the most beautiful and groundbraking math i've ever studied

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

[@anywallsocket]

Yeah cuz λ calc is Turing complete, so it’s complexity is sufficient to simulate any normal computation, including the simulation of any other computer.

[@writerightmathnation9481]

Complexity is not the same as effectiveness. Some languages are faster because of their expressiveness, and others are slower because of the design of their use of their expressive power.

[@anywallsocket]

@@writerightmathnation9481 i believe that was OP's point, you just said it differently. no one is saying complexity == effectiveness

[@SL3DApps]

This isn’t true. A language ability is highly different when used for certain areas in computing. However, If you’re only interested in making simple programs then you won’t ever have to worry.

[@cinderwolf32]

​@@SL3DApps things like I/O, direct memory access, network access, etc don't count here. This video, and the comment you're replying to, are about computation, not making programs and apps. Computation does not care about these things, and studying it takes place in an imaginary world with infinite memory and infinite time. In that case, Scratch and C are equivalent. If you're seriously unconvinced, consider that someone has successfully emulated a RISC machine in Scratch and used it to boot Linux all within the project.

[@yaksher]

@2:30 I like how this presented as some sort of obvious improvement over writing an arrow even though it's more visual noise and more characters.

[@Anonymous-df8it]

I wonder what the programming language would look like if the arrow was preserved

[@yaksher]

@@Anonymous-df8it This is what languages like Ocaml do.

[@ScottHess]

In a regular computer system, using . is a lot easier than using an arrow. Of course, the notation also added lambda at that point, so no gains had…

[@yaksher]

@@ScottHess Yeah, I mean, you can do that, but somehow virtually no language does, probably because it's much worse for legibility. Even haskell which does use a \ or lambda then uses an arrow, though you're right that it's less convenient to type than a dot. I think in practice, Rust's solution of using |args| is one of the better ones in terms of typing ergonomics

[@0LoneTech]

@@yaksher Fun fact; Emacs VHDL mode binds ,, and .. to arrows left and right () to make them easier to type. Programming editors tend to have such capabilities. As for typing ergonomics, you might be horrified at the contortions programmers in countries where the leading language isn't English get to do. []{}\|@$ˆˋ are distinctly not easy to type e.g. with a standard Swedish/Finnish layout.

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

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

[@Eyesomorphic]

That is quite the compliment, thank you!

[@CTimmerman]

@@Eyesomorphic As a Python fan, I still prefer Python's readability to Lisp and math. AND and NOT gates are more intuitive to me than strange symbol transformations with formulas i never learned.

[@voltydequa845]

No way! This video, although valid, has nothing to do with the (added) value of FP. This video wouldn't have contributed to your appreciation of the FP if you didn't already knew about FP. It happens because too many FP zealots fail to explain it in a linear and axiomatic way. For example FP helps abstraction, but too many of them fail to abstract being obsessed by side-effects, purity, etc etc. Kinda fundamentalists that get lost in their talking the functional talk.

[@blaz2892]

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

[@Eyesomorphic]

They are computationally equivalent, so you can actually encode a Turing Machine in the lambda calculus, and vice versa! This also means that there is a lambda calculus equivalent of a Universal Turing Machine, so you can build terms in the lambda calculus that act as an interpreter to run terms in the lambda calculus!

[@anywallsocket]

Bro watched the video 😂

[@scottcarothers837]

@@Eyesomorphicwell, yeah, of course they’re equivalent. lamba calculus is turing complete.

[@zTJq40sl]

​@@Eyesomorphic It's even relatively simple: If we encode the variable x as λ a b c . a x the application M N as λ a b c . b [encoding of term M] [encoding of term N] the lambda abstraction λ x . M as λ a b c . c (λ x . [encoding of M]) then an interpreter for the such-encoded lambda terms is "just" E = Y λ e m . m (λ x . x) (λ m n . (e m) (e n)) (λm v . e (m v)) where (as seen at 12:28) Y = λ f . (λ x . f (x x)) (λ x . f (x x)) (I'm using here "λ x y z . M" as a shorthand for "λ x . λ y . λ z . M", as usual once we've seen that we can emulate multi-argument functions by currying.) So yeah, if just looking at these lambda terms, they might seem rather unwieldy. But considering that they implement a fully self-hosting interpreter for a turing-complete language, they are rather tame. (And all the a b c-dot-something stuff is just for marking the encoded terms as (a) variable, (b) application or (c) abstraction, so that the interpreter can handle them accordingly.)

[@BC2300-NewStart]

Yeah, there's this thing called the church Turing thesis thay was only found cuz church and Turing realized that their attempts at defining computability were basically equal fr

[@little-ork]

halfway through the video I suddenly understood Haskell

[@ckpioo]

💀💀

[@ckpioo]

haskell mentioned

[@peacefulexistence_]

LC does have that effect on people :) ML (the family of languages Haskell is a part of) derives from LC.

[@rogergalindo7318]

now you have to follow the prophecy and become a haskell wizard!

[@pascalcharbonneau9019]

I have been trying really hard to learn functional programming without learning Haskell and this video gave me hope haha.

[@himanshutripathi7441]

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.

[@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! :))

[@kikivoorburg]

Some linguists have rigorously encoded linguistics using type theory! It’s well beyond my level of understanding, but some information can be found on Wikipedia

[@voltydequa845]

@@kikivoorburg If it was so we would have today real (symbolic logic) AI instead of the hyped trickstery that is presenting the gpt/llm stochastic parrot, or, better, the technique of "pattern matching on steroids"(© Torvalds), as AI. Language understanding (understanding implies inferences, so no llm) is all about domain, context and cognitive representation. Though types (domain & context) can help, encoding the cognitive representation is prohibitive seen the complexity (if we were that intelligent, we would have implemented the industrial revolution as soon as we got down from the trees).

[@cube2fox]

Simply typed lambda calculus is actually used in formal semantics, which is a branch of linguistics.

[@carmensavu5122]

@@cube2fox Yea, but I don't think it works.

[@emilmullerv3519]

To think that just because we can enconde certains part of language into math theories, then it would follow that we would be able to use that encoding directly in real life applicatios is absurd. LLM and tyoe theoretical analysis of language have wildly different onjectives, people who work iin the latter have interest in analysing the language itself, not in building applications that can chat with people or whatever ​@@voltydequa845

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

[@Eyesomorphic]

Glad it was helpful!

[@scroipt]

Though this really is more of a "hey this seems to work out" kind of proof than a particularly rigorous one.

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

[@houstonbova3136]

I thought he said Logician.

[@maximumhamster]

I heard the same thing, but it was due to listening on 2x speed. When I put it back to the 1x speed I could hear Logician.

[@BonktYT]

get off your high horse

[@angeldude101]

I heard "magician" and I was playing at 1x speed _and_ had captions turned on that said "logician."

[@lemoneer7474]

What’s funny is that this isn’t even the first time I’ve misheard logician as magician.

[@vivekkaushik9508]

Beautiful. I wish all subjects were taught like this in school. Soothing piano background music. Slow yet consistent pacing. Small breaks between individual sub topics. Thanks man. ❤

[@Eyesomorphic]

Thank you very much for the kind words :D

[@Dhiren_]

This is the best video I've seen on understanding how lambda calculus relates to logic, at the low-level! Thank you!

[@Eyesomorphic]

How kind :D

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

[@Zeero3846]

A compiled program is going to be correct, but whether you actually described the problem you intended to solve is an exercise left entirely to you.

[@andrew_ray]

@@Zeero3846 But by making liberal use of newtypes, the compiler can forbid many mistakes. For example, if you define newtypes for Seconds, Minutes, and Hours, the compiler will not let you make the mistake of assigning a number of minutes to a variable that expects to be denominated in hours. Or inches. Or hectopascals. You can avoid forgetting to sanitize inputs by requiring that all rendered strings be wrapped in a SafeString newtype. With the OverloadedStrings directive, string literals within the code don't need to be made safe, but any strings that come from user land do. And if the only way to convert a user land String to a SafeString is through the sanitizer... then you've proven you haven't forgotten to sanitize any user input because your program literally wouldn't typecheck if you had.

[@voltydequa845]

@@Zeero3846 Suggestion: the next time ask the gpt-style commenter to define better, by quantifying, what his «decent chance it's correct» means. He got 32 likes for serving hot-air - a dynamics similar to that of popular tv shows where more simplistic and vague one is, more the public appreciates.

[@rumble1925]

I recommend the talk "Lambda Calculus - Fundamentals of Lambda calculus & functional programming in Javascript" and follow along in the code examples - for anyone that wants to try this in practice and encode your own functions

[@Ploofles]

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

[@neutillius]

But It ld be a very long one. Like classical literature sentences for pages.

[@natebrown2805]

exec("print('hello') print('world')")

[@TrusePkay]

Try languages like F# and Scala. You will see how 3 lines of Scala will dwarf 15 lines of Java

[@AkivaB]

You can already do many of them anyways Comprehensions are weird

[@M-F-H]

even without "def" : just a single lambda expression! :)

[@PantheraLeo04]

I tried evaluating that "if 1 then false else true" example you gave to see if it could still be interpreted even though when using the abstracted names it looks like nonsense. When I expanded it out and worked through all the beta reductions, I got the identity function "λb.b". It's really cool that even when things seem like they should nonsense with no reasonable interpretation, you can still break it down and try to make something from it anyway.

[@chrisray9653]

This reminds me of that MIT video from '86 talking about the eval / apply loop at the core of Lisp. "MIT Structure and Interpretation of Computer Programs" "Scheme / Lisp"

[@dw3yn693]

you've got a link?

[@jackren295]

@@dw3yn693 I think it's this series, which is a classic: kzbin.info/www/bejne/Y3vCqX9qfqybgKM

[@chrisray9653]

@@dw3yn693 It's called Structure and Interpretation of Computer Programs (SICP MIT by Abelson and Sussman)

[@nythrox3047]

What's the name

[@mikemilner8080]

@@dw3yn693 Try a Google search of the MIT OpenCourseWare web site. The Wizzard book (Structure and Interpretation of Computer Programs) gets its name from the MIT course 6.001's title. I took 6.001 way back in 1969 - at that time the course used PAL (Pedagogical Algorithmic Language), a syntacically sugared version of Curried Lamba Calculus. Having only be previously exposed to procedural languages, the power of functional languages was a revelation.

[@neoplumes]

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

[@GlortMusic]

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

[@tessimago9625]

that's nice, now print "hello world"

[@angeldude101]

Hmm... that might be challenging... Would you accept just returning a string containing the characters for "hello world". In typed lambda calculus: "hello world" In untyped lambda calculus: (would need to define cons cells to form a linked list and store in that list the Church-encoded Peano numbers corresponding to the ASCII/Unicode codepoints of each character)

[@AnarchoAmericium]

(λx:String.x)("hello world")

[@gregoryfenn1462]

No, returning a string or data object isn't what the OP wants, they want the program to literally write to our stdout console. It's the most basic task in any new programming language, so how is that done in lamda calculus?

[@angeldude101]

@@gregoryfenn1462 For a more serious answer, one possibility would be to evaluate to a function whose argument is a hypothetical print "function", and then call that "function" with "hello world". Lambda Calculus can perform any _pure_ computation, but it doesn't inherently have any access to any host environment. Technically, if you stripped C of external libraries (including libc) and inline assembly, you would be just as incapable of "printing" to a "screen" as you would be in pure Lambda Calculus. Same as if you tried to write Brainfuck without the . and , commands.

[@nikolaygruychev2504]

consider a "standard library" - your program must be a function, not an application, and it accepts a pair list of all input. it can also emit a pair list itself, to represent the output. funnily, pairs can be used as sort-of-iterators, given that cons = \x. \y. \f. f x y; car = \p. p (\x.\y. x) ; cdr = \p. p (\x.\y. y), then we can have a lazyCons = \x.\f.\g. g x (lazyCons (f x) f) [google y combinator recursion], meaning that lazyCons 1 (\x. x + 1) gives us a list of all natural numbers, i.e. enumFrom 1 in haskell. with this, we can theoretically process any input stream, do computation with it, and emit output partially while the computation is going on much the same way a regular turing machine can. lambda calculus was not intended as proof math can be a programming language, but that machines can do math or something, idk im not a computer scientist

[@danielli3288]

this video is very good, it doesn't assume what you know and explains everything in a clear and concise way

[@fredericmazoit1441]

Very nice video. I would have added a hint as to why java is not more powerful than lambda calculus: we can write a java interpreter in lambda calculus. Thus any computation of a java program can be be performed by a lambda term.

[@56independent]

How does one then interact with the OS like most programming languages allow? How does one do the less abstract and more pragmatic "get me onto the internet" stuff? Whilst programming and lambda are equally powerful when considering closed systems where all the data is spoon-fed, in the real world of hardware and connections, one needs the interface with the real world.

[@Matthew-by2xx]

@@56independentThere are functional languages like Haskell, you still very much so can.

[@fredericmazoit1441]

@@56independent As with a processor, there are 2 kind of conputation: inputs/outputs and "real" computation. The structure of most programs can be reduced to while not finished: inputdata=input() data=computation(data) output(data) When we say that lambda calculus is as powerful as, say, java, we do not consider inputs/outputs.

[@aioia3885]

you could also make a java interpreter in the lambda calculus. In fact, someone made a compiler from c to the lambda calculus

[@56independent]

@@Matthew-by2xx ah, i forgot i even tried to learn it once

[@shadamethyst1258]

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

[@СергейМакеев-ж2н]

Are you using de Brujin indices? If so, when substituting M into x, the last thing you do to M is increase all indices by 1, which means there aren't any zeroes there, right?

[@shadamethyst1258]

@@СергейМакеев-ж2н That's the solution that the class I followed quickly led us to, yeah. But for a bit, we would work with call by value without de bruijn indices, and propagating substitutions across lambdas was a pain

[@amritawasthi7030]

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.

[@iisthphir]

Good concept, shame about the masochist who came up with the notations.

[@throstlewanion]

Absolutely fascinating premise. At first I was a bit confused about the purpose of this language, but now you have opened my eyes to the existence of an entire field dedicated to the study of the theory of programming. Wonderful video!

[@Eyesomorphic]

I'm glad that the video had it's intended effect! Thanks :)

[@mohamedfarouk9654]

Alice is so obsessed with Java.

[@mythacker4365]

😂😂😂😂

[@ryanbartlett672]

Great animations, pacing, and no assumption that we know this logic

[@ai_outline]

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

[@Italanon]

I was introduced to Alonzo Church’s lambda calculus paper when carrying out my a MSc. Course back in 1978. I don’t know how this popped up in my feed :)

[@underfilho]

I was expecting some haskell propaganda, but its actually for proof-assistants, great to hear about that!

[@setheisenberger247]

Incredible video. I was learning Lean4 a few months ago and found it difficult to wrap my head around the syntax. This video gives excellent motivation for the way Lean is!

[@ruanvermeulen7594]

I came back to this video. I wanted to tell someone else about the concept, but no reading material explains it this beautifully. Of course I just gave them the link to the video.

[@Eyesomorphic]

That's extremely kind, thanks!

[@bennyboiii1196]

There's a lambda interpreter called Interaction Combinators which uses graph theory to do lambda calculations in parallel without any race conditions or collisions. This actually makes parallel computing a lot easier for functional programmers, because historically, it was extremely difficult for FP do be done in parallel. It's also easier than doing it with procedural programming languages, because you don't need mutexes and locks.

[@samuelmayna]

Where did you read this?😂😂😂The opposite is what is true. FP was actually invented to enhance multiprocessing since no state is shared.

[@kenevanchik4478]

I had to take a course in this subject for my CS major long ago when I was a young man. It reminds me why I personally think I had so much problems with it, and certain kinds of math in particular. The concepts being presented to me are straightforward. What isn't however, is keeping all the symbols and characters clear in their meaning. I find these kinds of subjects tend to write things in ways which maximize brevity at the expense of understanding. Maybe that's just needed if you're an expert in the field, but honestly there just isn't enough mental separation for me from the visual presentation of the syntax. Variables are lower case letters, but applications are upper case. That beta-reduction example of M[N/x] is masking a lot going on. The example is simple in the video for comprehension, but that can get really complicated in a hurry. As a developer in the real world you can see lambda expressions in languages such as Kotlin, and frankly I don't know how much I like it. A lambda expression for a common or well known function is easier to type. If however, the function isn't well known, or complicated, then a lambda expression can make the function cryptic to the developer and difficult to grasp.

[@danielpark9033]

Thank you so much! I can now understand how lambda calculus works more than ever!

[@Oscar-vs5yw]

10/10, clear explanation, good examples, awesome balance of rigor and simplicity. And a conclusion that very much so made me wonder about lambda calculus! I was always too afraid to approach lambda calculus, but your video showed it to just be python! Thanks so much

[@Eyesomorphic]

That's very encouraging, thanks for the kind words

[@shathamaayouf6048]

This was therapeutic and educational at the same time. Wow.

[@Double-Negative]

since regular lambda calculus is untyped, you can give functions inputs that shouldn't work. for example, if you add 2 instances of church + using church +, you get another binary function f(x,y) = 2x + y

[@CTimmerman]

Sounds significant somehow, but dangerous like Perl.

[@swankitydankity297]

fantastic video! you paced it so well and animated it so clearly that I was able to follow closely and never felt lost.

[@Ridaha]

Awesome video :-) Formalized mathematics is the future! A proof of Fermat's Last Theorem in LEAN is being currently worked on by professor Kevin Buzzard and the lean community!

[@kotylka90]

this channel is so underrated!

[@julianvillaquira4127]

First video I watch and immediately subscribed. PS: Eyesomorphic is a damn good name 🤯

[@Eyesomorphic]

Thank you!

[@DanDart]

I seriously thought you said "magician" instead of "logician" there - that's hilarious and probably also true.

[@LethalChicken77]

The problem with functional programming is it's not how humans think and it's not how computers work.

[@mushykitten]

nontheless it's an extremely useful tool for computer science. sometimes computer science or math is about exploring these unique systems and seeing what is there to learn about them.

[@rogergalindo7318]

the thing is, it’s not that simple. Compiler optimizations can do wonders. Haskell can get at 3x C. Which really is on the camp of go, java, etc, o only beaten by cpp c or rust on the other hand, once you “get” how to think “functionally”, it’s really not that hard. It’s just a matter of usage or habit

[@klermaud314]

It is definitely how many people think. It just depends on how you learned programming. And basically no programming language that people write their programs in is how computers work. The whole point of programming languages is to abstract away from the underlying machine.

[@klembokable]

I disagree with everything you just said. As someone who has built a garbage register computer in a simulation, and wrote a bit of haskell, I see as little connection between haskell and assembly as I do between python and assembly...

[@klembokable]

As far as humans thinking is concerned, I think seeing the world in terms of the inputs and outputs of actions makes about as much sense as seeing things in terms of the individual attributes of the objects acted on

[@dylanjayatilaka8533]

Bravo! I didn't think that the notion of higher order was special, but it was astounding that you could encode True and False. And "3", which seems to be three applications of any old function f. And recursion. And it seemed to me that the Curry-Howard correspondence could also itself be expressed in terms of the lambda calculus, as a proposition. Is there an end to this madness? It occured to me that, I myself might correspond to a kind of imperfect lambda machine, which begs the question, what machine? Where did the lambda notion of this representation of True and False come from? Is it possible to define a lamba expression/machine that comes up with hypotheses such as True and False, and is able to make and name things like Bool and "numbers"? I feel the answer to this imperfectly phrased question is False. But bravo again on this episode, I finally "get it", at the expense of going slightly mad. I just mention that I had to pause at several points, whereas on most other videos, I go at twice normal speed. Bravo!

[@cmilkau]

Not only do you only need 3 rules of syntax, in fact you only need 3 objects: a "const" function (λx.λy.x), a "symbolic evaluation" function (λf.λg.λx.[f(x)][g(x)]) [you can interpret this as taking a family f_x of functions and a family g_x of function arguments and return a family f_x(g_x) of function values), and function application. There is a mechanistic algorithm that turns any lambda expression into an expression tree containing just these two functions as leaves and function composition as inner nodes. Some important derivations: const = λx.λy.x symb = λf.λg.λx.(fx)(gx) chain = λf.λg.λx. f(gx) = λf.λg.λx.(const f x)(gx) =(**)= λf.λg. symb (const f) g =(***)= λf. symb (const f) = λf. (const symb f)(const f) = symb (const symb) const swap_args = λf.λx.λy. f y x = λf.λx.λy. (f y)(const x y) = λf.λx. symb f (const x) =(*)= λf. chain (symb f) const = λf. (chain (symb f)) (const const f) = symb (chain chain symb) (const const) swap_args = λf.λx.λy. f y x = λf.λx.λy. (f y)(const x y) = λf.λx. symb f (const x) = λf.λx. (const (symb f) x)(const x) = λf. symb (const (symb f)) const = λf. symb (const (symb f)) (const const f) = symb (λf. symb(const(symb f))) (const const) = symb (symb (const symb) (λf.const(symb f))) (const const) = symb (symb (const symb) (symb (const const) symb)) (const const) const_id = λy.λx.x = swap_args const =(*)= chain (symb const) const =(**)= symb (const (symb const)) const id = λx.x = (λy.λx.x)(const) = const_id const =(*)= chain (symb const) const const = symb const (const const) There is a simpler derivation of const_id and id, but it doesn't yield the correct type on typical (a bit too naive) type systems: const_id = λg.λx.x = λg.λx. const x (gx) = λg. symb const g = symb const, id = λx.x = (λy.λx.x)(const) = const_id const = symb const const This is because typical type systems would expect g to accept a value x, even though it is never "called" like that, because the value gx is completely ignored. Other interesting equations: chain =(***)= λf. symb (const f) = chain symb const const_id = chain const_id const

[@alonamaloh]

"Makes ANYTHING a comptuter can do", except for spell checking, apparently. :)

[@Eyesomorphic]

That does seem to be the case 😭

[@ChumitoMC]

Can't believe it took me this video to understand Python's lambda function 😭 thx for this video! ☺️☺️☺️💖

[@kevon217]

Wow, this was so intuitively explained. Excellent!

[@ChecedRodgers]

What a lovely video. This nicely clarified a few concepts I'd encountered in passing but had not unpacked yet. Thanks for this.

[@Eyesomorphic]

That's very kind 🤠

[@pianocoder]

Thanks for the nice video again! It's very unfortunate that Coq wasn't mentioned here. :) For anyone interested in proof assistants, I recommend Software Foundations volume 1 for Coq, and mathematics in lean tutorial for Lean!

[@st04713]

Awesome ! please and please upload more contents. This video saves a lot of my time trying to understand functional programing.

[@wol2403]

You know a video is really good when it takes you 2 hours to watch it even though its only 20 minutes long

[@writerightmathnation9481]

It might help if you point out how this is significantly different from the traditional notation using Polish notation: f(x).

[@com0oan]

Tried to understand lambda calculus for years. First video that made the concept click in my mind. thanks!

[@hitoshiyamauchi]

I thank you for this excellent introduction to lambda-calculus. Thanks for the video. 😀

[@Eyesomorphic]

That means a lot, thank you :D

[@Fine_Mouche]

so M stand for Map ? and it's equivalent to the Image if x is the antecedent (inverse-image) ? and equivalent to x : start set and M the finish set of a function ?

[@the_actual_lauren]

Why don't we just use function notation as established early on in math education such as f(x) = x + 1 instead of lamda x . x + 1 which is harder to read?

[@M_1024]

"^x.x + 1" is directly the function itself. "f(x) = x + 1" creates a function and gives it a name. Its like a difference between "5" (value) and "x := 5" (assigment). In fact "f(x) = x + 1" is equivalent to "f := (^x.x + 1)".

[@the_actual_lauren]

@@M_1024 Thanks

[@logician1234]

Please do a video on Calculus of Constructions and encoding logic in it

[@backhdlp]

this is actually really easy to understand if your first programming language was functional

[@familiagavassafavoretti4805]

Those pauses you make are key. Great job!!!

[@funktorial]

really good animations dude. also did a really good job of picking what not to include (eta reduction, Church-Rosser, etc)

[@linusandersen5608]

any book recommendations on lambda calculus / computation theory?

[@cindrmon]

thanks for igniting my interest for computer science just because of lambda calculus! didn't know this was indirectly taught to us through LISP, since it does seem resemble a lot of similarities to LISP's functional programming approach

[@JJ-tp2lc]

I hope you do another video on lambda calculus, especially on the Y combinator, because I still dont quite understand it

[@RAyLV17]

I have always been kind of comfortable with programming, but found it difficult to go into proofs and higher mathematics. But learning about this and LEAN is giving me hope. I am surely gonna check it out!

[@Eyesomorphic]

That's great to hear, proof assistants can be daunting but I find them very rewarding!

[@cerulity32k]

SO THAT'S WHY ANONYMOUS FUNCTIONS ARE CALLED LAMBDAS

[@qcolive]

close enough welcome back haskell

[@Dent42]

I'd be interested to learn how the encodings would change if incorporating ternary/paraconsistent logic

[@adrianfd7440]

I completely enjoyed this video. Thank you so much

[@blankboy-ww7jt]

Very good introductory content, from lambda calculus to types and the CH correspondence

[@gregoryfenn1462]

When you introduced the syntax for Lambda calculus at 4:30, there are no symbols for + or 1, so when you used those to define the function mapping x to x+1, how is that possible? Your example at 6:03 uses the + symbol, but this symbol itself is not even part of the Lambda calculus language, so you can not use it.

[@chezbgone0]

We're using the symbols + and 1 for pedagogic purposes, but as noted later you can define numbers (and operations on them like addition) like we defined booleans, and there would be lambda terms that represent the symbols you mentioned.

[@lexkoal8657]

Thanks for the video. A few questions/clarifications: what does Applications M M means at 4:10, and it would have been helpful to explain how multiple inputs work: the most left input goes first and works on the most left lambda abstraction and so on. Because input goes where the variable is kinda obvious but other semantics of lambda calculus are not that clear

[@vibaj16]

it means applying M to M. When lambda terms are next to each other, you apply from left to right, unless parentheses change the order: a b c means apply a to b, then apply that to c. On the other hand, a (b c) means apply b to c, then apply a to that.

[@tricky2014]

I find lambda calculus so much more elegant than turing machines.

[@FranoGames]

finally haskell syntax makes sense

[@sundae6610]

This give me motivation. Making a language might be a good side project after i finished my current one haha

[@roastyou666]

You can talk about logical programming next, like PROLOG.

[@Sadigziggi]

Isn't beta reduction what happens when you add a hydrogen to a double bond?

[@germanassasin1046]

16:02 very generous of you to use c as an example for statically typed language

[@NostraDavid2]

If you want to do another video about math that's the foundation for a lot of code I recommend the Relational Model by E. F. Codd. I'll admit that the first paper was not as rigorous as the Lambda Calculus, but it is Super fundamental to any relational database.

[@NostraDavid2]

Oh, and use both 1969 (nice!) and 1970 papers!

[@PhilippSLSchäfer]

Lean is so cool! Not coming from a formal mathematical background Lean helped me to learn what mathematical proofs are all about. But since most analysis textbooks are based on ZF(C) and Lean is based on dependent type theory I couldn't use it to solve all my exercises :/

[@bachirlachguel9218]

This looks great and is very well explained, which software do you use for the slides ?

[@Eyesomorphic]

I use Manim for the animated mathematics and pivot for the animated figures. Then I use da Vinci resolve to splice them all together :)

[@Phostings1]

I was always curious about what a lamda function did. I did some digging around and eventually understood how it works on the programming side of things. So watching this verified my understanding to some extent and made me feel a little better knowing i'm not quite strong in math,lol.

[@uliveulearnandregret]

Two big figures inventing programming concepts before programming was technically a thing

[@GabriTell]

This is so great... Will you ever make a video about Type Theory? 👀

[@CjqNslXUcM]

I'm eagerly awaiting the next video.

[@TrusePkay]

This video reminds me of my F# days. The real fundamental property of functional languages that separate them from mainstream imperative languages is that functional code has an immutable state. You cannot reassign values on the fly. And there are no nulls, although these are compensated with Option type systems. This makes functional languages not suitable for applications where states are important. Because the definition is clear, functional languages are short and free of bugs most of the time. They read code left to right. I was talking to a friend. He asked me how can a programming language be practically acceptable if it does not have procedures like if statements, loop statements, nulls, return keywords. I showed him how pattern matching, function composition, partial applications, generative sequences, and list comprehension, pattern work in F# and Scala, and you don't need to write verbose repetitive loops and branches. Just go straight to the point, and the program is ready. It's sad that functional programming is not mainstream or not even computing with the mainstream.

[@ay-rf5se]

now im starting to wonder what the "simplest" kind of tool equal to a turing machine is. im not sure if simple is the correct word here, but take a non-deterministic turing machine for an example. idk if its "simpler" than a regular turing machine, but it definitely achieves the same output with equally as many or less steps. and then again, simpler doesnt always mean easier

[@electra_]

I think a decent candidate is the "find and replace" algorithm, where you just have a list of terms to find and replace, and you do them in order, and then repeat. So like if the replacements were A -> B, BB -> A, then you'd have like BABA (A -> B) BBBB (BB -> A) AA (A -> B) BB (BB -> A) A (A -> B) B To demonstrate this is Turing Complete, you can have a sequence of find and replaces that act primarily on the "head" of the tape, represented by its state. So if the states of the machine are A and B, and the data is 1s and 0s, a tape would look like 001001A001010 and a relevant find and replace operation for (When in state A, if 0 move to the left in state A, if 1 turn it into 0 and move to the right in state B) would be 0A0 -> A00 1A0 -> A10 A1 -> 0B Another similar one is having a list of resource exchanges to be done, something like Lose 10 As, add 3 Bs Lose 2 As and 2 Bs, add 1 C and you just try to do these exchanges in order if possible, with the higher ones having higher priority This ends up being turing complete if you have 7 resource types, and maybe less. The proof is more complicated than the previous one, the tape is represented by 3 resource types: L, C, R the count of L and R are binary numbers representing the tape, and C is the center (the one that's selected) so the tape 100(0)101 would be L = 4, C = 0, R = 5 note that least significant bit is always closest to the center theres also a temporary variable T and this is used for multiplication and division you can do something like 2R -> T T -> R to half or double things and this can be used to bit-shift but you need a control signal of some sort to make that work so there is SL, SR for the shift left and shift right so that'd be something like 5SR, R -> 5SR, T 5SR -> 4SR 4SR, T -> 4SR, 2R and having different values of SR required ensures that you always do the steps in order so to shift right you would multiply R by 2 move C to R divide L by 2, putting remainder in C then to control the state, you have S where the count of S is the state you're on and that would be something like S, C -> 3S, 5SR S -> 2S, C, 5SL so you can very easily determine the shift direction, next state, and next center value to reduce that to 4 types from 7, you can notice that C, SL, SR, and S all have a finite amount of states so you can just combine those into one state variable which encodes all of those state transitions L, R, and T represent infinitely long binary numbers and thus you can't do the same with them

[@M_1024]

Here is a very simple turing complete system: start with a bitstring (input) and a "book" of bitstrings (instructions). Every iteration: 1. Remove the first bit from the main bitstring. 2. If it was a 1 append the contents of the current page of the book to the bitstring. 3. Flip to the next page in the book (or the first page if you are at the end). 4. Repeat.

[@M_1024]

Another simple turing complete system: a programming launguage with 3 instructions: 1. Increase variables A and B by one. 2. Decrease A by one if its positive, otherwise jump to a specific point in the program 3. Same as above but for B. It can be made even simpler if you make it so that instructions 2 and 3 always jump the same amount K forward, and join the end of the program to its beggining. If K is large enough this will also be turing complete.

[@cinderwolf32]

You should check on the Wikipedia page for single instruction set computers!

[@tylerfusco7495]

I mean there's the SK combinator calculus, with just two terms and no variables, and there's also cellular autonomic rules that seem incredibly simple but are turing complete. It all depends on what your definition of "simple" is

[@ValidatingUsername]

1:45 Do not confuse this with multivariable equations that you can find the inverse of or isolate for a variable and determine properties given that alpha equivalence and alpha conversion capacity. If y = x^2 that doesn’t mean x = x^2 unless the “programming language” overwrites the interpretation to make them isomorphic. Because that’s what different glyphs holding the same value is doing.

[@beck3k]

The figure wears a wide-brimmed hat while teaching lambda calculus, just like my programming languages professor!

[@nerida3347]

Man, i would've paid attention in math class if my teachers took their time like this and explain it clearly lol

[@taylormanning2709]

"Named after the magician Haskell Curry" (7:37) Can't believe I had to look that up. For a second... I believed you

[@Eyesomorphic]

Sorry, a few people seem to have misheard 'Logician' as 'Magician'. Though there is an argument to be had that Curry's work was profound enough to classify it as magic!

[@DeathSugar]

Wish someone made step-by-step explanaition of that simple lean proof with unfolding the stuff.

[@TymexComputing]

20:45 - well there are some long elaborate proofs that could be found using LEAN but still you need to pass some time for it as many many of conjectures simply live over the basic axioms - as Turing proved himself.

[@minecrafting_il]

When you revealed how to use multiple inputs I said out loud "Fuck you.". That is a dirty, dirty trick that has no right being as mathematically elegant as it is.

[@Eyesomorphic]

I remember having a similar reaction when I learnt about it! It's not only elegant, it's incredibly useful! We can 'partially apply' functions to get new functions, so (add 1) is itself a function that we can pass around and use, and simply adds one to its argument!

[@minecrafting_il]

@@Eyesomorphic yep, I get that. You explain things very well, earned yourself my sub!