lambda calculus

The $\lambda$-Calculus is a system for manipulating strings of symbol, similar to algebra or logic. It serves as a model of computation, and is the foundation for functional programming.

The strings are composed of parenthesis, variables, and operators.
Every computable function can be expressed in $\lambda$-calculus using only these three constructs:

Variables (names): $a$
Function definitions ($\lambda$-abstractions): $(\lambda x.M)$

$$\begin{array}{rl}& (\lambda a.a)\\ & \\ \text{def }& \text{identify(}a\text{):}\\ & \text{return }a\end{array}$$

Function calls (application): $(ab)$ means “apply $a$ to $b$”

$$\begin{array}{c}(ab)\\ /\backslash \\ \text{function}\text{argument}\end{array}$$

$a,b$ can be any variable or expression (abstraction or application). Random examples: $(x(\lambda y.z))$, $(a(b(c(de)a)p))$, $(\lambda a.(\lambda b.(ab)))$, $a$

$\beta$-reduction

When a function is applied to an argument, we substitute the argument for the bound variable:

$$((\lambda x.M)N)\to M[x:=N]$$

“Replace all free occurrences of $x$ in $M$ with $N$”

$\beta$- reduction

$$\begin{array}{rl}((\lambda x.(x(yx)))(ff))& \to (ff)(y(ff))\end{array}$$

$x$ is the bound variable
$x$ occurrences get replaced
$y$ stays unchanged (it’s not bound by this λ)
$ff$ is substituted for each $x$

From algebra to λ-calculus

Starting with a familiar function:

$$f(x)=x^2+x+3$$

Applying it to 5: $f(5)=5^2+5+3=33$

Transforming it to $\lambda$-calculus form:

$$\begin{array}{rl}((x\mapsto x^2+& x+3)5)\\ ((\lambda x.x^2+& x+3)5)\\ 5^2+& 5+3\\ & 33\end{array}$$

The $\beta$-reduction substitutes $5$ for every occurrence of $x$ in the function body.

Currying

Transforming a function that takes multiple arguments into a sequence of functions that each take a single argument. In $\lambda$-calculus, all functions technically take only one argument, so multi-argument functions are achieved through currying.

$$f(x,y)\text{becomes}\lambda x.(\lambda y.\text{...})$$

Currying in action

Let’s curry a function that adds $5y+x$:

$$\begin{array}{rl}& (((\lambda x.(\lambda y.5\ast y+x))5)3)\\ & \to ((\lambda y.5\ast y+5)3)\text{(substitute }x=5\text{)}\\ & \to 5\ast 3+5\text{(substitute }y=3\text{)}\\ & \to 20\end{array}$$

Partial application

Currying enables partial application - we can apply arguments one at a time:

$$(\lambda xy.5\ast y+x)5=(\lambda y.5\ast y+5)$$

This creates a new function “add 5 after multiplying by 5”

Shorthand notation

Instead of writing nested lambdas, we often use shorthand:
Full form: $\lambda x.(\lambda y.(\lambda z.\text{...}))$
Shorthand: $\lambda xyz.\text{...}$

Similarly for application:
Full form: $((fa)b)c$
Shorthand: $fabc$

Booleans are selectors.

In $\lambda$-calculus, booleans are functions that select between two options:

$$\begin{array}{rl}\text{TRUE}& =\lambda a.(\lambda b.a)\text{(selects first argument)}\\ \text{FALSE}& =\lambda a.(\lambda b.b)\text{(selects second argument)}\end{array}$$

Or in shorthand notation:

$$\begin{array}{rl}\text{TRUE}& =\lambda ab.a\\ \text{FALSE}& =\lambda ab.b\end{array}$$

The boolean itself acts as the conditional:

$$\text{IF }p\text{ THEN }x\text{ ELSE }y\equiv pxy$$

If $p=\text{TRUE}$: returns $x$, if $p=\text{FALSE}$: returns $y$

Example

When we apply TRUE or FALSE to two values $V_1$ and $V_2$:

$$\begin{array}{rl}\text{TRUE }{V}_1{V}_2& =(\lambda ab.a)V_1{V}_2\to V_1\\ \text{FALSE }{V}_1{V}_2& =(\lambda ab.b)V_1{V}_2\to V_2\end{array}$$

Not

$$\begin{array}{r}\text{NOT}=(\lambda x.(x\text{FALSE}\text{TRUE}))\end{array}$$

Here, $x$ is expected to be a “church-encoded” boolean, and acts as a selector of the opposite argument.

---

$$\begin{array}{rl}\text{NOT FALSE}& =(\lambda x.(x\text{FALSE}\text{TRUE}))\text{FALSE}\\ & =\text{FALSE FALSE TRUE}\\ & =((\lambda ab.b)\text{FALSE}\text{TRUE})\\ & =((\lambda b.b)\text{TRUE})\\ & =\text{TRUE}\end{array}$$

And

$$\begin{array}{r}\text{AND}=(\lambda xy.(xy\text{FALSE}))\end{array}$$

$x,y$ are expected to be booleans… “if $x$ then $y$ else $\text{FALSE}$”

Or

$$\begin{array}{r}\text{OR}=(\lambda xy.(x\text{TRUE}y))\end{array}$$

$x,y$ are expected to be booleans… “if $x$ then $\text{TRUE}$ else $y$”