![]() 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 |