Introducing Lambda Calculus: Spilling the HoTT

[00:02] you've just watched an awesome scene from an anime read a great passage from from an anime read a great passage from a book or enjoyed a particular Meme and then when you go to talk about it with your friends you realize that without

[00:14] all the context that moment just won't land then you have to explain the entire backstory for it to make sense for me that's a laville fixed Point theorem an awesome mathematical concept that unifies Cano's theorem go Bell's

[00:30] incompleteness theorem and the undecidability of the halting problem that's right you get three I say three of the most important results in mathematics all for the price of one but what's more if you order now you also

[00:44] get keen's recursion theorem Roger fixo theorem and Curry's Paradox absolutely theorem and Curry's Paradox absolutely free I'm sorry something just overcame me however to do lille's fix Point theorem Justice I would need a model of

[01:01] computing most likely Lambda calculus because I'm a functional programming hipster type I guess I'll have to do hipster type I guess I'll have to do explaining L Val's fix Point theorem

[01:14] sometime later I know that there's a new field of mathematics right on The field of mathematics right on The Cutting Edge called homotopy type Theory a part of mathematics where new discoveries and theorems are being made

[01:28] homotopy type Theory it's a real mouthful to say so let's contract that mouthful to say so let's contract that to hot tea which isn't such a mouthful since you tend to sip it most of current mathematics sits a top a foundation

[01:43] mathematics sits a top a foundation based on zfc set theory or at least it based on zfc set theory or at least it pretends to type theory is an alternative foundation for mathematics it has the advantage that computer-based

[01:57] it has the advantage that computer-based theorem provs are very well suited for type based systems and Mathematics can leverage all the great work that computer scientists and compiler Engineers have done as well the

[02:12] mathematicians can contribute their own expertise to the field of computer science and compiler engineering it's so new and shiny that we don't even know if

[02:24] hot tea will be the type theory that becomes the foremost type Theory type becomes the foremost type Theory type Theory and hot tea also depend on Lambda calculus while we are discussing using computers and Mathematics there is also

[02:40] the computable reals a way to have most of the useful properties of the of the useful properties of the so-called real numbers but without the numbers having an infinite information density and ex and imploding your brain

[02:55] into a black hole what your brain hasn't been imploded into a black hole perhaps that was because you actually using computable reels and just pretending that they were the complete ordered field computable reels are a useful

[03:09] field computable reels are a useful subset of the reels that avoids most of the weird paradoxes you get with them by replacing them with a whole lot of other weird properties to do computable reels Justice again I'm going to need a model

[03:23] of computing so Lambda calculus or something equivalent yeah I think I'm going to have to do Lambda calculus Lambda calculus isn't a boring meal that you have to eat in order to get dessert It's a Wonderful enlightening subject

[03:40] all to itself so here is what I'm going to do since Lambda calculus is the root of all of these ideas this video will be the root of a tree of videos each

[03:53] exploring an application of Lambda calculus

[04:06] oversimplified mathematical models of reality and honestly is it even a real science if you don't have a mathematical model yes of course it is but having a chauvinistic disdain towards less mathematical stem subjects is both

[04:22] mathematical stem subjects is both slightly humorous and also perpetuates a slightly humorous and also perpetuates a deeply toxic interdistance ten rivalry to the overall detriment of society in Newtonian physics you have

[04:36] frictionless balls engaging in elastic collisions in a vacuum in chemistry you have the ball and stick models of molecules and in geoscience the earth is

[04:48] often simplified into a sphere rather than the oblake spheroid that it really is have you ever noticed that science seems overly obsessed with ball in computer science we want to be able

[05:02] in computer science we want to be able to reason about computers comp size to reason about computers comp size needs a simple mathematical model that allows us to work with computer science that can apply to all computers

[05:15] regardless of Hardware it would be kind of a hassle if we had to reinvent all of computer science every time somebody invented a new bit of Hardware it should

[05:27] be Universal the only time computer scientists go into Hardware based details as if it would result in a great idea for a paper or a conference talk or

[05:39] idea for a paper or a conference talk or if they're really lucky a startup in mature Fields the mathematical models you use are pretty settled however you use are pretty settled however compai is a very young field so there

[05:52] are many competing models you have probably heard of touring machines conceived by the great Alan touring in order to solve the halting problem that I casually mentioned before a touring machine is basically a finite State

[06:08] automata strapped to a real tooreal tape machine if you want to learn more about finite State automata I've got a great video for that this way of modeling Computing is a very bottom up Hardware oriented model of computing you can

[06:25] build physical models of touring machines well at least in theory the mathematically ideal touring machine has an infinite long tape which is kind of

[06:39] an infinite long tape which is kind of Impractical however there is also a topdown model of computing for those who are really into abstraction in Lambda are really into abstraction in Lambda calculus all Computing is simulated as a

[06:53] calculus all Computing is simulated as a system of text substitution rules now I am sure you have received a document like this dear title first name last name you have not paid your bill of amount to not a scam Incorporated please

[07:09] send payment before we start legal actions yours not a scam Incorporated actions yours not a scam Incorporated where the title first name Etc have been replaced with scraped copies of something resembling your personal D

[07:24] details times you can even get letters like this from legitimate business like this from legitimate business even if you have been fortunate never to receive a bill in your life you are watching this on YouTube Modern websites

[07:40] like YouTube basically work on this principle of substitution as well you have a basic template of what the web page looks like and then the details for page looks like and then the details for each page are substituted based on

[07:54] entries in a database there are two Styles these templates can be rep Styles these templates can be rep presented in Lambda calculus Lambda name presented in Lambda calculus Lambda name the Lambda symbol made famous by

[08:07] halflife 2 followed by the name of the variable that will be substituted a period as a separator and then the string the text will be copied into there is an alternative more compact way

[08:22] of writing this where you have the variable name introduced the barred Arrow to indicate map to and what follows is the template to substitute into now if you have done some programming you might recognize this as

[08:39] being a little bit like a function declaration although it doesn't give the function a name that's why in some places these Lambda expressions are also

[08:51] called Anonymous functions an anonymous function of course is just a fancy name for a masquerade ball but e even more technically Lambda expressions are not always really functions but they act a lot like functions and I just call them

[09:09] functions anyway the reason why they are not functions is a bit of a spoiler for later in the video in this system you can apply this function by

[09:22] concatenating a value after it the brackets are there to remove any ambiguity from where the body of the function ends and the value I will be substituting in starts this type of substitution is

[09:39] starts this type of substitution is called beta reduction if we apply beta reduction until we can reduce no more then we get what is called the canonical then we get what is called the canonical form it might sound strange but this

[09:53] repeated beta reduction is all you need to do computation there's also Al a process called Alpha conversion that we can change the name of a variable to

[10:05] another name as long as we change all of the variables that are bound together the variables that are bound together Alpha conversion is done to ensure that variables that coincidentally have the same name won't Collide this is to

[10:21] ensure that the variable has a thing called lexical scope if you want to PA the Lambda expressioned into its grammatical components it will create a

[10:34] PA tree and the variables will be bound to the Declaration that it is directly under in the pass tree a new variable being introduced with the same name Will

[10:46] being introduced with the same name Will Shadow or mask the variables above it in the tree don't worry we're going to do some examples and that should help we can Nest the Lambda expression to create create a function that has multiple

[11:02] create a function that has multiple arguments the arrows and the shading should show you how the variable Mark the variables abound and the scope of each variable again if we pause this into a tree you can see how the scoping

[11:17] of the variable and the PA tree lines up a new variable name is introduced in the abstraction node and has scope to everything below it application node

[11:29] noes are where the functions are called and variable nodes are places where on application the input parameters will be replaced this style of tree is called an

[11:42] replaced this style of tree is called an abstract syntax tree this trick of using abstract syntax tree this trick of using nested Expressions to have multiple arguments is called currying and is one of the most spicy aspects of Lambda

[11:56] of the most spicy aspects of Lambda calculus to make this trick work cleanly it's also handy to have Lambda Expressions work as being left Expressions work as being left associative that is the leftmost pairs

[12:11] are evaluated first so if we have an expression like this the pair of on the expression like this the pair of on the left will be evaluated first then the next one across and then the final one you can force a different order by

[12:28] making use of bracketing but I said these Expressions could be used for these Expressions could be used for computing so how is that

[12:42] video then you might already have heard about church encoding in passing so how do we represent numbers as functions you use a number function that applies

[12:54] use a number function that applies another that applies another function another that applies another function some number of times oh that colon three line thing is defined as in this version of Lambda calculus it's just an easy

[13:09] of Lambda calculus it's just an easy nickname to simplify complex formation also to keep them separated from also to keep them separated from variable names these aliases will start

[13:21] variable names these aliases will start with a capital letter we can read this as one takes the function f and an argument for that function X then applies that function to the argument once we are just getting

[13:35] started so let's do two to get the hang of it two takes a function f and an argument for that function X applies that function f to the argument F then

[13:47] applies the function again to what was just returned in other words it applies the same function twice and what is a number system without a zero something

[14:00] number system without a zero something positively medy eval zero just Returns positively medy eval zero just Returns the argument without applying the function so zero takes the function and does nothing with it returning the

[14:14] original argument unchanged of course having numbers isn't very useful unless we can do something with those numbers let's start with addition for addition we going are going to need a function that takes two addin

[14:31] to need a function that takes two addin we also know that returns a number which we also know that returns a number which takes two arguments then we can apply takes two arguments then we can apply the function f m times and then take the

[14:44] the function f m times and then take the return value of that and apply it n return value of that and apply it n times let's try that out right

[15:33] and we have successfully shown that 1 + 1 equal 2 in much less than 360 Pages now that might have been a little difficult to follow so let's do it again difficult to follow so let's do it again this time using an abstract syntax tree

[16:16] obvious whenever we have an application node whose left child is an abstraction we replace every instance of that variable it's also Poss possible to

[16:29] variable it's also Poss possible to Define expressions for successor multiplication and the predecessor function I'm not going to go over all of those in detail because this is meant to be an introduction to Lambda calculus I

[16:44] suggest you look up church encodings for them on a resource like Wikipedia them on a resource like Wikipedia numbers and basic operations on numbers aren't really enough to do Computing we also need logic and that's what we have

[16:58] also need logic and that's what we have have the church booleans for named for have the church booleans for named for George Bull and his wife and editor Mary Everest bull here are the functions that act as bullin true takes two functions

[17:14] and Returns the first argument and false takes two functions and Returns the second these basically act a little bit like an if then statement with the true

[17:26] Bing returning the then part and the false Bing returning the else part for false Bing returning the else part for example you could Implement not as this

[17:38] you can see if we call this with the true argument it will return false and if pass a false argument it will return true also you might have noticed that

[17:50] true also you might have noticed that false looks exactly like zero this sort of coincidence might end up being a symptom of a problem that comes up later on these are fun so far let's Implement logical and the operator that is true if

[18:08] logical and the operator that is true if both inputs are true and false in all both inputs are true and false in all other situations we can simply translate that truth table into a Lambda expression there are a few easy ways to

[18:23] expression there are a few easy ways to simplify this further with and and not you can implement every other logical operation for logic to be useful though

[18:35] we need a way to probe the rest of the universe and bring data Into The Logical universe and bring data Into The Logical realm we need predicates is zero is one realm we need predicates is zero is one of the easiest predicates to do in

[18:49] Lambda calculus this takes a number and returns true if the number is zero and returns true if the number is zero and false otherwise we basically use the property of zero it always returns the second argument unchanged so for zero

[19:06] true will be returned and when we use any other value false will be returned any other value false will be returned we have almost everything we need to do Computing we have logic we have numbers we have operations on numbers we even

[19:22] we have operations on numbers we even have a way to do Loop operations a set number of times we just use the number as it as a function what we don't have as it as a function what we don't have is a way of doing a loop until some

[19:38] condition is satisfied in order to do that we have to make use of one of the that we have to make use of one of the most powerful tools mathematics has recursion the ability of a function to call itself General recursion is a

[19:55] prerequisite for computing the power of General recursion unfortunately makes General recursion unfortunately makes this Lambda calculus unsuitable to act as a foundation for mathematics this isn't an this is not an accident or

[20:11] coincidence there exists thresholds of expressive power which when crossed become incomplete in predict unpredictable and even un sound however

[20:24] that is a topic of a future video as I'll be saying it quite a few times at this point all I have is explain how you can turn Lambda inside out with Y the

[20:37] can turn Lambda inside out with Y the fixed point combinator if we feed the Y combinator uh dummy function first we expand out Y into its canonical form then we apply beta reduction replacing all the fs with G's we then apply beta

[20:55] reduction again this time replacing all all the x's in the first Clause with the all the x's in the first Clause with the second Clause now if you look at the argument to G here you will notice that it looks exactly like the second line

[21:11] which we have already shown is equal to YG so we can replace that with YG and we have ourself a selfing fixed point and a restaurant for

[21:25] selfing fixed point and a restaurant for your Mexican style food your Mexican style food you can see how it ends up with G being you can see how it ends up with G being passed into G this is a type of fixed

[21:37] point where the function going in is the same as the function going out I always same as the function going out I always find examples to be helpful so let's try find examples to be helpful so let's try and implement the factorial so how would

[21:52] you implement this the easiest way is to make use of what I call the recursive algorithm algorithm this method allows you to work out how to create a recursive algorithm for even the most complex of tasks in this method first

[22:10] you try to solve the simplest case this is your base case then you work out a way to take a step towards your base case this is your recursive or inductive

[22:23] step so for factorial we will need to start with some basic boiler plate since it's recursive we know it's going to use the Y combinator and the function we

[22:36] will that we will pass into the Y combinator is going to receive itself as the first argument with factorial we know the next argument will be the number we will be factorial liing now the base case of factorial is

[22:54] zero which is one since we have the zero predicate it's quite easy to do this for the true branch of the Boolean we return one for

[23:06] the recursive step we have to start with the N value and then we reduce it down the N value and then we reduce it down to the n n - one case for factorial this

[23:18] to the n n - one case for factorial this is the n * nus factorial in our Lambda is the n * nus factorial in our Lambda calculus implementation we multiply M with the results of our recursive step so let's try this with three

[24:11] [Applause] [Music]

[25:20] we can Define pairs once we have pairs of values we can Define whole numbers as pairs of the counting numbers that we've constructed using Church numerals then constructed using Church numerals then we can have rational numbers as pairs of

[25:35] whole numbers the numerator and the denominator we can also Define lists as denominator we can also Define lists as nested pairs defining real numbers is a little bit more complicated and will be the topic of its own video we can also

[25:53] the topic of its own video we can also treat numbers as characters using treat numbers as characters using Unicode and if we have a list of characters that allows us to make strings it's even possible for these

[26:07] strings to be the string repres representation of Lambda Expressions we could even go super meta we can write a Lambda expression that will take a string pause it evaluate the lamb

[26:22] string pause it evaluate the lamb expression and return that expression's expression and return that expression's canonical form we you could even write a Lambda expression that when reduced will totally emulate a touring machine

[26:36] basically Lambda Expressions can perform any algorithm that a computer can perform and any computer given sufficient time and memory can emulate

[26:49] sufficient time and memory can emulate any Lambda Lambda expressions are not really functions well functions are supposed to

[27:02] be total this means for every input there is a corresponding output however you can make a Lambda expression like this one which will run forever and this one which will run forever and never ever settle down to a real value

[27:17] never ever settle down to a real value this is unfortunately true for every this is unfortunately true for every model of computing you can't build an uncrashable computer being a able to crash is simply an inherent part of

[27:32] being a computer this is something that unfortunately makes Lambda calculus inappropriate as a foundation for mathematics as any architect will tell

[27:45] you a collapsable Foundation is bad for building there is another problem that building there is another problem that makes this style of Lambda calculus mathematical perspect perspective and as a computer language I

[28:02] talked about functions taking numbers as inputs or booing or even strings however this is just enforced by convention there is nothing to stop us passing a

[28:14] number into a function meant for a bulling or for us to try and add two bulling or for us to try and add two bulling together it is trivially easy to bulling together it is trivially easy to write programs that are total nonsense

[28:26] this is the limitation of of this style of Lambda calculus called the untyped Lambda calculus untyped should not be confused with fake type which is a Japanese electro swing band but if this is untyped Lambda calculus can we have a

[28:43] is untyped Lambda calculus can we have a typed Lambda calculus yes and that will typed Lambda calculus yes and that will be our next video