Lambda Calculus

Sources:

• Introduction to Lambda Calculus
• Lecture Notes on the Lambda Calculus

---

For Equivalences in Lambda Calculus and Reductions, see the connected pages.

Application

An application in lambda calculus is an operation $F\cdot A$, also written as $FA$ where the algorithm $F$ is applied to the input $A$.

Abstraction

An abstraction is another basic operation. $\lambda x.M[x]$ denotes a function that takes in input $x$ and execute the expression $M[x]$, which depends on the input $x$.

Free and Bound variables

In an abstraction, there are bound and free variables.

• free: are the variables that do not appear in the input. We denote that a variable $a$ is a free variable of the $\lambda$-term $M$ with $a\in FV(M)$.
• bound: are the variables that are taken in input. We formally denote it with $a\notin FV(M)$. The bound variables are dummy variables, since their name doesn’t modify the final result. $\lambda x.xy$ here $x$ is a bound variable, and $y$ is a free variable.

Combinators

$M$ is a combinator (or closed $\lambda$-term) if $FV(M)=\varnothing$. The set of all $\lambda$-terms is denoted with $\Lambda$ (capital Lambda), and the one of closed $\lambda$-terms ${\Lambda }^{\circ }$.

Functions with more arguments

In order to express a function with more than one argument, we can use iteration of application (this is often called currying).

We can define: $F=\lambda x.F_x$ where $F_x=\lambda y.f(x,y)$ and so we can see that $(Fx)y=F_{x}y=f(x,y)$. We can also see that we need association to the left on iterated applications for this to work, so that would be the standard from now on. $Fxyz$ denotes $((Fx)y)z$.

On the other hand, iterated abstractions uses association to the right: $\lambda x_1\dots x_n.f(x_1,\dots ,x_n)\text{ denotes }\lambda x_1.(\lambda x_2(\dots (\lambda x_n.f(x_1,\dots ,x_n))\dots ))$

Substitution

We denote the substitution operation as $M[x:=N]$ which means that we substitute the free occurrences of $x$ in $M$ with $N$.

Standard Combinators

There are several standard combinators in lambda calculus that have specific names and properties. The most common ones are:

1. Identity Combinator ($I$) $\lambda x.x$: it takes an argument and returns the same argument unchanged. It represents the identity function.
2. Constant Combinator ($K$) $\lambda xy.x$: it takes two arguments and returns the first argument while ignoring the second one. It represents a constant function.
3. Constant Combinator * ($K^{\ast }$) $\lambda xy.y$: is the opposite of the $K$ combinator, and returns the second argument instead of the first one.
4. Duplication Combinator (D) $\lambda x.xx$: it takes an argument and applies it to itself. It is also known as the “self-application” combinator.
5. Composition Combinator (B) $\lambda fgx.f(gx)$: it takes two functions, $f$ and $g$, and an argument $x$, then applies $g$ to $x$ and $f$ to the result of $gx$.
6. Flip Combinator (C) $\lambda fxy.fyx$: it takes a binary function $f$ and two arguments $x$ and $y$, then applies $f$ to $y$ and $x$ instead of the usual order.
7. S Combinator (S) $\lambda fgx.fx(gx)$: it’s used to apply two functions $f$ and $g$ to the same argument $x$ and then combine their results.
8. Y Combinator (Y) $\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$: it’s used to implement recursion in lambda calculus. It allows defining recursive functions without named recursion.

Church Numerals

---

tags: lambda-calculus