Lambda Calculus

Many modern programming languages trace their roots back to Lisp, which in turn builds on ideas from lambda calculus. In this post, I explore the core ideas of lambda calculus.

What is lambda calculus

For the longest time, I had the impression that lambda calculus has something to do with the calculus from high school mathematics. I was wrong, calculus here simply means to calculate.

lambda calculus is a system to define any computation. Think of it like an abstract programming language to express programs. It does so using simple ideas: variables, functions and their application.

Basic constructs

lambda calculus defines two basic constructs. These are sufficient to model any computation.

• Variables

  Variables are symbols that act as identifiers in the computation. Variables can be free or bound to a function's scope (parameter).

  x           # x is free
  

  But the variables don't behave like programming languages. So, you cannot assign values to them.

• Functions

  Functions take arguments and perform some computation. The arguments are bound variables in the function's scope.

  This is a simple function that takes one argument x and returns it.

  𝛌y. y       # y is bound
  

  Sidenote: A function can only take a single argument. But multiple arguments can be simulated by defining nested functions.

  𝛌y.𝛌z y
  

Function application and β-reduction

Functions are not useful on their own. To use the functions, you can apply them to arguments. Lambda calculus defines how functions are computed: β-reduction.

β-reduction is a fancy term for repeated substitution. The functions are computed by progressively substituting bound variables within the function body.

This is a contrived example to visualize β-reduction properly. Here is a nested function that takes two arguments and by repeated substitution, we get the result.

(𝛌x.𝛌y. x) A B

(𝛌y. A) B        # First reduction for outer function.

A                # Second reduction for inner function.

Conclusion

That's it, there is no construct for conditionals, data types, loops etc. But curiously, it is possible to encode high-level constructs using these basic ideas. In a future post, I'll explore church encodings to encode conditionals and integers in lambda calculus.