O'Reilly logo

Good Math by Mark C. Chu-Carroll

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required