22.1. Syntax of the Lambda Calculus¶
22.1.1. Lambda Calculus¶
The lambda calculus (also written as \(\lambda\)-calculus, where lambda is the name of the Greek letter \(\lambda\)) was created by Alonzo Church in the early 1930s to study which functions are computable. In addition to being a concise yet powerful model in computability theory, the lambda calculus is also the simplest functional programming language. So much so that the lambda calculus looks like a toy language, even though it is (provably!) as powerful as any of the programming languages being used today, such as JavaScript, Java, C++, etc.
Programs in the lambda calculus are called lambda expressions (abbreviated \(\lambda exp\)), of which there are only three kinds. In fact, here is a complete BNF grammar for the lambda calculus:
This BNF grammar tells us that expressions in the lambda calculus come in one of three flavors:
A variable (the first production above): typically, we will use a single letter, with an optional integer subscript, to denote a variable. So, \(x, y, a_1\), and \(p_2\) are examples of variables.
A function abstraction (the second production above): this type of \(\lambda\) expressions, also called a lambda abstraction, corresponds to a function definition, which contains two components: the formal parameter of the function (there must be exactly one parameter, namely the \(< var >\) non-terminal in the second production above) and the body of the function (namely the \(<\lambda exp >\) non-terminal in the same production). So, for example, \(\lambda x.y\) is the function whose formal parameter is \(x\) and whose body is \(y\). Note that the non-terminal \(<var>\) after the \(\lambda\) terminal is not the name of the function. In fact, all functions in the lambda calculus are anonymous.
An application (the third production above): this type of \(\lambda\) expressions corresponds to a function call (or application, or invocation), which contains two components: the function being called, followed by the argument that is passed into the function. So, for example, \((f\ x)\) is the application of the variable \(f\) (which must stand for a function, since functions are the only values in the lambda calculus) to the argument \(x\), which must also stand for a function.
Note that in the lambda calculus, the parentheses surround both the function and its argument, while in many modern programming languages (and in mathematical notation), the function would come first and be followed by the formal parameter in parentheses, like this: \(f(x)\). In the lambda calculus, the parentheses are not optional around function calls. Furthermore, the grammar above makes it clear that they cannot be used anywhere else.
The grammar above is quite concise, since it contains only two non-terminals. Yet it generates an infinite set of expressions that represent all computable functions! Recall that the expressive power of BNF grammars comes from recursion, which is present in both the second and third productions in the grammar above.
The following slideshow demonstrates how to use the grammar above to build the parse tree for a given lambda expression.
Questions to ponder
Q1. Why does the non-terminal \(<var>\) not appear on the left-hand size of any productions in the grammar above? Is the grammar incomplete?
Q2. How many terminals does this grammar contain?
Q3. Is this grammar ambiguous, since the third production is doubly recursive?
22.1.2. RP 14 part 1¶
Test your mastery of the syntax of the lambda calculus with this exercise. To get credit for this randomized exercise, you must solve it correctly three times in a row.
22.1.3. RP 14 part 2¶
Once you can consistently solve the previous problem, try this more intense exercise, in which you have to analyze four expressions each time. To get credit for this randomized exercise, you must solve it correctly three times in a row.
