Lamba Calculus

The Lambda Calculus is a computation system invented by Alonzo Church. One can think of the Lambda Calculus as a functional programming language in miniature or as a computation engine for functional programming languages. The importance of lambda calculus is that every pure functional programming language can be expressed in terms of the lambda calculus; in other words, if you were developing a functional programming langauge and you wanted to bootstrap your language, you might develop a microengine capable of interpreting the lambda calculus, and then you might implement your new functional programming language by transforming more complex expressions in your language into simpler expressions in the lambda calculus. There are a number of variations of the lambda calculus, but in the canonical version of the lambda calculus, lambda functions only take one parameter (so currying is required to achieve passing of multiple parameters), and loop constructs are not built-in. We now describe the canonical version of lambda calculus below:

BNF Grammar

<program>    ::= <expression>	     
 
<expression> ::= <application-expression>
		   |   <binarybuiltin-expression>
		   |   <lambda-expression>
		   |   number

<application-expression>    
		  ::= ( <expression>1 <expression>2 )

<binarybuiltin-expression>  
		  ::= ( <binary-operator> <expression>1 <expression>2 )

<lambda-expression>         
                  ::= ( lambda identifier . <expression> )

<binary-oparator>           
                   ::= + | - | * | / | equal? | notequal? 
                   |   less? | greater? | lessequal? | greaterequal?

Expressions

Lambda calculus has three types of expression: application expressions, binary builtin expressions, lambda expressions, and simple numeric expressions. An application expression invokes a function-expression which was created using a lambda expression, passing in the second expression as its argument. A binary builtin expression performs basic arithmetic or comparison operations on two subexpressions. A lambda expression creates a single-parameter function, which -- when invoked -- evaluates to the given expression, except with all free instances of the parameter name bound to the function's argument. To make this a little bit more clear, here are some examples:

Examples

	(lambda x . 1) // evaluates to a function which, 
		       // regardless of the argument, evaluates to 1

        (lambda x . x) // evaluates to the identity function 
                       //(i.e. a function which returns its argument)

	( (lambda x . x) 5 ) // invocation of identity function 
                             // on the argument 5, yielding 5

        (lambda f . (lambda x . (f x))) // a function which invokes
                                        // the function f on the argument x

        ( ((lambda f . (lambda x . (f x))) (lambda x . (+ x 1)) 5) 
                                       // invokes f(5) where f(x)=x+1,
				       //  yielding 6

Lambda Calculus Trickery

I claimed earlier that we can define an entire functional programming language using the lambda calculus. While I will not demonstrate the entire process, I will show one example of how lambda calculus can be used to create higher-level constructs. Let us consider an if-expression. An if-expression if of the form (if cond yes no), and evaluates to "yes" if "cond" evaluates to true and evaluates to "no" if "cond" evaluates to false (yes and no may be arbitrary expressions).

We can implement the if-expression by defining T (true) and F (false) in the following way:

	T = (lambda yes . (lambda no . yes))
	F = (lambda yes . (lambda no . no))

In other words, we define T as a function which takes in a yes and no expression and evaluates to yes, and we define F as a function which takes in a yes and a no expression and evaluates to no. With these definitions of the primitives T and F, we can then define an if-expression as:

	(if C Y N) = ((C Y) N)

In other words, we treat the condition as a function (which is sensible to do, since we have define T and F as functions), and then we simply pass in the yes and no expressions. If C was T, then we can see that the result will be the yes-expression, and if C was F, we can see that the result will be the no-expression.

Practicing With Lambda Calculus

You can practice lambda calculus and functional programming with the Scheme programming language. The CEC linux labs have an implementation of Scheme already installed (simply type "mzscheme" on the commandline). Alternatively, you can download and install Dr. Scheme, which is cross-platform. The old version of the CSE 425S website has many resources for understanding Scheme and lambda calculus. Additional resources are given below:

Related Links