Lambda Tutorial (2016)

Lambda tutorial

These web pages provide a practical introduction to lambda reduction, with a few pointers to more esoteric issues. I'm a linguist, and I have linguists in mind for my audience, so linguistic issues will be emphasized (e.g., a discussion of the interaction of lambda with other binding operators such as $\exists$ "exists" and $\forall$ "forall").

Browser issues : If your browser can handle JavaScript 1.2, and if you have JavaScript turned on, you will be able to evaluate examples by clicking on a button, and to make up your own examples to try; otherwise, the examples will just sit there. For instance, try clicking on the "Reduce" button:You should see the string "(it works)" appear in the second window. This is a live program written in JavaScript---you can type any expression into the input box and try reducing it (you need to spell out "lambda" in the input, the program will convert it to " $\lambda$ " in the output). Character problems : As of May 2003, Internet Explorer doesn't seem to be able to print the forall or the exists symbols in the first paragraph above (you may see an empty box). But Opera and Mozilla (both with free versions) seem to do ok. Finally, Mozilla can't deal with the lambda symbol (" $\lambda$ ") in JavaScript output, so for now all the lambdas are spelled out when they are in examples.

Goal : Church's $\lambda$ -calculus provides a convenient way of representing meanings, whether meanings of programs or of expressions in English or some other natural language. As a result, it is ubiquitous in computer science, logic, and formal approaches to the semantics of natural language. The $\lambda$ -calculus consists of two things: a formal language and an associated notion of REDUCTION (roughly equivalent to "computation"). In the context of the lambda calculus, reduction is specifically called $\lambda$ -reduction. What these pages will attempt to do is teach you how to perform $\lambda$ -reduction accurately and confidently.

Other sources : I recommend Hankin's Lambda Calculi : A Guide for Computer Scientists (Oxford) for a readable survey, and Barendregt's The Lambda Calculus (Elsevier) for a more complete reference work. Barendregt and Barendsen's shorter introduction to the lambda calculus is also excellent , and accessible electronically for free (if the citeseer link ceases to work, I've cached a copyhere; note for some mysterious reason pages 2, 3 and 4 are blank). Selinger has an excellent set of lecture notes covering many logical and computational aspects of the lambda calculus here . For a more linguistic perspective, chapter 2 of Carpenter's Type-Logical Semantics (MIT Press) presents a $\lambda$ -calculus within a framework for describing natural language. The following is too fun not to mention: David Keenan, To dissect a mockingbird: a graphical notation for the lambda calculus with animated reduction .

Acknowledgements : Saber Ben Salem made a number of helpful suggestions.

Contents of this document:

Binding: free versus bound

$\beta$ -reduction (the heavy lifting)

$\alpha$ -reduction (alphabetic variants)

Examples and practice

Order of combination versus order of reduction; convergence

Various alternative notational conventions

The semantics of the $\lambda$ -operator

Scheme reference code

Combinatory Logic

Binding: free versus bound

$\lambda$ is a binding operator, just like backwards E ("∃") or upside down A ("∀"). Consequently, it always binds something (a variable), taking scope over some expression that (usually) contains occurrences of the bound variable. More practically, $\lambda$ always occurs in the following configuration:

( $\lambda$ var body) Here, "var" is the variable bound by the lambda operator, and "body" is the constituent that the lambda operator has scope over.

For instance:

( $\lambda$ x (* (+ 3 x) (- x 4))) Here "x" is the variable (the one immediately after the binding operator), and the body is "(* (+ 3 x) (- x 4))". The body contains two occurrences of "x", and both are bound by the $\lambda$ operator; any variable token that is not bound is free . ( $\lambda$ x (* (+ y x) (- x z))) In this form, the tokens of "y" and of "z" are both free.

Freedom is always relative to a particular expression. If the preceding expression is embedded within a larger one, the free variables can come to be bound:

(∃ y ( $\lambda$ x (* (+ y x) (- x z)))) In this case, the "y" has been bound, and only the "z" remains free.