I won’t *define* the (untyped) λ-calculus; you have the rest of the internet for that. But the basic formalism is remarkably simple. Instead of writing , for example, we write λ*x*.(2·*x*). The λ-term ( λ*x*.(2·*x*))7 stands for the application of the doubling function to 7, and we say that ( λ*x*.(2·*x)*)7 reduces to 2·7=14. (This is called β-*reduction* or β-*conversion*.)

The λ-calculus gleefully flouts the notion that a function can’t be its own argument. For example, the identity function *I* is defined by λ*x.x*, and *II* reduces to *I.* Try it: *II* written out is (λ*x.x*)(λ*x.x*). To β-reduce this, you take the right hand copy of (λ*x.x*) and use it to replace the *x* in the left hand copy. (Maybe it’s easier if we rewrite *II* as (λ*x.x*)*I*. This β-reduces to *I*.)

For my money, this is one of the most charming features of the λ-calculus. Of course, it *does* make it hard to *model* the λ-calculus via those earth-bound functions of conventional set theory. For the first few decades of its history, the untyped λ-calculus remained a computational formalism.

A λ-term is *reduced* if it can’t be reduced any further. So λ*x.x* is reduced but (λ*x.x*)(λ*x.x*) isn’t. Not all λ-terms *can* be (fully) reduced. The self-application term provides the standard example: *D* = λ*x.xx.* Now, *D* itself is reduced, but if we try to reduce *DD*, we end up in an infinite loop.

There is one natural model of the λ-calculus. Regard λ-terms as programs and not as functions. (Well of course!) Let Λ be the totality of all reduced λ-terms. With any reduced λ-term *T*, we associate the partial function from Λ to Λ that takes a reduced term *W* to the reduction of *TW*—that is, if it *has* a reduction. So you get a partial function.

It doesn’t seem like you could model the λ-calculus with *total* functions, but in the 1970s Dana Scott and Gordon Plotkin discovered (independently) that you *can*. I gave a seminar on a preprint by Scott. I recently latexed up my old hand-written notes; here’s the result.

I should say a word or two about the *typed* λ-calculus—everything above refers to the *untyped* calculus. Self-application is fun in some contexts, and sometimes very useful, but other times it’s a nightmare. To a computer scientist, having just one type for everything is the 9th circle of hell. After Scott came up with his model, he scaffolded up a whole theory of types based on these ideas. All very significant in theoretical computer science, but just a little too humdrum for my taste.

The typed λ-calculus doesn’t seem humdrum to me: this is the version that clearly reveals the connection to cartesian closed categories! This is the beginning of lots of fun.

“Types” are objects. The “untyped” λ-calculus should be called the “one-typed” λ-calculus, because it has just one type. While it’s bizarrely fun (and insanely dangerous) to have all data be of the same type when you’re doing computation, it’s sadly limiting and a bit mystifying from the category-theoretic point of view to focus on categories with just one object.

I recommend Lambek and Scott’s book for more on all this, or my lecture notes.

Huh. I ran out of categorical steam after I finished my Leinster solutions. That was just about when I was getting to Cartesian closed categories and topoi. I guess I’ll just have to add it to the list of 57 things I want to learn.

(The list is ever-renewing—it’s

always57 items long, no matter how much I learn. Kind of like the bowl in Greek mythology. Now ifeveryone elsewould just stop discovering new stuff…)