Lambda Calculus | Ankit Gadiya

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.