## Link https://youtu.be/QVwm9jlBTik ## Clips ### There was in the 1920s a project involving both Church and Curry to create a new foundation for mathematics involving functions rather than sets, and the project ran into paradoxes very similar to the ones that had afflicted naive set theory start = 0:55 end = 2:10 ### The big three important theorems about lambda calculus start = 2:00 end = 5:00 ### The second Church Rosser theorem says that to find the normal form in general, you have to substitute the parameter into the function body WITHOUT evaluating it first - This corresponds to lazy evaluation start = 4:50 end = 6:20 ### S K combinators - Curry and how it arose start = 7:00 end = 10:40 ### John McCarthy developed Lisp starting in 1958 - S language atoms start = 9:00 end = 11:15 ### McCarthy's model was Kleene's theory of recursive functions. start = 11:45 end = 12:45 ### Lisp was not based on the lambda Calculus, notwithstanding McCarthy's use of the term lambda. He hadn't read Church when he made Lisp. McCarthy was thinking about the General Recursive Functions model, and that makes the scopes come out wrong. Not until Scheme in 1975 did you get versions of LISP with lambda calculus based scope rules start = 11:45 end = 13:45 ### Meanwhile, back on the other side of the Atlantic, ALGOL-60 was happening, which was the grandfather of a great many languages on the mu side of computing. You could pass functions as parameters but not return them start = 12:45 end = 14:45 ### The invention of closures - Randal and Russell were among the first people to do a full implementation of ALGOL-60 around 1964, and they discuss how to implement free variables start = 13:30 end = 15:00 ### Landin (the "Next 700 programming languages" guy) was the one who first figured out how to implement closures! start = 14:30 end = 16:30 ### ISWIM was never implemented but it inspired PAL at MIT and Gendanken start = 16:00 end = 17:00 ### A problem with Lisp if you're using it to teach lambda calculus is that Lisp has this eval quote business which is really orthogonal to what's going on in the lambda calculus. start = 17:00 end = 21:00 ### SASL was consciously designed based on the lambda calculus and it has multi level pattern matching which really increases readability start = 19:00 end = 21:00