Lambda Calculus: The Foundation of Functional Programming

Functional programming is based on a theoretical foundation called lambda calculus (also written as $\lambda$-calculus) , invented by Alonzo Church. The easiest way to understand lambda calculus is to think of it as an idealized bare-bones functional programming language. In other words, take OCaml or any similar functional programming language and strip down all features that do not contribute to the ability to do functional programming. What remains is essentially lambda calculus.

Lambda expressions

The expressions of lambda calculus, called lambda expressions, can be built from either one of the following three rules:

• A variable — x, y, myvar, and so on—is a lambda expression.
• Given x is a variable and e is a lambda expression. A function abstraction is a lambda expression.
• If e1 and e2 are lambda expressions, a function application, e1 e2, is also a lambda expression.

We can use the Backus–Naur form (BNF) notation to express the formal syntax of lambda calculus more succinctly.

<var> ::= x | y | myVar | ...
<lambda_expr> ::= 
  <var>
| λ <var> . <lambda_expr>
| <lambda_expr> <lambda_expr>

Moreover, we can use parentheses in lambda expressions to avoid ambiguity.

As we can see, lambda calculus centers around two concepts—function abstraction and function application—drawn directly from mathematical functions. Function abstraction formulates the way we declare a mathematical function of one argument, for example $f(x) = x$. Likewise, in lambda calculus, $\lambda x.\, x$ represents a function that takes an input x and returns itself. This is the identity function. Function application resembles how we apply a function to an argument. For instance, we can apply $f(x) = x$ to $2$ and obtain $f(2) = 2$. Similarly, $(\lambda x.\, x)\,y$ ...