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 :)

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

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

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

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

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

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

[@gerocastano8]

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

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

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

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

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

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

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

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

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

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

[@danielli3288]

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

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

[@mohamedfarouk9654]

Alice is so obsessed with Java.

[@mythacker4365]

😂😂😂😂

[@GlortMusic]

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

[@neoplumes]

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

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

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

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

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

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

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

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

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

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

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

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

[@swankitydankity297]

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

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

[@backhdlp]

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

[@danielpark9033]

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

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

[@ryanbartlett672]

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

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

[@st04713]

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

[@kevon217]

Wow, this was so intuitively explained. Excellent!

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

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

[@underfilho]

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

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

[@iisthphir]

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

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

[@funktorial]

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

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

[@com0oan]

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

[@blankboy-ww7jt]

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

[@shathamaayouf6048]

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

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

[@germanassasin1046]

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

[@logician1234]

Please do a video on Calculus of Constructions and encoding logic in 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!

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

[@ChumitoMC]

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

[@alonamaloh]

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

[@Eyesomorphic]

That does seem to be the case 😭

[@JJ-tp2lc]

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

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

[@writerightmathnation9481]

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

[@adrianfd7440]

I completely enjoyed this video. Thank you so much

[@hitoshiyamauchi]

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

[@Eyesomorphic]

That means a lot, thank you :D

[@linusandersen5608]

any book recommendations on lambda calculus / computation theory?

[@cerulity32k]

SO THAT'S WHY ANONYMOUS FUNCTIONS ARE CALLED LAMBDAS

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

[@sundae6610]

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

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

[@snoopy1alpha]

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.

[@Dent42]

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

[@wol2403]

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

[@familiagavassafavoretti4805]

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

[@nerida3347]

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

[@DanDart]

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

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

[@cube2fox]

It's important to mention that you use the "+" function in the first part but this function is not part of the lambda calculus! So this only works if you first encode numbers and addition as valid functions within the lambda calculus, similar to "true" or "ifthen".

[@GabriTell]

I don't know if I'm the only one who appreciates how fascinating this is. ✨ It's very cool not only because it allows you to give shape to the most abstract mathematical concepts, but also because it literally allows you to create new maths (since this is such a very high level of language abstraction, we haven't even defined things such as what means two "things" to be "equal"), we could even construct a realm of maths where there are three truth values (or as many as we want). The only limit is our imagination. 🔥✨ This video inspired me to define maths as: "The language of creativity"

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

[@FranoGames]

finally haskell syntax makes sense

[@tricky2014]

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

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

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

[@julianvillaquira4127]

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

[@Eyesomorphic]

Thank you!

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

[@roastyou666]

You can talk about logical programming next, like PROLOG.

[@DeathSugar]

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

[@NuclearShadowYT]

Wait until you find out about the Haskell programming language

[@kotylka90]

this channel is so underrated!

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

[@kales901]

and you could define the the ifthen as that (lambda:b.lambda:x.lambda:y.b x y) function

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

[@arossfelder]

Can we talk about the fact that the recurrence thing is genius, and you can even put condition to stop it !

[@pandalonium]

Thank you soo much. I found programming languages super difficult but this, this is so simple and easy to understand.

[@ananyapamde4514]

What a beautiful video! God bless you

[@qcolive]

close enough welcome back haskell

[@BertLeyson]

Hearing Bob and Alice literally reminds me of GBG.