Lambda Calculus I

Motivation and Introduction

Is there a fuctional theory where functions and their arguments are at the same level?

Example

$$f(x)=x^2$$ $$f:\mathbb{R}\to \mathbb{R}$$

It looks like functions are somewhat larger than its arguments…

• $\lambda$ calculus to CS is like algebra to mathematics
• It inspired funcional pragramming: LISP, ML, Haskell…

At the core of $\lambda$ calculus is a way to define annonymous functions.

Example

$f(x)=x^2$ is represented as $\lambda x.x\times x$. $x$ is the argument, and $x\times x$ is the function. Note that here it is just an example. There is actually no notation like $\times$ in $\lambda$ cal. In Python, we can write $\lambda$ cal as:

lambda x: x*x

Proof theory notation

$$\text{(name)}\frac{P_1\in S,\dots ,P_n\in S}{C\in S}\text{(side conditions)}$$

• Things above the line are premises (what you know or assume)
• Thing below the line is conclusion (what you are now allowed to claim)
• Every rule has a name
• When there is no side condition, it is called an axiom.

Term

$\lambda$ cal is basically studying terms. The set of terms $\Lambda$ is defined by:

$$\begin{array}{rl}& \text{(variable)}\frac{}{x\in \Lambda }(x\in \mathcal{V})\\ & \text{(abstraction)}\frac{s\in \Lambda }{(\lambda x.s)\in \Lambda }(x\in \mathcal{V})\\ & \text{(application)}\frac{s\in \Lambda ,t\in \Lambda }{(st)\in \Lambda }\end{array}$$

• A sequence of applications associates to the left. So $xyz$ means $((xy)z)$
• The body of a lambda abstraction (the part after the dot) extends as far to the right as possible. So $\lambda x.st$ means $\lambda x.(st)$ not $(\lambda x.s)t$
• Nested abstractions associate to the right and can be collected under a single $\lambda$ sign. So $\lambda xy.z$ means $\lambda x.\lambda y.z$
  • It can be seen as a function that receive multiple inputs

Free and Bound Variable

Free Variable FV(s)

$$\begin{array}{rl}& FV(x)=\{x\}\\ & FV(st)=FV(s)\cup FV(t)\\ & FV(\lambda x.s)=FV(s)\setminus \{x\}\end{array}$$

• A variable $x$ is free in a term $s$ if $x\in FV(s)$
• A variable $x$ is bound if it is in a subterm $\lambda x.u$ of $s$
• A term $s$ is closed if it has no free variable. They are also called as combinators
• A term can simutaneously be free and bound

What does "bound" means?

Basically, that a variable that is bound means it is “captured” by a $\lambda$, so it will be replaced when you provide an input. Think of it as a local variable in coding, which only has meaning inside the specific block.

Alpha Conversion

Alpha convertible

$s$ and $t$ are $\alpha$ converible if one can derive the other by simply renaming bound variables, written as $s\equiv t$.

• Bound variables’ name is meaningless, since it will be replaced when given an input.

Beta Conversion

Application in $\lambda$ cal means substitution, which is basically the $\beta$ conversion.

$$(\lambda x.s)t\stackrel{\beta }{\to }s[t/x]$$

Here $s[t/x]$ is not a term, but it represent a term that is obtained by the substitution.

$$\begin{array}{rl}x[t/x]& \equiv t,\\ y[t/x]& \equiv y,\\ (su)[t/x]& \equiv (s[t/x])(u[t/x]),\\ (\lambda y.s)[t/x]& \equiv \lambda y.(s[t/x])\text{ assuming }y\not\equiv x\text{ and }y\notin \text{FV}(t)\end{array}$$

• Substitution should only be applied to free occurences of $x$ in $s$
• Avoid unintended capture of free variables! It can be avoided by simply rename the bound variables.

Example

$s\equiv \lambda x.yx,t\equiv \lambda z.xz$. What is the result of $s[y/t]$? $\lambda x.(\lambda z.xz)x$ is not correct. Rename $x$ into $x^{\prime }$ first, and we got $\lambda x^{\prime }.(\lambda z.xz)x^{\prime }$

Equation Theory

$\lambda \beta$

$$\begin{array}{rl}\text{(reflexivity)}& \frac{}{s=s}\\ \text{(symmetry)}& \frac{s=t}{t=s}\\ \text{(transitivity)}& \frac{s=tt=u}{s=u}\\ \text{(application)}& \frac{s=s^{\prime }t=t^{\prime }}{st=s^{\prime }{t}^{\prime }}\\ \text{(abstraction)}& \frac{s=t}{\lambda x.s=\lambda x.t}\\ (\beta )& \frac{}{(\lambda x.s)t=s[t/x]}\end{array}$$

A formal proof of an equation in $\lambda \beta$ theory is a proof tree constructed by rules.

Example

\begin{prooftree} \AXC{} \LeftLabel{($\beta$)} \UIC{$(\lambda xy.x)p = \lambda y.p$} \AXC{} \LeftLabel{(refl)} \UIC{$q=q$} \LeftLabel{(app)} \BIC{$(\lambda xy.x)pq = (\lambda y.p)q$} \AXC{} \LeftLabel{($\beta$)} \UIC{$(\lambda y.p)q = p$} \LeftLabel{(trans)} \BIC{$(\lambda xy.x)pq = p$} \LeftLabel{(sym)} \UIC{$p = (\lambda xy.x)pq$} \end{prooftree}

is the proof that $\lambda \beta ⊢p=(\lambda xy.x)pq$

$\lambda \beta \eta$

The difference between $\lambda \beta \eta$ and $\lambda \beta$ theory is the additional eta rule:

$$\begin{array}{r}(\eta )\frac{}{\lambda x.sx=s}(x\notin \text{FV}(s))\end{array}$$

• It says that a function that take $x$ as input and apply $s$ to it is just $s$ itself
• Or it says that if two functions return same output when given same input, they are the same function

Fixed Point

Fixed Point

$u$ is a fixed point of $f$ if $\lambda \beta ⊢fu=u$

First Recursion Theorem

Let $f$ be a term, then there is a term $u$ that is the fixed-point of $f$. Moreover, it can be computed in $\lambda$ cal using fixed-point combinators.

Proof

There are many fixed-point combinators, an example is Curry’s ‘paradoxical’ Y combinator:

$$y\equiv \lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$$ $$\begin{array}{rl}yf& =(\lambda x.f(xx))(\lambda x.f(xx))\\ & =f((\lambda x.f(xx))(\lambda x.f(xx)))\\ & =f(yf)\end{array}$$