24Calculus: No, Not That Calculus—λ Calculus

In computer science, especially in the field of programming languages, when we’re trying to understand or prove facts about computation, we use a tool called λ (“lambda”) calculus.

λ calculus was designed by an American mathematician named Alonzo Church (1903--1995) as part of one of the first proofs of the Halting problem (which we’ll talk more about in 27, The Halting Problem). Turing is largely credited as the person who solved that, and his proof is the one that most people remember. But Church did it independently of Turing, and his proof was actually published first!

λ calculus is probably the most widely used theoretical tool in computer science. For example, among programming-language ...

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.