If we rename a to b, we get λb.b b, an abstraction that applies its argument to itself-something went wrong here! This new expression has a different meaning because we inadvertently captured the free variable b, making it a bound variable. Consider λa.a b, an abstraction that applies its argument to b. First, the new variable must not occur as a free variable in the body. However, there are two restrictions on alpha-reduction. The parameter is just a placeholder-it’s name doesn’t really matter. For example, λx.x is alpha-equivalent to λn.n. We do this by changing the parameter, including and all its occurrences in the body, to a new letter. There are three methods of reducing expressions, named using the Greek letters alpha, beta, and eta.Īlpha-reduction allows us to rename parameters in abstractions. Reduction is a process guided by a set of simple yet powerful rules, and it is the essential component that allows us to call the λ-calculus a calculus. The heart of the lambda calculus lies in the reduction of expressions. For this reason, we should always be clear if we are talking about the whole expression or just a part of it. Even so, it is equally correct to say that x is a free variable in b x of that expression. If we consider λx.b x as a whole, then x is a bound variable. One final thing to note is that a variable’s freedom depends on the scope being considered. Here we have four distinct variables-one free and three bound-and they all reuse the letter a. To drive the point home, consider the expression a λa.( a λa.( a λa.a)). In these cases, we say that the new bound variable shadows the free variable. When a variable is bound, everything inside the abstraction refers to this new bound variable, regardless of what the variable means outside. Clearly b is a free variable, but what about a? It looks like a occurs three times, but there are actually two distinct variables here! The a that occurs in the abstraction is a bound variable, while the rightmost a is a free variable. Let’s look at some examples: Expressionīe careful with that last example. All variables are free until they are bound in an enclosing abstraction. However, the x in λx.x is not free because the abstraction binds it we call these variables bound variables. A variable by itself, such as x, is always a free variable. When we look at all the variables in a given λ-expression, we classify some as free variables. Abstraction bodies extend as far to the right as possible: λx.( x x) is the same as λx.x x, which is different from the application ( λx.x) x.On the other hand, the parentheses in a ( b c) are necessary to preserve meaning. Applications are left-associative: (( a b) c) is the same as a b c.Outer parentheses are unnecessary: ((( x))) is the same as x.To interpret λ-expressions unambiguously, we need a few conventions: On the other hand, λa.λb.λc.c is a well-formed expression. For example, λx.λ is invalid because the part after the abstraction’s period should be an expression, but λ by itself is not an expression.
Using this recursive definition, we can tell whether any string of characters is a valid λ-expression. If h is an abstraction, then this is like applying a function h to an argument x. An application has the form ( h x) where h and x are expressions.You can think of it as an anonymous function of one parameter x with a function body e. An abstraction has the form λx.e where x must be a variable and e can be any expression.The letter has no purpose other than to distinguish one variable from another. A variable is represented by a letter such as x.There are three types of expressions: variables, abstractions, and applications:
ExpressionsĮverything in the λ-calculus is an expression.
The λ-calculus ( lambda calculus) is one such system, and it is very important in computer science. A calculus is a formal system of calculation or reasoning, usually involving the symbolic manipulation of expressions. Most people think of Newton and Leibniz’s infinitesimal calculus when they hear the word calculus, but the term is actually more general than that. Tuesday, 7 April 2015 Introduction to the λ-calculus Meet your new favourite formal system
0 kommentar(er)
