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.
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.
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.
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."
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.
@@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).
@@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.
@@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.
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
@@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
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
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.
Yeah cuz λ calc is Turing complete, so it’s complexity is sufficient to simulate any normal computation, including the simulation of any other computer.
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.
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.
@@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.
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. ❤
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!
@@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.)
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
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.
@@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.
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.
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.
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! :))
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
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
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.
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.
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!
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)
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?
@@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.
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
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
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 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.
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 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.
@@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.
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!
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 :)
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?
@@СергейМакеев-ж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
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.
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
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.
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.
@@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.
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.
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
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.
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.
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!
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!
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
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!
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!
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.
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
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.
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...
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
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
I remember learning that at university. I also remember us covering the Y-function and recursion in the lambda calculus. I wish you hat covered that in more detail. My lambda calculus skills have been crippled over the years. However, I remember that I used to be good at it 😀Maybe I should challenge myself again in Haskell.
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
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.
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!
The phrase "we know it's correct because it type checks" has blown my mind. I must learn more about Curry-Howard correspondence now
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.
Absolutely insane
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.
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.
wait until you hear about dependently typed programming languages
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."
That's very reassuring, I'm glad you enjoyed it :)
as someone who loves both maths and programming, this is probably my favourite math video I've ever seen
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.
@@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).
@@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.
@@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.
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
@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.
I wonder what the programming language would look like if the arrow was preserved
@@Anonymous-df8it This is what languages like Ocaml do.
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…
@@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
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
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.
Yeah cuz λ calc is Turing complete, so it’s complexity is sufficient to simulate any normal computation, including the simulation of any other computer.
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.
@@writerightmathnation9481 i believe that was OP's point, you just said it differently. no one is saying complexity == effectiveness
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.
@@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.
halfway through the video I suddenly understood Haskell
💀💀
haskell mentioned
LC does have that effect on people :) ML (the family of languages Haskell is a part of) derives from LC.
now you have to follow the prophecy and become a haskell wizard!
I have been trying really hard to learn functional programming without learning Haskell and this video gave me hope haha.
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. ❤
Thank you very much for the kind words :D
As a computer science student that studied functional programming and mathematics, I absolutely love this video. Please keep going!
Lambda Calculus seems like the Functional version of a Turing Machine. Very interesting.
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!
Bro watched the video 😂
@@Eyesomorphicwell, yeah, of course they’re equivalent. lamba calculus is turing complete.
@@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.)
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
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.
Years of fp propaganda from my friends; And it is this video that finally convinces me it is in fact worth the effort
That is quite the compliment, thank you!
@@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.
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.
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.
Glad it was helpful!
Though this really is more of a "hey this seems to work out" kind of proof than a particularly rigorous one.
Wait, this was released 10 days ago? I swear I come back to watch this every 6 months
This is the best video I've seen on understanding how lambda calculus relates to logic, at the low-level! Thank you!
How kind :D
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! :))
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
@@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).
Simply typed lambda calculus is actually used in formal semantics, which is a branch of linguistics.
@@cube2fox Yea, but I don't think it works.
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
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.
You summed up most of the Theory of Computation, Complexity and Logic course that I attended at university. Kudos to you Eyesomorphic! 👏🏼
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.
That's extremely kind, thanks!
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!
I'm glad that the video had it's intended effect! Thanks :)
so what your saying is i can write every single python program in one line
But It ld be a very long one. Like classical literature sentences for pages.
exec("print('hello')
print('world')")
Try languages like F# and Scala. You will see how 3 lines of Scala will dwarf 15 lines of Java
You can already do many of them anyways
Comprehensions are weird
even without "def" : just a single lambda expression! :)
that's nice, now print "hello world"
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)
(λx:String.x)("hello world")
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?
@@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.
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
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
7:30 "This method...is named currying after the magician Haskell Curry." I'm sure advanced mathematics seems to be magic to some people.
I thought he said Logician.
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.
get off your high horse
I heard "magician" and I was playing at 1x speed _and_ had captions turned on that said "logician."
What’s funny is that this isn’t even the first time I’ve misheard logician as magician.
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"
you've got a link?
@@dw3yn693 I think it's this series, which is a classic: ua-cam.com/video/-J_xL4IGhJA/v-deo.html
@@dw3yn693 It's called Structure and Interpretation of Computer Programs (SICP MIT by Abelson and Sussman)
What's the name
@@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.
this video is very good, it doesn't assume what you know and explains everything in a clear and concise way
You know a video is really good when it takes you 2 hours to watch it even though its only 20 minutes long
Alice is so obsessed with Java.
😂😂😂😂
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.
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.
@@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.
@@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.
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!
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 :)
this is actually really easy to understand if your first programming language was functional
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...
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?
@@СергейМакеев-ж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
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.
Great animations, pacing, and no assumption that we know this logic
Man, i would've paid attention in math class if my teachers took their time like this and explain it clearly lol
Good concept, shame about the masochist who came up with the notations.
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
That's very encouraging, thanks for the kind words
Thank you so much! I can now understand how lambda calculus works more than ever!
I was expecting some haskell propaganda, but its actually for proof-assistants, great to hear about that!
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.
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.
@@56independentThere are functional languages like Haskell, you still very much so can.
@@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.
you could also make a java interpreter in the lambda calculus. In fact, someone made a compiler from c to the lambda calculus
@@Matthew-by2xx ah, i forgot i even tried to learn it once
What a lovely video. This nicely clarified a few concepts I'd encountered in passing but had not unpacked yet. Thanks for this.
That's very kind 🤠
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.
We need more channels like this. Great Computer Science content mate!! Instant subscribe 🙏🏼
fantastic video! you paced it so well and animated it so clearly that I was able to follow closely and never felt lost.
This was therapeutic and educational at the same time. Wow.
16:02 very generous of you to use c as an example for statically typed language
Tried to understand lambda calculus for years. First video that made the concept click in my mind. thanks!
Awesome ! please and please upload more contents. This video saves a lot of my time trying to understand functional programing.
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
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.
Wow, this was so intuitively explained. Excellent!
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.
Where did you read this?😂😂😂The opposite is what is true. FP was actually invented to enhance multiprocessing since no state is shared.
This give me motivation. Making a language might be a good side project after i finished my current one haha
Can't believe it took me this video to understand Python's lambda function 😭 thx for this video! ☺️☺️☺️💖
I thank you for this excellent introduction to lambda-calculus. Thanks for the video. 😀
That means a lot, thank you :D
Very good introductory content, from lambda calculus to types and the CH correspondence
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!
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!
really good animations dude. also did a really good job of picking what not to include (eta reduction, Church-Rosser, etc)
I seriously thought you said "magician" instead of "logician" there - that's hilarious and probably also true.
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
Sounds significant somehow, but dangerous like Perl.
Those pauses you make are key. Great job!!!
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!
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!
That's great to hear, proof assistants can be daunting but I find them very rewarding!
Can we talk about the fact that the recurrence thing is genius, and you can even put condition to stop it !
I find lambda calculus so much more elegant than turing machines.
The problem with functional programming is it's not how humans think and it's not how computers work.
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.
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
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.
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...
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
"Makes ANYTHING a comptuter can do", except for spell checking, apparently. :)
That does seem to be the case 😭
Please do a video on Calculus of Constructions and encoding logic in it
this channel is so underrated!
I completely enjoyed this video. Thank you so much
First video I watch and immediately subscribed. PS: Eyesomorphic is a damn good name 🤯
Thank you!
finally haskell syntax makes sense
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
I remember learning that at university. I also remember us covering the Y-function and recursion in the lambda calculus. I wish you hat covered that in more detail. My lambda calculus skills have been crippled over the years. However, I remember that I used to be good at it 😀Maybe I should challenge myself again in Haskell.
close enough welcome back haskell
Only 7K upvotes? I would expect it to be 700K!!!
I hope you do another video on lambda calculus, especially on the Y combinator, because I still dont quite understand it
You can talk about logical programming next, like PROLOG.
bro, where was this during my autumn semester :D
Wait until you find out about the Haskell programming language
Having experience with Haskell helped me understand this video
Two big figures inventing programming concepts before programming was technically a thing
Your intro is dope
This looks great and is very well explained, which software do you use for the slides ?
I use Manim for the animated mathematics and pivot for the animated figures. Then I use da Vinci resolve to splice them all together :)
This video is a treasure
I always wanted to understand lambda calculus, this is so beautiful i actually almost cried
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
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.
I'm eagerly awaiting the next video.
light theme manim somehow feels cursed yet makes perfect sense at the same time
Wish someone made step-by-step explanaition of that simple lean proof with unfolding the stuff.
if only this was here during my organization of programming languages class
This is so great...
Will you ever make a video about Type Theory? 👀
SO THAT'S WHY ANONYMOUS FUNCTIONS ARE CALLED LAMBDAS
Hearing Bob and Alice literally reminds me of GBG.
Thank you for the great introduction.
Great explanation and animations.
I've been trying to tell everyone about this for 10 years. I have a project which iterates through each possible algorithm.
"Named after the magician Haskell Curry" (7:37)
Can't believe I had to look that up. For a second... I believed you
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!
The figure wears a wide-brimmed hat while teaching lambda calculus, just like my programming languages professor!