Комментарии:
The best video on λcalc‼️‼️
ОтветитьBest explanation on the internet
ОтветитьA bit of trivia about S and K...
TL;DR: The type schemas for K and S are T -> U -> T and (T -> U -> V) -> (T -> U) -> T -> V, respectively. These two types, when read as logical formulas and taken as axioms form a basis of the propositional calculus (with -> as the only connector).
In more detail:
First let us consider B, which is \fgx.f(gx). This is also known as "function composition" - f is called with the result of calling g on x. S is a "stronger" version of B where the outer function (here f) also receives x as an additional argument while also - like B - receiving gx, i.e., the result of applying the second function to that argument. S = \fgx.fx(gx)
Now suppose we want to give types (really: type schemas) to K and S.
K is easy. If the type of the first argument of K is T and the type of the second argument is U, then the type of the result is again T. Therefore we have:
K: T -> U -> T
(Side note: the type arrows group to the right, which meshes well with function application grouping to the left. T -> U -> T is really T -> (U -> T).)
Before looking at S, let's again look at its simpler cousin B. Here the second argument is a function from some type T to some other type U, which means that the first argument must be a function able to receive an argument of type U while then producing a result of a third type V. The end result is a function from T to V.
B: (U -> V) -> (T -> U) -> T -> V
The case of S this is very similar, except the first function not only receives U but also a copy of the T argument:
S: (T -> U -> V) -> (T -> U) -> T -> V
Now look at only the type schemas and forget about the combinators. We have:
T -> U -> T
(T -> U -> V) -> (T -> U) -> T -> V
Further forget that these are types and instead read them as formulas in propositional calculus, reading the function type arrow -> as implication:
T -> U -> T means:
If we already know T, then anything (call it U) implies that T. (It does not matter what the U is and whether or not it is true.)
(T -> U -> V) -> (T -> U) -> T -> V means:
Suppose T implies U (that's the second argument or the middle of the formula). Further suppose that when T is true then U implies V. (That's the first argument. Notice that U does not need to unconditionally imply V, it only needs to imply V when T is true.) Then T implies V.
It turns out that these two formulas, when taken as logical axioms, form a basis of the propositional calculus (where the only connector is implication). In other words, every tautology in propositional calculus can be proved from just these two axioms.
Isn't that neat?
Brought to you courtesy of Mr. Curry and Mr. Howard. :)
PS: Of course, the same thing works for the types of the combinators of any other basis, including the one consisting of 5 combinators mentioned in the talk. It just means there are also 5 corresponding axioms then.
Best explanation yet from a high school student perspective thank you :)
ОтветитьI choked already on the first example. Why 'const'? What is constant there? And why is it relevant?
ОтветитьWhat I’d give to be in that classroom :(
Ответить🙌
ОтветитьNot going to lie, that man not only smart but is also looking fine as day 😏
Ответитьlambda calculus ist the most nonsensical, useless shit i have ever seen.
Ответитьshouts out i finally get it
ОтветитьThis makes me wonder why Lambda Calculus never became the standard... It certainly makes a lot more sense than the turing approach in my opinion!
ОтветитьRemarkable, this is the video recommended by my professor
ОтветитьI need more of this. Gabriel now works for Google. If they were wise, they would have him give lectures.
ОтветитьAwesome, thanks a lot. This is a programming 💎
ОтветитьWhy did not we use "lambda e.f" function at the end of beta reduction ?
ОтветитьThe inset obscures important items in the discussion.
ОтветитьThanks for the great presentation!
ОтветитьGreat video!
ОтветитьClearly clearest explanation on YT
ОтветитьThis talk is essential. Seriously. I've spent the last 9 months implementing λ-calculus, inspired by this, and every now and then I come back to it, just because it is so awesome.
Ответитьsomething i thought of: for that "equality", instead of lambda p, q: p q (Not q) you could instead have lambda p, q: p Id Not q, and Xor is just p Not Id q. Xor especially generalizes to any number of terms by repeating: lambda a, b... z: a Not Id b Not Id ... z
ОтветитьRe-upload with the camera on the right it gets in they way now unfortunately
ОтветитьThis probably just saved my midterm grade, 10000x more clear than anything my professor has ever said. Also, this dude looks like the Jeff Winger of logical mathematics
ОтветитьMr. Lebec, thank you very much for this material of yours. I will do my best to digest this to the best of my intellectual ability.
Ответитьso clear explained and slide are just artwork
ОтветитьThankyou so much for the lecture.
ОтветитьMoses Isajewitsch Schönfinkel Ukrainian Logician born in Dnipro.
Schönfink: German for "green munia". A bird species from India... now all these bird references make a bit more sense.
I watched several videos about this topic and felt I kind of grasped it but this talk just made it crystal clear. Seriously can't say anything that hasn't already been said, but this talk is amazing and mind expanding!
Ответить🎵Go Haskell go go! Haskell B. Curry
ОтветитьA great talk fun and truly informative.
ОтветитьThe prettiest slides I have ever seen.
edit: also some of the most engaging math/programming teaching I have ever been privy to!
superb!
ОтветитьThis was great. What should I watch (or read) next if I want to dig a little deeper?
Ответитьgreat talk. pity about the placement of the video camera image… needs to move around to show the final line of code that we sometimes never see as he changes slide without entering new lines.
Ответить1000x better than university professor's explanation
ОтветитьThis was honestly a very amazing talk, fun and educational at the same time, I've just had fun learning while preparing for my exams, again great work and many thanks mister Gabriel!
ОтветитьThank you for making this !!
Ответить