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.
#Lambda calculus how to#
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 kommentar(er)
