26Types, Types, Types: Modeling λ Calculus
λ calculus began with the simple untyped λ calculus that we discussed in the previous chapter. But one of the great open questions about λ calculus at the time of its invention was this: is it sound? In other words, does it have a valid model?
Church was convinced that λ calculus was sound, but he struggled to find a model for it. During his search, Church found that it was easy to produce some strange and worrisome expressions using the simple λ calculus. In particular, he was worried about falling into a Gödel-esque trap of self-reference (which we’ll talk about more in 27, The Halting Problem), and he wanted to prevent that kind of inconsistency. So he tried to distinguish between values representing ...
Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.
Read now
Unlock full access