The Lambda-Calculus and the Plotkin/Scott Model

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 x\mapsto 2\cdot x, 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.




Filed under Logic

2 responses to “The Lambda-Calculus and the Plotkin/Scott Model

  1. 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 always 57 items long, no matter how much I learn. Kind of like the bowl in Greek mythology. Now if everyone else would just stop discovering new stuff…)

      (Lately, I’ve been calling this my swid list.)

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.