$\lambda$-Calculus: symbolic computation





  • Literals: 1, 2, 3, “Hello world”
  • Variables: $x, y, z, \dots$


  • $+ : (x,y)\mapsto x+y$
  • $\mathrm{inc} : x\mapsto x+1$
  • $\dots$

  • Always returns one value.
  • Takes a fixed number of inputs: arity of the function *

Value as function

A value is a zero-arity function.

Function as value

We want to extend the idea of things to include functions.

This is a central idea in functional programming.

Value $\equiv$ Function = Everything

Syntax for expressions (value / function)


  • $x, y, z, \dots$ are expressions


  • If $x$ is a variable, and $e$ is an expression, then $\lambda x. e$ is an expression


  • If $e_1$ is a function with arity 1, $e_2$ is an expression, then $e_1 e_2$ is an expression


We assume that all functions are with arity 1.

This is not a restriction.

The weird syntax of $\lambda$ calculus

Defining things



We can write it conveniently as $\lambda xyz.e$

Computing with $\lambda$-Calculus


We rely on string-rewriting to evaluate LC expressions.

Substitution of variables in function applications


$e[x/e’]$ is the expression obtained by substituting all occurances of $x$ in the expression $e$ with the expression $e’$.


Substition as a way to evaluate function application:

$(\lambda x. e) e’ \implies e[x/e’]$.


\begin{eqnarray} && (\lambda x.x x) (\lambda y. y) \\ &\implies& (x x)[x/(\lambda y.y)] \\ &\implies& (\lambda y.y)(\lambda y.y) \\ &\implies& y[y/(\lambda y.y)] \\ &\implies& (\lambda y.y) \end{eqnarray}



We can easily get into trouble.

Substitution cannot be used freely.

Free & Bound Variables

Variables in a function abstraction expression can be free or bound.


If a variable represents the input parameter in a function expression, then it’s considered bound. Otherwise, it’s free.

Variable Capturing

Consider an expression:

$$\lambda x. (\lambda x.x)$$

There are multiple occurrences of $x$, so let’s label them so we can refer to the individual occurrences.

$$\lambda x_1. (\lambda x_2.x_3)$$

Which input variable does $x_3$ refer to?


! This is called capturing.

Elimination of Variable Capturing

There is a rewrite rule that allows us to rename the parameter variables without changing the meaning of the expression.

$$ \lambda x. x \equiv \lambda y.y \equiv \lambda \mathsf{hello}.\mathsf{hello} $$


Suppose that $x$ is a free variable of $e$, and $y$ does not appear in $e$ at all.

Then $\lambda x.e \implies \lambda y.e[x/y]$

Elimination of Variable Capturing

Back to:

$$\lambda x. (\lambda x.x)$$


! Generally, we only apply substitution to evaluate function applications if there is no variable capturing; and this can be achieved by renaming.

How to perform computation using LC?


All can be done using LC

  1. Express the algorithm in terms of natural numbers, arithmetics, loops and conditional branches.

  2. Encode the algorithm in LC.

  3. Apply syntax rewriting until no more rewriting is possible.

  4. !

A glance of LC in action

A bit of notation:

$\lambda x.\lambda y. \lambda z. e$ is written as as $\lambda xyz. e$.

Now we can encode numbers:

$0 \equiv \lambda sx. x$ (takes two inputs, but only keep the second one.)

$1 \equiv \lambda sx. sx$

$2 \equiv \lambda sx. ssx$



Consider the simplest arithmetics: increment by 1.


def succ(n):
    return n + 1


$$S \equiv \lambda n. \lambda yx.y(nyx)$$

Let’s try this out.

\begin{eqnarray} S 0 &=& (\lambda n. \lambda yx.ynyx)0 \\ &=& (\lambda yx.ynyx)[n/0] \\ &=& \lambda yx.y(0yx) \\ &=& \lambda yx.y((\lambda sz.z)yx) \\ &=& \lambda yx.y(x) \\ &=& 1 \end{eqnarray}



def add(n1, n2):
    return n1 + n2



$2 S 3 = 5$ (work it out, it’s quite incredible.)

So, we have:

$$+ \equiv \lambda mn. mSn$$


Can you guess the LC expression for multiplication?



$$ \mathbf{Y} f = f (\mathbf{Y} f) $$


$$ \mathbf{Y} f x \implies f (\mathbf{Y} f) x \implies f f \dots f x $$

! $\mathbf{Y} f$ is a fixed point.

Using Y-combinator to implement factorial

Consider a function $F$ as:

$$\lambda fx. (\mathrm{ifzero}\ x)\ 1\ (*\ x\ (f\ (\mathrm{dec}\ x)))$$

If we apply the Y-combinator to $F$, we get:

$$ (\mathbf{Y} F) n = F (\mathbf{Y} F) n $$

You can check the following:

$$ (\mathbf{Y} F) n = (\mathrm{ifzero}\ n)\ 1\ (*\ n\ ((\mathbf{Y} F)\ (\mathrm{dec}\ n))) $$

! This is really quite amazing. We have achieved Turing-completeness via recursion. The amazing part is that we don’t need variables to refer to any values. So $F$ is just for convenience and readability.



© KEN PU, 2016