Lambda Calculus for Dummies

Introduction

Lambda calculus is a system for expressing computations based on function abstraction & application. It’s the basis of functional programming and provides a simple way to represent computations.

It was introduced by Alonzo Church in the 1930s as part of his research into the foundations of mathematics.

λ Terms

Lambda calculus is comprised of constructing lambda terms and doing reduction operations on those terms.

Abstraction is the process of creating a function. The syntax of these functions are: λx. M, where x is the parameter of the function, and M is the lambda expression (also known as the body of the function). For instance, a function that doubles some x would look like: λx. x * 2

Application is the process of applying an argument to a function. The syntax of this is (M N), where M and N are lambda expressions. For instance, (λx. x * 2) 2 applies the double function from before to the argument 2, resulting in 2 * 2 = 4.

Expressions

Lambda calculus consists of a few expression rules, such as alpha conversion, beta reduction, and eta conversion:

• Alpha conversion renames variables
  • λx. x is equivalent to λy. y
• Beta reduction applies arguments to functions
  • (λx. x + 1) 2 reduces to 2 + 1 = 3
• Eta conversions simplify functions
  • λx. (f x) is equivalent to f if f doesn’t use x in the lambda expression.