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 ...
Get Good Math now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
