Lambda calculus (
λ-calculus) is one of the most well-known formal models of computer science. It is the basis for functional programming like
Turing machines are the foundation of imperative programming. These two systems are equivalent and both can be used to formulate
and investigate fundamental questions about solvability and computability.
First, we introduce the reader to the basics of λ-calculus: its syntax and transformation rules. We discuss the most important properties of the system related to normal forms
of λ-expressions. We present the recursive version of λ-calculus and finally give the classical results that establish the link between λ-calculus, partial recursive functions and Turing machines.