1. Semantics of the Lambda Calculus¶

In the previous section, we covered the entirety of the syntax of the lambda calculus. The rest of this chapter, including this section, deals with the semantics of the lambda calculus, that is, the meaning of lambda expressions, or in other words, how they are interpreted and what their value is. Clearly, the expressive power of the lambda calculus is outstanding: its tiny syntax will allow us to express a rich set of computations, in fact, all possible computations (for more on this, look up the Church-Turing thesis).

Note that all programs in the lambda calculus are expressions, that is, programs that get evaluated for their value. The lambda calculus does not contain any statements, that is, commands that get executed for their side effects, for example, modifying the contents of memory via assignment statements or sending a string to the standard output stream via print statements. Therefore, the lambda calculus is a purely functional language.

Now, we will explain the meaning of the three types of lambda expressions whose syntax is given in the lambda calculus grammar. For each type of lambda expressions, we will describe its meaning using both an English statement and a JavaScript code fragment.

1. A variable in the lambda calculus (the first production in the Lambda Calculus grammar) is a placeholder for another lambda expression. In other words, like in all programming languages, a variable can be used to refer to some value that may or may not be known yet. So variables \(x\) and \(p_1\) in the lambda calculus can be represented by the variables x and p1, respectively, in JavaScript.

   Example	\(\lambda\) Expression	English Statement of the Semantics	JavaScript Implementation
   1	\(x\)	the variable named \(x\)	x

   The main difference between lambda calculus and JavaScript is that, in the lambda calculus, each variable can only get bound to one value during the execution of the whole program, whereas, in JavaScript, the value of a variable can be changed multiple times during execution using assignment statements. In conclusion, variables in the lambda calculus are more like named constants than variables in imperative programming languages. Furthermore, in the lambda calculus, since the only values are functions, all variables are placeholders for function values.

2. A lambda abstraction in the lambda calculus (the second production in the grammar) is a function definition, that is, an expression that defines a function, not a function call. Since all functions of the lambda calculus are anonymous and only take one parameter, all we need to define a function is the name of its parameter (that is, the variable following the \(\lambda\) in the second production in the grammar) and its body (a lambda expression).

   Example	\(\lambda\) Expression	English Statement of the Semantics	JavaScript Implementation
   2	\(\lambda x.x\)	the function of \(x\) that returns \(x\) (i.e., the identity function)	function (x) { return x; }
   3	\(\lambda y.y\)	the function of \(y\) that returns \(y\) (i.e., the identity function)	function (y) { return y; }
   4	\(\lambda x.y\)	the constant function (of \(x\)) that returns \(y\)	function (x) { return y; }
   5	\(\lambda z.y\)	the same function as above	function (z) { return y; }
   6	\(\lambda y.x\)	the constant function (of \(y\)) that returns \(x\)	function (y) { return x; }
   7	\(\lambda x.\lambda y.y\)	the function of \(x\) that returns the function of \(y\) that returns \(y\) (in other words, the function of \(x\) that returns the identity function)	function (x) { return function (y) { return y; }; }

   Note that example 7 above is the curried function of two arguments, namely \(x\) and \(y\), that returns its second argument.

3. A function application in the lambda calculus (the third production in the grammar) is a function call, that is, an expression that invokes a function on a single argument. The first component in a function application is either a variable (see example 8 below) or a more complex lambda expression that will eventually evaluate to a function. In examples 9 and 10 below, the first component of the function application is a lambda abstraction, that is, a function that is being defined and called right away. In JavaScript, this type of function application is a common idiom sometimes referred to as an IIFE.

   Example	\(\lambda\) Expression	English Statement of the Semantics	JavaScript Implementation
   8	\((x\ y)\)	the invocation of function \(x\) on argument \(y\)	x(y)
   9	\((\lambda x.x\ y)\)	the identity function applied to \(y\)	(function (x) { return x; })(y)
   10	\((\lambda z.x\ y)\)	the constant function \(x\) applied to \(y\)	(function (z) { return x; })(y)
   11	\(\lambda x.(x\ y)\)	the function of \(x\) that returns the value returned when \(x\) is called on \(y\)	function (x) { return x(y); }
   12	\((\lambda x.\lambda y.y\ z)\)	the function from example 7 above applied to \(z\). Since the curried function of two parameters is being called with a single argument, the evaluation of this application will return the identity function.	(function (x) { return function (y) { return y; }; })(z)
   13	\(( (\lambda x.\lambda y.y\ u)\ v)\)	the function from example 7 above applied to \(u\) and \(v\). Since the curried function of two parameters is being called with two arguments, the evaluation of this application will return the value of the second argument, namely \(v\).	(function (x) { return function (y) { return y; }; })(u)(v)

Note that, in example 11 above, the top-level expression is a lambda abstraction whose body is a function application.

2. Mastering Lambda Calculus Semantics¶

This problem is about the semantic equivalence between lambda expressions and JavaScript expressions.