In the previous section, when we were applying one lambda expression to the other we were essentially performing a β-reduction. In this case, we substitute x by 2:īeta-reductions, Beta-reduxes, and The Beta-normal FormĪ β-reduction is a step in the execution of a function. Now that we know this, let’s substitute x in an expression which adds 1 to the number passed to it. The syntax for substitution is: Expression. We’ll see how it does that in a next post, for now just trust that the + function adds two numbers (it is curried, of course). When you do a sum in Lambda Calculus you do not write it as a + b, you write it as + a b instead, because in fact, + is just the name of a function which performs addition. Substituting allows us to replace a bound variable’s name with an expression.Īfter so long, it’s finally about time we destroy a sweet illusion we’ve had for so long so that I can explain this. a b so I chose to rename the bound variable b in λa. Notice that in the example above we would not have been able to rename the free variable b in λa. a b), for example, you can obtain the α-equivalent expression ((λa. If you perform an alpha reduction in ((λa. When you perform renamings so that there are no more repeated variable names you’ve done an alpha-reduction. Renaming variables is important in order to reduce confusion so that you can easily know which variables are bound to which terms. Now let’s rename a few variables in the lambda expression λx. The syntax for substituting a variable is Expression. Since this does not change what an expression does, you might have already come to the conclusion that by doing this we can obtain α-equivalent expressions. Given a certain lambda expression, renaming allows us to replace the bound variables names by other names. If you still think you cannot identify each case easily, once again I’ll recommend you to read this section about types of variables in the previous post. If we rename that outermost x, which is not free, we’re not changing the semantics of the function in any way.īeing familiar with the concept of bound and free variables is essential for you to understand this post. x are α-equivalent because the x in the inner function is bound to the inner meta-variable x and the outermost metavariable (which coincidently has the same name) is a completely different variable. In the first one we apply x to y and in the second one, we apply y to x. x y are not α-equivalent because even though they have the same variable names, they differ in what they do. x z are not α-equivalent because the free variable y in the first function is not the same one as the free variable z in the second function, even though the bound variable still has the same name. The y is a free variable and didn’t have its name changed. a y are α-equivalent because the only variable name that changed is the name of the bound variable x. The reason why these functions are not α-equivalent is because even though their bodies are the same, in fn1 the variable z is free (it is present in the outermost context) while in fn2 the variable z is bound (it is passed in as an argument, which means it’s bound to the metavariable z). The following functions, for example, are alpha-equivalent: In Lambda Calculus we say that two functions are alpha-equivalent when they vary only by the names of the bound variables. Now, let’s continue our amazing adventure through the fascinating world of logic. This will be perhaps the most practical post of this series and will serve as a basis for us to understand more abstract concepts in the future. In this post we’ll see how to actually evaluate lambda calculus and get to know all the important concepts behind it, such as alpha-equivalence, alpha-reduction, beta-reduction, beta-reduxes, and the beta-normal form, which will allow us to really understand what is going on when a certain expression gets executed. To make sure you’ll have the necessary knowledge about Lambda Calculus’ syntax you will probably want to read the first post in this series before coming back to this one. This is the second blog post in my series about Lambda Calculus. Lucas Fernandes da Costa at London, United Kingdom
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |