Lambda calculus (or -calculus) was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s to describe functions in an unambiguous and compact manner. Many real languages are based on the lambda calculus, including Lisp, Scheme, Haskell, and ML. A key characteristic of these languages is that functions are values, just like integers and booleans are values: functions can be used as arguments to functions, and can be returned from functions. The name “lambda calculus” comes from the use of the Greek letter lambda () in function definitions. (The letter lambda has no significance.) “Calculus” means a method of calculating by the symbolic manipulation of expressions. Intuitively, a function is a rule for determining a value from an argument. Some examples of functions in mathematics are
Syntax
The pure -calculus contains just function definitions (called abstractions), variables, and function application (i.e., applying a function to an argument). If we add additional data types and operations (such as integers and addition), we have an applied -calculus. In the following text, we will sometimes assume that we have integers and addition in order to give more intuitive examples.
The syntax of the pure -calculus is defined as follows. An abstraction is a function: variable is the argument, and expression is the body of the function. Note that the function doesn’t have a name. Assuming we have integers and arithmetic operations, the expression is a function that takes an argument and returns the square of .
An application requires that is (or evaluates to) a function, and then applies the function to the expression . For example, is, intuitively, equal to 25, the result of applying the squaring function to 5. Here are some examples of lambda calculus expressions. Lambda expressions extend as far to the right as possible. For example is the same as 𝜆𝑥. 𝑥 (𝜆𝑦. 𝑦), and is not the same as . Application is left associative. For example is the same as . In general, use parentheses to make the parsing of a lambda expression clear if you are in doubt.
Variable binding and 𝛼-equivalence
An occurrence of a variable in an expression is either bound or free. An occurrence of a variable 𝑥 in a term is bound if there is an enclosing ; otherwise, it is free. A closed term is one in which all identifiers are bound.
Consider the following term: Both occurrences of are bound, the first occurrence of is bound, the is free, and the last is also free, since it is outside the scope of the .
If a program has some variables that are free, then you do not have a complete program as you do not know what to do with the free variables. Hence, a well formed program in lambda calculus is a closed term.
The symbol is a binding operator, as it binds a variable within some scope (i.e., some part of the expression): variable is bound in in the expression .
he name of bound variables is not important. Consider the mathematical integrals and . They describe the same integral, even though one uses variable 𝑥 and the other uses variable 𝑦 in their definition. The meaning of these integrals is the same: the bound variable is just a placeholder. In the same way, we can change the name of bound variables without changing the meaning of functions. Thus is the same function as . Expressions and that differ only in the name of bound variables are called -equivalent, sometimes written .
Higher-order functions
In lambda calculus, functions are values: functions can take functions as arguments and return functions as results. In the pure lambda calculus, every value is a function, and every result is a function!
For example, the following function takes a function as an argument, and applies it to the value 42. This function takes an argument and returns a function that applies its own argument (a function) to .
Semantics
𝛽-equivalence
Application applies the function to . In some ways, we would like to regard the expression as equivalent to the expression where every (free) occurrence of 𝑥 is replaced with . For example, we would like to regard as equivalent to 。
We write to mean expression 𝑒1 with all free occurrences of 𝑥 replaced with 𝑒2. There are several different notations to express this substitution, including (used by Pierce), (used by Mitchell), and (used by Winskel).
Using our notation, we would like expressions and to be equivalent. We call this equivalence, between and , is called -equivalence. Rewriting into is called a -reduction. Given a lambda calculus expression, we may, in general, be able to perform 𝛽-reductions. This corresponds to executing a lambda calculus expression.
There may be more than one possible way to -reduce an expression. Consider, for example, . We could use -reduction to get either or . The order in which we perform 𝛽-reductions results in different semantics for the lambda calculus.
Call-by-value
Call-by-value (or CBV) semantics makes sure that functions are only called on values. That is, given an application , CBV semantics makes sure that is a value before calling the function. So, what is a value? In the pure lambda calculus, any abstraction is a value. Remember, an abstraction is a function; in the pure lambda calculus, the only values are functions. In an applied lambda calculus with integers and arithmetic operations, values also include integers. Intuitively, a value is an expression that can not be reduced/executed/simplified any further. We can give small step operational semantics for call-by-value execution of the lambda calculus. Here, can be instantiated with any value (e.g., a function). We can see from these rules that, given an application , we first evaluate until it is a value, then we evaluate until it is a value, and then we apply the function to the value--a -reduction.
Let’s consider some examples. (These examples use an applied lambda calculus that also includes reduction rules for arithmetic expressions.)
Call-by-name
Call-by-name (or CBN) semantics applies the function as soon as possible. The small step operational semantics are a little simpler, as they do not need to ensure that the expression to which a function is applied is a value. Let’s consider the same examples we used for CBV.
Note that the answers are the same, but the order of evaluation is different. (Later we will see languages where the order of evaluation is important, and may result in different answers.)
