COMS W4115
Programming Languages and Translators
Lecture 21: April 13, 2015
Introduction to the Lambda Calculus

Outline

1. History of the lambda calculus and functional programming languages
2. CFG for the lambda calculus
3. Function abstraction
4. Function application
5. Free and bound variables
6. Beta reductions
7. Evaluating a lambda expression
8. Currying
9. Renaming bound variables by alpha reduction
10. Eta conversion
11. Substitutions
12. Disambiguating lambda expressions
13. Normal form
14. Evaluation strategies

1. History of the Lambda Calculus and Functional Programming Languages

• The lambda calculus was introduced in the 1930s by Alonzo Church at Princeton University as a mathematical system for defining computable functions.
• The lambda calculus is equivalent in definitional power to that of Turing machines.
• The lambda calculus serves as the theoretical model for functional programming languages and has applications to artificial intelligence, proof systems, and logic.
• Lisp was developed by John McCarthy at MIT in 1958 around the lambda calculus.
• ML, a general-purpose functional language, was developed by Robin Milner at the University of Edinburgh in the early 1970s. Caml and OCaml are dialects of ML developed at INRIA in 1985 and 1996, respectively.
• Haskell, considered by many as one of the purest functional programming languages, was developed by Simon Peyton Jones, Paul Houdak, Phil Wadler and others in the late 1980s and early 90s.
• Many legacy languages including C++ and Java have incorporated features from the lambda calculus such as lambda expressions.
• Because of its simplicity, the lambda calculus is a useful tool for the study and analysis of programming languages.

2. CFG for the Lambda Calculus

• The central concept in the lambda calculus is an expression which we can think of as a program that when evaluated returns a result consisting of another lambda calculus expression.
• Here is the grammar for lambda expressions:

expr → λ variable . expr | expr expr | variable | ( expr ) | constant

• A variable is an identifier.
• A constant is a built-in function such as addition or multiplication, or a constant such as an integer or boolean. However, as we shall see, all programming language constructs can be represented as functions with the pure lambda calculus so these constants are unnecessary. However, we will use some constants for notational simplicity.

3. Function Abstraction

• A function abstraction, often called a lambda abstraction, is a lambda expression that defines a function.
• A function abstraction consists of four parts: a lambda followed by a variable, a period, and then an expression as in λx.expr.
• In the function abstraction λx.expr the variable x is the formal parameter of the function and expr is the body of the function.
• For example, the function abstraction λx. + x 1 defines a function of x that adds x to 1. Parentheses can be added to lambda expressions for clarity. Thus, we could have written this function abstraction as λx.(+ x 1) or even as (λx. (+ x 1)).
• In C this function definition might be written as

int addOne (int x)
{
  return (x + 1);
}

• Note that unlike C the lambda abstraction does not give a name to the function. The lambda expression itself is the function.
• We say that λx.expr binds the variable x in expr and that expr is the scope of the variable.

4. Function Application

• A function application, often called a lambda application, consists of an expression followed by an expression: expr expr. The first expression is a function abstraction and the second expression is the argument to which the function is applied. All functions in lambda calculus have exactly one argument. Multiple-argument functions are represented by currying, which we shall explain below.
• For example, the lambda expression λx. (+ x 1) 2 is an application of the function λx. (+ x 1) to the argument 2.
• This function application λx. (+ x 1) 2 can be evaluated by substituting the argument 2 for the formal parameter x in the body (+ x 1). Doing this we get (+ 2 1). This substitution is called a beta reduction.
• Beta reductions are like macro substitutions in C. To do beta reductions correctly we may need to rename bound variables in lambda expressions to avoid name clashes.
• Function application associates left-to-right; thus, f g h = (f g)h.
• Function application binds more tightly than λ; thus, λx. f g x = (λx. (f g)x).
• Functions in the lambda calculus are first-class citizens; that is to say, functions can be used as arguments to functions and functions can return functions as results.

5. Free and Bound Variables

• In the function definition λx.x the variable x in the body of the definition (the second x) is bound because its first occurrence in the definition is λx.
• A variable that is not bound in expr is said to be free in expr. In the function (λx.xy), the variable x in the body of the function is bound and the variable y is free.
• Every variable in a lambda expression is either bound or free. Bound and free variables have quite a different status in functions.
• In the expression (λx.x)(λy.yx):
• The variable x in the body of the leftmost expression is bound to the first lambda.
• The variable y in the body of the second expression is bound to the second lambda.
• The variable x in the body of the second expression is free.
• Note that x in second expression is independent of the x in the first expression.
• In the expression (λx.xy)(λy.y):
• The variable y in the body of the leftmost expression is free.
• The variable y in the body of the second expression is bound to the second lambda.
• Given an expression e, the following rules define FV(e), the set of free variables in e:
• If e is a variable x, then FV(e) = {x}.
• If e is of the form λx.y, then FV(e) = FV(y) - {x}.
• If e is of the form xy, then FV(e) = FV(x) ∪ FV(y).
• An expression with no free variables is said to be closed.

6. Beta Reductions

• A function application λx.e f is evaluated by substituting the argument f for all free occurrences of the formal parameter x in the body e of the function definition.
• We will use the notation [f/x]e to indicate that f is to be substituted for all free occurrences of x in the expression e.
• Examples:
1. (λx.x)y → [y/x]x = y.
2. (λx.xzx)y → [y/x]xzx = yzy.
3. (λx.z)y → [y/x]z = z since the formal parameter x does not appear in the body z.
• This substitution in a function application is called a beta reduction and we use a right arrow to indicate it.
• If expr1 → expr2, we say expr1 reduces to expr2 in one step.
• In general, (λx.e)f → [f/x]e means that applying the function (λx.e) to the argument expression f reduces to the expression [f/x]e where the argument expression f is substituted for the function's formal parameter x in the function body e.
• A lambda calculus expression (aka a "program") is "run" by computing a final result by repeatly applying beta reductions. We use →* to denote the reflexive and transitive closure of →; that is, zero or more applications of beta reductions.
• Examples:
1. (λx.x)y → y (illustrating that λx.x is the identity function).
2. (λx.xx)(λy.y) → (λy.y)(λy.y) → (λy.y); thus, we can write (λx.xx)(λy.y) →* (λy.y). Note that here we have applied a function to a function as an argument and the result is a function.

7. Evaluating a Lambda Expression

• A lambda calculus expression can be thought of as a program which can be executed by evaluating it. Evaluation is done by repeatedly finding a reducible expression (called a redex) and reducing it by a function evaluation until there are no more redexes.
• Example 1: The lambda expression (λx.x)y in its entirety is a redex that reduces to y.
• Example 2: The lambda expression (+ (* 1 2) (- 4 3)) has two redexes: (* 1 2) and (- 4 3). If we choose to reduce the first redex, we get (+ 2 (- 4 3)). We can then reduce (+ 2 (- 4 3)) to get (+ 2 1). Finally we can reduce (+ 2 1) to get 3.
• Note that if we had chosen the second redex to revaluate first, we would have ended up with the same result:
(+ (* 1 2) (- 4 3)) → (+ (* 1 2) 1) → (+ 2 1) → 3.

8. Currying

• All functions in the lambda calculus are prefix and take exactly one argument.
• If we want to apply a function to more than one argument, we can use a technique called currying that treats a function applied to more than one argument to a sequence of applications of one-argument functions. For example, to express the sum of 1 and 2 we can write (+ 1 2) as ((+ 1) 2) where the expression (+ 1) denotes the function that adds 1 to its argument. Thus ((+ 1) 2) means the function + is applied to the argument 1 and the result is a function (+ 1) that adds 1 to its argument: (+ 1 2) = ((+ 1) 2) → 3

9. Renaming Bound Variables by Alpha Reduction

• The name of a formal parameter in a function definition is arbitrary. We can use any variable to name a parameter, so that the function λx.x is equivalent to λy.y and λz.z. This kind of renaming is called alpha reduction.
• Note that we cannot rename free variables in expressions.
• Also note that we cannot change the name of a bound variable in an expression to conflict with the name of a free variable in that expression.

10. Eta Conversion

• The two lambda expressions (λx.+ 1 x) and (+ 1) are equivalent in the sense that these expressions behave in exactly the same way when they are applied to an argument -- they add 1 to it. η-conversion is a rule that expresses this equivalence.
• In general, if x does not occur free in the function F, then (λx.F x) is η-convertible to F.

11. Substitutions

• For a beta reduction, we introduced the notation [f/x]e to indicate that the expression f is to be substituted for all free occurrences of the formal parameter x in the expression e:
(λx.e) f → [f/x]e
• To avoid name clashes in a substitution [f/x]e, first rename the bound variables in e and f so they become distinct. Then perform the textual substituion of f for x in e.
• For example, consider the substitution [y(λx.x)/x] λy.(λx.x)yx.
• After renaming all the bound variables to make them all distinct we get [y(λu.u)/x] λv.(λw.w)vx.
• Then doing the substitution we get λv.(λw.w)v(y(λu.u)).
• The rules for substitution are as follows. We assume x and y are distinct variables, and e, f and g are expressions.
• For variables
   [e/x]x = e
   [e/x]y = y
• For function applications
   [e/x](f g) = ([e/x]f) ([e/x]g)
• For function abstractions
   [e/x](λx.f) = λx.f
   [e/x](λy.f) = λy.[e/x]f, provided y is not free in e (this is called the "freshness" condition).
• Examples:
1. [y/y](λx.x) = λx.x
2. [y/x]((λx.y) x) = ([y/x](λx.y)) ([y/x]x) = (λx.y)y
3. Note that the freshness condition does not allow us to make the substitution [y/x](λy.x) = λy.([y/x]x) = λy.y because y is free in the expression y.

12. Disambiguating Lambda Expressions

• The grammar we gave in section 4 for lambda expressions is ambiguous. A few simple rules will remove the ambiguities.
• Function application is left associative: f g h = ((f g) h)
• Function application binds more tightly than lambda: λx.f g x = (λx.(f g) x)
• The body in a function abstraction extends as far to the right as possible: λx. + x 1 = λx. (+ x 1).

13. Normal Form

• An expression containing no possible beta reductions is said to be in normal form. A normal form expression is one containing no redexes.
• Examples of normal form expressions:
• x where x is a variable.
• x e where x is a variable and e is a normal form expression.
• λx.e where x is a variable and e is a normal form expression.
• The expression (λx.x x)(λx.x x) does not have a normal form because it always evaluates to itself. We can think of this expression as a representation for an infinite loop.
• The expression (λx. λy. y)((λz.z z)(λz.z z)) can be reduced to the normal form λy.y.

14. Evaluation Strategies

• An evaluation strategy specifies the order in which beta reductions for a lambda expression are made.
• Some reduction orders for a lambda expression may yield a normal form while other orders may not. For example, consider the given expression
(λx.1)((λx.x x)(λx.x x))
This expression has two redexes:
1. The entire expression is a redex in which we can apply the function (λx.1) to the argument ((λx.x x)(λx.x x)) to yield the normal form 1. This redex is the leftmost outermost redex in the given expression.
2. The subexpression ((λx.x x)(λx.x x)) is also a redex in which we can apply the function (λx.x x) to the argument (λx.x x). Note that this redex is the leftmost innermost redex in the given expression. But if we evaluate this redex we get same subexpression: (λx.x x)(λx.x x) → (λx.x x)(λx.x x). Thus, continuing to evaluate the leftmost innermost redex will not terminate and no normal form will result.
• There are two common reduction orders for lambda expressions: normal order evaluation and applicative order evaluation.
Normal order evaluation
• In normal order evaluation we always reduce the leftmost outermost redex at each step.
• The first reduction order above is a normal order evaluation.
• A remarkable property of lambda calculus is that every lambda expression has a unique normal form if one exists. Moreover, if an expression has a normal form, then normal order evaluation will always find it.
Applicative order evaluation
• In applicative order evaluation we always reduce the leftmost innermost redex at each step.
• The second reduction order above is an applicative order evaluation.
• Thus, even though an expression may have a normal form, applicative order evaluation may fail to find it.

15. Practice Problems

1. Evaluate (λx. λy. + x y)1 2.
2. Evaluate (λf. f 2)(λx. + x 1).
3. Evaluate (λx. (λx. + (* x 1)) x 2) 3.
4. Evaluate (λx. λy. + x((λx. * x 1) y))2 3.
5. Is (λx. + x x) η-convertible to (+ x)?
6. Show how all bound variables in a lambda expression can be given distinct names.
7. Construct an unambiguous grammar for lambda calculus.

16. References

• Simon Peyton Jones, The Implementation of Functional Programming Languages, Prentice-Hall, 1987.
• Benjamin C. Pierce, Types and Programming Languages, The MIT Press, 2002.
• Stephen A. Edwards: The Lambda Calculus  
• http://www.inf.fu-berlin.de/lehre/WS01/ALPI/lambda.pdf
• http://www.soe.ucsc.edu/classes/cmps112/Spring03/readings/lambdacalculus/project3.html