The λ-calculus and combinatory logic are two systems of logic which can also serve as abstract programming languages. They both aim to describe some very general properties of programs that can modify other programs, in an abstract setting not cluttered by details. In some ways they are rivals, in others they support each other.

The λ-calculus was invented around 1930 by an American logician Alonzo Church, as part of a comprehensive logical system which included higher-order operators (operators which act on other operators). In fact the language of λ-calculus, or some other essentially equivalent notation, is a key part of most higher-order languages, whether for logic or for computer programming. Indeed, the first uncomputable problems to be discovered were originally described, not in terms of idealized computers such as Turing machines, but in λ-calculus.

Combinatory logic has the same aims as λ-calculus, and can express the same computational concepts, but its grammar is much simpler. Its basic idea is due to two people: Moses Schönfinkel, who first thought of it in 1920, and Haskell Curry, who independently re-discovered it seven years later and turned it into a workable technique.

The purpose of this book is to introduce the reader to the basic methods and results in both fields.

The reader is assumed to have no previous knowledge of these fields, but to know a little about propositional and predicate logic and recursive functions, and to have some experience with mathematical induction.

Applicative structures

In first-order logic, a common question to ask about a formal theory is ‘what are its models like?’. For the theories λβ and CLw the first person to ask this was Dana Scott in the 1960s, while he was working on extending the concept of ‘computable’ from functions of numbers to functions of functions. The first non-trivial model, D∞, was constructed by Scott in 1969.

Since then many other models have been made. The present chapter will set the scene by introducing a few basic general properties of models of CLw, and the next will do the same for λβ, whose concept of model is more complicated. Then Chapter 16 will describe the model D∞ in detail and give outlines and references for some other models. Scott's D∞ is not the simplest model known, but it is a good introduction, as the concepts used in building it are also involved in discussions of other models.

But first, a comment: although λ-calculus and combinatory logic were invented as long ago as the 1920s, there was a 40-year gap before their first model was constructed; why was there this long delay?

There are two main reasons. The first is the origin of λβ and CLw. Both Church and Curry viewed these theories, not from within the semantics that most post-1950 logicians were trained in, but from the alternative viewpoint described in Discussion 3.27.

In Chapter 1 the technicalities of bound variables, substitution and α-conversion were merely outlined. This is the best approach at the beginning. Indeed, most accounts of λ omit details of these, and simply assume that clashes between bound and free variables can always be avoided without problems; see, for example, the ‘variable convention’ in [Bar84, Section 2.1.13]. The purpose of this appendix is to show how that assumption can be justified.

Before starting, it is worth mentioning two points. First, there is a notation for λ-calculus that avoids bound variables completely. It was invented by N. G. de Bruijn, see [Bru72], and in it each bound variable-occurrence is replaced by a number showing its ‘distance’ from its binding λ, in a certain sense. De Bruijn's notation has been found useful when coding λ-terms for machine manipulation; examples are in [Alt93, Hue94, KR95]. But, as remarked in [Pol93, pp. 314–315], it does not lead to a particularly simple definition of substitution, and most human workers still find the classical notation easier to read.

For such workers, the details of α-conversion would not be avoided by de Bruijn's notation, but would simply be moved from the stage of manipulating terms to that of translating between the two notations.

The second point to note is shown by the following two examples: if we simply deleted ≡α from the rules of λ-calculus, we would lose the confluence of both ⊳βη and ⊳β.

Simple types

In mathematics the definition of a particular function usually includes a statement of the kind of inputs it will accept, and the kind of outputs it will produce. For example, the squaring function accepts integers n as inputs and produces integers n2 as outputs, and the zero-test function accepts integers and produces Boolean values (‘true’ or ‘false’ according as the input is zero or not).

Corresponding to this way of defining functions, λ and CL can be modified by attaching expressions called ‘types’ to terms, like labels to denote their intended input and output sets. In fact almost all programming languages that use λ and CL use versions with types.

This chapter and the next two will describe two different approaches to attaching types to terms: (i) called Church-style or sometimes explicit or rigid, and (ii) called Curry-style or sometimes implicit. Both are used extensively in programming.

The Church-style approach originated in [Chu40], and is described in the present chapter. In it, a term's type is a built-in part of the term itself, rather like a person's fingerprint or eye-colour is a built-in part of the person's body. (In Curry's approach a term's type will be assigned after the term has been built, like a passport or identity-card may be given to a person some time after birth.)

Introduction: complete partial orders

Having looked at the abstract definition of ‘model’ in the last two chapters, let us now study one particular model in detail. It will be a variant of Dana Scott's D∞, which was the first non-trivial model invented, and has been a dominant influence on the semantics of λ-calculus and programming languages ever since.

Actually, D∞ came as quite a surprise to all workers in λ − even to Scott. In autumn 1969 he wrote a paper which argued vigorously that an interpretation of all untyped λ-terms in set theory was highly unlikely, and that those who were interested in making models of λ should limit themselves to the typed version. (For that paper, see [Sco93].) The paper included a sketch of a new interpretation of typed terms. Then, only a month later, Scott realized that, by altering this new interpretation only slightly, he could make it into a model of untyped λ; this was D∞.

D∞ is a model of both CLw and λβ, and is also extensional. The description below will owe much to accounts by Dana Scott and Gordon Plotkin, and to the well-presented account in [Bar84], but it will give more details than these and will assume the reader has a less mathematical background.

The construction of D∞ involves notions from topology. These will be defined below. They are very different from the syntactical techniques used in this book so far, but they are standard tools in the semantics of programming languages.

The definitions of the theories

The relations of reducibility and convertibility were defined in Chapters 1 and 2 via contractions of redexes. The present chapter gives alternative definitions, via formal theories with axioms and rules of inference.

These theories will be used later in describing the correspondence between λ and CL precisely, and will help to make the distinction between syntax and semantics clearer in the chapters on models to come. They will also give a more direct meaning to such phrases as ‘add the equation M = N as a new axiom to the definition of = β … ’ (Corollary 3.11.1).

In books on logic, formal theories come in two kinds (at least): Hilbert-style and Gentzen-style. The theories in this chapter will be the former.

Notation 6.1 (Hilbert-style formal theories) A (Hilbert-style) formal theory T consists of three sets: formulas, axioms and rules (of inference). Each rule has one or more premises and one conclusion, and we shall write its premises above a horizontal line and its conclusion under this line; for examples, see the rules in Definition 6.2 below.

If г is a set of formulas, a deduction of a formula B from г is a tree of formulas, with those at the tops of branches being axioms or members of г, the others being deduced from those immediately above them by a rule, and the bottom one being B.

The definition of λ-model

The discussion of models in the last chapter was almost too easy, so simple was the theory CLw. In contrast, the theory λβ has bound variables and rule (ξ), and these make its concept of model much more complex. This chapter will look at that concept from three different viewpoints. The definition of λ-model will be given in 15.3, and two other approaches will be described in Section 15B to help the reader understand the ideas lying behind this definition.

Notation 15.1 In this chapter we shall use the same notation as in 14.1, except that ‘term’ will now mean ‘λ-term’.

The identity-function on a set S will be called IS here.

The composition, φ ° ψ, of given functions φ and ψ, is defined as usual by the equation

and its domain is {a : ψ(a) is defined and in the domain of φ}.

If S and S′ are sets, and functions φ : S → S′ and ψ → and ψ : S′ → S satisfy

1. (a) ψ ° φ = IS,

then ψ is called a left inverse of φ, and S is called a retract of S′ by φ and ψ, and the pair 〈φ, ψ〉 is called a retraction; see Figure 15:1.