Proposed by Alonzo Church in ~1930.
intented to formalize mathematics.
Syntactic expressions that represent functions.
designed to represent the entire foundation of mathematics.
Rules of rewriting the syntactic expression
rewrite rules represent mathematical reasoning.
Values
- Literals: 1, 2, 3, “Hello world”
- Variables: $x, y, z, \dots$
Functions
- $+ : (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 *
A value is a zero-arity function.
We want to extend the idea of things to include functions.
This is a central idea in functional programming.
- $x, y, z, \dots$ are expressions
Abstraction:
- If $x$ is a variable, and $e$ is an expression, then $\lambda x. e$ is an expression
Application:
- 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.
$\lambda x.e$
This is a function taking one input, represented by the variable $x$. It returns one value, which is evaluated as the expression $e$. The expression $e$ usually makes uses of $x$, but not necessarily.
$e_1 e_2$
This is passing $e_2$ as an argument to the expression $e_1$. Recall that everything is a function. So $e_1$ is a function with one argument.
$e_1 e_2 e_3 = ((e_1 e_2) e_3)$
This shows that $e_1$ takes one argument ($e_2$), and returns an expression which is yet again a function which takes $e_3$ as an input.
Identity function
$\lambda x.x$
Functions with multiple arity
Suppose we have a function $f(x,y,z) = e$ where the expression involves all three input variables $x, y, z$.
We can use the following expression to build $f$:
$\lambda x.(\lambda y.(\lambda z. e))$
This is a big deal.
Functions as values in action here.
We can write it conveniently as $\lambda xyz.e$
We rely on string-rewriting to evaluate LC expressions.
Notation:
$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’]$.
Example:
\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}
Warning
We can easily get into trouble.
Substitution cannot be used freely.
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.
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.
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} $$
Renaming
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]$
Back to:
$$\lambda x. (\lambda x.x)$$
First we consider the sub expression $\lambda x.x$.
Using renaming, we can rewrite it to $\lambda y.y$.
Then we get:
$$\lambda x. (\lambda x.x) \implies \lambda x.\lambda y. y$$
! Generally, we only apply substitution to evaluate function applications if there is no variable capturing; and this can be achieved by renaming.
All can be done using LC
Express the algorithm in terms of natural numbers, arithmetics, loops and conditional branches.
Encode the algorithm in LC.
Apply syntax rewriting until no more rewriting is possible.
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$
$\vdots$
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
Observe:
$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?
LC does not require assigning aliases to functions.
Technically, there is just ONE expression for the entire algorthm.
Why it’s hard to do recursion without aliases?
def factorial(n):
if n <= 1:
return n
else:
return n * factorial(n-1)
Is it even possible?
Yes. It’s called the Y-combinator.
$$ \mathbf{Y} \equiv (\lambda y.(\lambda x.y(xx))(\lambda x.y(xx)))$$
$$ \mathbf{Y} f = f (\mathbf{Y} f) $$
So,
$$ \mathbf{Y} f x \implies f (\mathbf{Y} f) x \implies f f \dots f x $$
! $\mathbf{Y} f$ is a fixed point.
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.
LC is purely symbolic.
It carries out computation by very simple string rewrites:
It solves problem by:
No variables are needed.