Lambda calculus beta reduction examples plus#
Lambda calculus beta reduction examples free#

The process of reducing more complex applications is quite simple, based on a few rules: Applications are left associative. There are other kinds of notation for variable substitutions, but I find this one quite clear and more familiar for developers, as it reminds of variable assignations. It’s called reduction because the head is consumed (reduced) by substituting its parameter in the body with the value the function was applied to.Įxample: apply the identity function to 3.

The process of evaluating (reducing) a lambda expression is known as beta reduction. Every time we rename a parameter in one of our functions, we are applying this concept. Is alpha equivalence something really new for developers? I don’t think so.

Lambda calculus beta reduction examples free#

This makes sense because different free variables can mean different things and they are irreducible, so they aren’t equivalent in the context of a function. This is important when there are name clashes during beta reduction.įree variables cannot be substituted if we want to preserve alpha equivalence. These alpha-equivalent functions could be used instead of the other ones, and the result, when evaluating the expression, would still be the same. In simple terms, this means that we can use different variable names for the same function as long as we preserve their meaning in the body of the function. Two expressions are alpha-equivalent if they can be obtained from each other in other words, if replacing the bound variables with other variables gives us back an equivalent expression. In this process, also called evaluation, two new concepts are involved: Alpha Equivalence Later on, we will want to reduce these expressions in order to get the value they produce. We’ve talked about expressions, which are used to create more complex abstractions (or functions). The variable z does not appear in the head, therefore it cannot be bound and substituted in the scope of the function. This has some implications during the evaluation of the function. Their scope is not local to the function.

Their values are defined outside of the function they are referenced in. They appear in the body, but not in the head. Nothing strange so far we use functions and variables substitution every day when coding.Īnother type of variable are free variables. We will see this process in more detail later. When the lambda is applied to the 3 parameter, the x variable is substituted with this value in the body. These kinds of variables are called bound variables. When applying the function to an expression, the occurrences of the variable in the body are substituted with the applied expression. We have seen so far functions with one variable in the head. This expression will be evaluated and reduced until an irreducible term is obtained (we will explain this process later). 3 is the parameter the function is applied to. (λx.x) is a function, as we have seen in the previous example. An example of a simple expression could look like the following: The reason is that they allow us to generalize a computation and reuse it for the different values of the variable (or parameter).Įxpressions are evaluated until an irreducible term is obtained as a result. This example is the identity function.įunctions are also known as abstractions. Λx is the head, the second x is the body, and the dot symbol (.) separates both. As we will see later, functions have only one parameter.

Lambda calculus beta reduction examples plus#

The head is a lambda plus a variable, and the body is an expression. Variables are not the ones we use to temporarily store values in imperative languages variables in Lambda Calculus are the parameters of functions.įunctions consist of a head and a body. Lambda Calculus is based on three basic building blocks: expressions, variables, and functions, which are combined to form other expressions. It is the most reducible form of all Functional Programming languages the primitive building block of Functional Programming. We use Lambda Calculus every day when we program.

Lambda Calculus sounds like an arcane term that only functional programming wizards can understand.