14 - Models of CL

Summary

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.