Understanding Lambda Calculus: The Mathematics Behind Functional Programming

Lambda calculus is a mathematical model for understanding computation. Despite its intimidating name, it's built on just three simple rules that can express any computable function.

Lambda calculus has had a huge influence on functional programming languages like OCaml and Haskell. Understanding these basic rules helps explain why functional languages work the way they do.

You can use variables like x, y, z to represent values.

The λ (lambda) symbol lets you define something as a function. In lambda calculus, functions are the only basic data type.

The basic form is: λ parameter.return

So λx.x represents the function f(x) = x, and λx.λy.x represents a function f(x, y) = x.

Lambda calculus uses a concept from mathematics called currying. Functional programming languages like OCaml have currying built in.

Currying is a method that breaks down functions that take multiple arguments into a chain of functions that each take only one argument. This makes functions easier to reuse by calling them repeatedly.

Instead of taking two arguments at once like λ(x,y).x y, lambda calculus uses the form λx.λy.x y.

An expression wrapped with λ is a function. To use that function, you apply a value to it:

λx.λy.x y
= f(x, y) = x
= x(y)

Example 1:

(λx.x) y
=> f(x) = x
=> x(y)

Example 2:

(λx.(λy.x)) z
=> f(x) = λy.x
=> λy.z

Example 3:

(λx.(λy.x y)) (λx.x) (z)
=> z

To use lambda calculus in programming languages, you need to handle basic data types like String, int, and Bool.

This problem was solved by American mathematician Alonzo Church (1903-1995). He invented Church Encoding to apply lambda numbers to Lambda Calculus.

Church Encoding is a formalized way of modeling data and functions.

Uses two arguments: returns the left argument when true, returns the right argument when false.

true = λa.λb.a   // if true, select parameter a
false = λa.λb.b  // if false, select parameter b

pred(n) = (n=0) ? 0 : n-1

Church encoding extends to other types like Maybe, Either, and more complex data structures, providing a way to represent any data type using only functions.

Lambda calculus proves that computation can be reduced to simple function application. Every programming concept you use today can be expressed using just these three rules. It's the mathematical foundation that makes functional programming possible.

References:

• Lambda Calculus - Stanford Encyclopedia of Philosophy

• Alonzo Church - Wikipedia