SURVEY ARTICLE: Models of the Lambda Calculus: An Introduction

The \(\lambda\)-calculus is a symbolic formalism for describing and calculating with functions. To give meaning to expressions in the \(\lambda\)-calculus they must be interpreted in terms of standard mathematical objects such as sets and functions. Each such interpretation is called a model of the \(\lambda\)-calculus. Because the concept of function embodied in the \(\lambda\)-calculus is very general---for example, a \(\lambda\)-calculus function can be applied to itself---we cannot model \(\lambda\)-calculus functions as ordinary mathematical functions. Consequently such models require some new ideas that turn out to have applications in other areas of mathematics, and in computer science as well. This paper presents an introduction to models of the \(\lambda\)-calculus that is largely self-contained, although most technical details are omitted. It starts with a brief exposition of the \(\lambda\)-calculus itself, followed by some basic theory of \(\lambda\)-models in general and then descriptions of two specific models, including Dana Scott's \(D_\infty\), the first non-trivial model discovered. It concludes with suggestions for further reading.