Day 4 - Lambda Calculus

Introduced by Alonzo Church in the 1930s, λ-Calculus is a formal system in mathematical logic that expresses computation based on function abstraction and application based on variable binding and substitution.

For example, a function in standard mathematical notation would be written as:

$$f(x) = M$$

In Lambda Notation, this is expressed using abstraction as:

$$\lambda x.\ M$$

This is defined as an anonymous function that takes one input $x$ and returns the result of expression $M$.

To apply a lambda function to an argument $N$, we write:

$$(\lambda x.\ M)N$$

This expression is reduced using beta-reduction (β-reduction), which substitutes the input $N$ for every instance of $x$ in $M$:

$$M[x:=N]$$

Lets use a square function as an example:

$$(\lambda x.\ x^{2})\ 2 \longrightarrow_\beta x^2[x := 2] = 2^2 = 4$$

Currying#

Now what if we want to take in two arguments? The Lambda Notation would not allow this, as it only allows a single argument. Instead, Lambda Functions are first-class, meaning they themselves could be passed in as variables. So in Lambda Calculus, functions and values are essentially equivalent, which is kinda trippy. We can use a method called currying to essentially do this.

Lets use the sum of two squares as an example. The lambda statement can be written as such:

$$(\lambda x.\ \lambda y.\ x^2 + y^2)\ 4\ 5$$

Using β-reduction, we can first take in the variable $x = 4$, yielding a new one argument function:

$$(\lambda x.\ \lambda y.\ x^{2} + y^{2})\ 4\ 5 \longrightarrow_{\beta} (\lambda y.\ 4^{2} + y^{2})\ 5$$

And then we substitute $y = 5$.

$$(\lambda y.\ 4^2 + y^2)\ 5 \longrightarrow_\beta 4^2 + 5^2 = 16 + 25 = 41$$

---

• https://www.youtube.com/watch?v=ViPNHMSUcog