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
onevalue.- 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’sfree.

- $\mathbf{FV}(e)$ are the free variables of $e$
- $\mathbf{BV}(e)$ are the bound variables
- !

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**.

- !
- Natural numbers
- Arithmetics
- Loop and conditional branching

**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:

- Function application
- Variable renaming

It solves problem by:

- Encode the problem as a single (huge) string of LC expression.
- Using the rules to rewrite the string to a
*normal*form. - The resulting LC expression is the answer.

No variables are needed.

© KEN PU, 2016