Lecture 19

In the past many models for computation have been presented. Church's lambda calculus one of these models. But don't be surprised, we have been using the lambda calculus extensively, when we where programming in ML. Through out everything from ML but function definition and application, and you obtain the simply typed lambda calculus.

What makes the lambda calculus run is the beta reduction rule which simply applies a function that can be applied. The lambda calculus is a minimal base for computation. Other concepts such as Booleans, and natural numbers, even recursion can be easily embedded into the untyped lambda calculus.