15 - Models of λ-calculus

Summary

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 I_S 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) ψ ° φ = I_S,

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.