## 2 - Lambda Calculus

2019-09-29 10:00 CST
2019-12-20 11:35 CST
CC BY-NC 4.0

## Introduction

### What is $\lambda$-calculus?

• Programming language
• Model for computation

### Why learn $\lambda$-calculus?

• Foundations of functional programming
• Offen used as a core language to study language theories

### $\lambda$-calculus as a language

PL = syntax （语法） + semantics （语义）

• Syntax: How to write a program?
• Semantics: How to describe the executions of a program?
• Others: Type system, model theory, …

## Syntax

$\lambda$-terms or $\lambda$-expressions:

(Terms) $M, N ::= x \vert \lambda x.M \vert MN$

$M ::= x \vert n \vert \lambda x.M \vert MN \vert M+N$

• Lambda abstraction ($\lambda x.M$): anonymous functions
• int f(int x){return x;} $\Rightarrow \lambda x.\ x$
• Lambda application ($MN$)
• f(3) $\Rightarrow (\lambda x.\ x)\ 3$

### Conventions

• Body of $\lambda$ extends as far to the right as possible
• $\lambda x.\ \ M\ N$ means $\lambda x.\ (M\ N)$, not $\sout{(\lambda x.\ M)\ N}$
• $\lambda x.\ \lambda f.\ f\ x = \lambda x.\ (\lambda f.\ (f\ x))$
• Function applications are left-associative
• $MNP$ means $(MN)P$, not $\sout{M(NP)}$
• $(\lambda x.\ \lambda y.\ x - y)\ 5\ 3 = ((\lambda x.\ \lambda y.\ x - y)\ 5)\ 3 = 5-3$

### Higher-order Functions

• Functions can be returned as return values
• $\lambda x.\ \lambda y.\ x - y$ is a function that takes $x$, returns a function $\lambda y.\ x - y$.
• Functions can be passed as arguments
• $(\lambda f.\ \lambda x.\ f\ x) (\lambda x.\ x + 1) \ 2$ passes a function.

Example. Given function $f$, return function $f \circ f$: $$\lambda f.\ \lambda x.\ f\ (f\ x)$$

\begin{aligned} & (\lambda f.\ \lambda x.\ f\ (f\ x)) (\lambda y.\ y+1)\ 5 \\ &= (\lambda x. \ (\lambda y.\ y+1) ((\lambda y.\ y+1)\ x))\ 5 \\ &= (\lambda y.\ y+1)\ 6 = 7.\end{aligned}

### Curried Functions

Notice difference between

• $\lambda x.\ \lambda y.\ x - y$: returns a function f(y)
• int f(int x, int y){return x-y;}: returns a value

$\lambda$ abstraction is a function of $1$ parameter.

But computationally they are the same. They can be transformed by currying: transform $\lambda (x, y)$ to $\lambda x, \lambda y$.

### Free and Bound Variables

$\lambda x. x + y$

• $x$: bound variable (can be renamed, “placeholder”)
• $y$: free variable
• $(x+y)$ is the scope （作用域） of the binding $\lambda x$

$(\lambda x. x + y)(x+1)$: $x$ has both a free and a bound occurrence, the same as

int x = 114, y = 514;
int foo(int x) {
return x + y;
}


Formal definition about free and bound variables? $\Rightarrow$ 《数理逻辑》

• $\text{fv}(x) = \{x\}$,
• $\text{fv}(\lambda x.M) = \text{fv}(M) \setminus \{x\}$,
• $\text{fv}(MN) = \text{fv}(M) \cup \text{fv}(N)$.

$\alpha$-equivalence: $\lambda x.M = \lambda y. M\left[\dfrac{y}{x}\right]$, where $y$ fresh

## Semantics

### Reduction

$\beta$-reduction: $(\lambda x.M)N \rightarrow M\left[\frac{N}{x}\right]$

Repeatedly apply $\beta$-reduction rule to any sub-term.

### Substitution

$M\left[\frac{N}{x}\right]$: replace $x$ by $N$ in $M$.

• $x[N/x] = N$
• $y[N/x] = y$
• $(MP)[N/x] = (M[N/x])(P[N/x])$
• $(\lambda x.M)[N/x] = M$ ($x$ is a bound variable)
• $(\lambda y.M)[N/x] = \lambda y. (M[N/x])$ if $y \notin \text{fv}(N)$
• $(\lambda y.M)[N/x] = \lambda z. (M[z/y][N/x])$ if $y \in \text{fv}(N)$ and $z$ fresh

### Reduction Rules

$${\over (\lambda x.M)N \rightarrow M[N/x]} (\beta)$$

Repeatedly apply $(\beta)$ to any sub-term:

$${M \rightarrow M' \over MN \rightarrow M’N}$$

$${N \rightarrow N' \over MN \rightarrow MN'}$$

$${M \rightarrow M' \over \lambda x.M \rightarrow \lambda x.M'}$$

### Normal Form

• $\beta$-redex: a term of the form $(\lambda x.M) N$
• $\beta$-normal form: aterm containing no $\beta$-redex
• Stopping point: cannot further apply $\beta$-reduction rules

Confluence (Church-Rosser Property): terms can be evaluated in any order. Final result (if there is one) is uniquely determined.

Corollary of confluence theorem: with $\alpha$-equivalence, every term has at most one normal form. Some reduction methods may not come out with a normal form.

### Reduction Strategies

• Normal-order reduction: choose the left-most, outer-most redex first.
• Applicative-order reduction: choose the left-most, inner-most redex first.

Theorem: normal-order reduction will find normal form if exists.

Examples:

• Normal-order: \begin{aligned} &(\lambda x.\ x\ x) ((\lambda y.\ y) (\lambda z.\ z)) \\ &\rightarrow ((\lambda y.\ y) (\lambda z.\ z)) ((\lambda y.\ y) (\lambda z.\ z)) \\ &\rightarrow (\lambda z.\ z) ((\lambda y.\ y) (\lambda z.\ z)) \\ &\rightarrow ((\lambda y.\ y) (\lambda z.\ z)) \\ &\rightarrow \lambda z.\ z \end{aligned}
• Applicative-order: \begin{aligned}&(\lambda x.\ x\ x) ((\lambda y.\ y) (\lambda z.\ z)) \\ &\rightarrow (\lambda x.\ x\ x) (\lambda z.\ z) \\ &\rightarrow (\lambda z.\ z) (\lambda z.\ z) \\ &\rightarrow \lambda z.\ z \end{aligned}

### Evaluation Strategies

• Only evaluate closed terms (i.e., no free variables)
• May not reduce all the way to a normal form.

Evaluation don’t reduce under lambda (terminates after first canonical form (i.e., lambda abstraction, or $\lambda x. M$)).

• Call-by-name (like normal-order): ALGOL 60
• Call-by-need (memorized call-by-name, lazy evaluation): Haskell, R, …
• Call-by-value(like applicative-order, eager evaluation): C, …

#### Normal Order Evaluation Rules

$${\over \lambda x. M \Rightarrow \lambda x. M}(\text{Term})$$

$${M \Rightarrow \lambda x. M' \ \ \ \ \ M'[N/x] \Rightarrow P \over MN \Rightarrow P}(\beta)$$

#### Eager Evaluation Rules

$${\over \lambda x. M \Rightarrow_E \lambda x. M}(\text{Term})$$

$${M \Rightarrow_E \lambda x. M' \ \ \ \ N \Rightarrow_E N' \ \ \ \ M'[N'/x] \Rightarrow_E P \over MN \Rightarrow_E P}(\beta)$$

## Programming in $\lambda$-calculus

### Encoding Boolean Values and Operators

• True: $\lambda x.\ \lambda y.\ x$
• False: $\lambda x.\ \lambda y.\ y$
• Not: $\lambda b. \texttt{ False True}$, or $\lambda b.\ \lambda x.\ \lambda y.\ b\ y\ x$
• And: $\lambda b.\ \lambda b'.\ b\ b'\ \texttt{False}$
• Or: $\lambda b.\ \lambda b'.\ b\ \texttt{True}\ b'$
• If $b$ then $M$ else $N$: $b M N$

### Church Numerals

• 0: $\lambda f.\ \lambda x.\ x$
• 1: $\lambda f.\ \lambda x.\ f\ x$
• n: $\lambda f.\ \lambda x.\ f^n\ x$
• succ: $\lambda n.\ \lambda f.\ \lambda x.\ f\ (n\ f\ x)$
• iszero: $\lambda n.\ \lambda x.\ \lambda y.\ n\ (\lambda z.\ y)\ x$
• add: $\lambda n.\ \lambda m.\ \lambda f.\ \lambda x.\ n\ f\ (m\ f\ x)$
• mult: $\lambda n.\ \lambda m.\ \lambda f.\ \lambda x.\ n\ (m\ f\ x)$

### Pairs and Tuples

• $(M, N): \lambda f.\ f\ M\ N$
• $\pi_0: \lambda p.\ p\ (\lambda x.\ \lambda y.\ x)$
• $\pi_1: \lambda p.\ p\ (\lambda x.\ \lambda y.\ y)$

$\pi_i = \lambda p.\ p\ (\lambda x_1. \ \cdots \lambda x_n.\ x_i)$

### Fixpoint in Arithmetics

$x$ is a fixpoint of $f$ if $f(x) = x$.

In $\lambda$-calculus, every term has a fixpoint.

Fixpoint combinator is a higher-order function $h$ satisfying that for all $f$, $(h\ f)$ gives a fixpoint of $f$, i.e. $h\ f = f(h\ f)$.

• Turing’s fixpoint combinator $\Theta$: $$A = \lambda x.\ \lambda y.\ y\ (x\ x\ y), \Theta = A\ A$$
• Church’s fixpoint combinator $\textbf{Y}$: $$\textbf{Y} = \lambda f.\ (\lambda x.\ f\ (x\ x)) (\lambda x.\ f\ (x\ x))$$

Let $F = \lambda f.\ \lambda n.\ \texttt{if } iszero(n) \texttt{ then } 1 \texttt{ else } n * f(n-1)$, the factorial function $fact$ is a fixpoint of $F$, i.e. $fact = \Theta F$. The right-hand side is a closed lambda term that represents the factorial function.