lambda calculus « Brandon Niemczyk’s Stuff

Quick and dirty intro to Lambda Calculus – Post #3

October 25, 2008 — bniemczyk

This is a continuation of my previous post.

In order for $\lambda$ -Calculus to be useful, we have to be able to encode data. In our previous post we used integers and booleans without any explanation as to how they may be encoded. This picks up and fills out those details.

Booleans

It is useful to encode boolean values as functions that take 2 parameters and then evalute the correct argument.

$T \equiv \text{True } \equiv \lambda xy . x$

$F \equiv \text{False } \equiv \lambda xy . y$

Assuming we have a boolean $P$ we can encode an if-then-else function as $PAB$ where $A$ is the result if $P \equiv T$ and $B$ is the result if $P \equiv F$ ie..

$TAB \equiv A$

$FAB \equiv B$

Church Numerals

$\text{Zero } \equiv \lambda fx . x$

$1 \equiv \lambda fx . fx$

$2 \equiv \lambda fx . ffx$

$3 \equiv \lambda fx . fffx$

…

$n \equiv \lambda fx . f^nx$

And now to show the basic operations on numerals

Increment

$\text{Inc } \equiv \lambda nfx . f (nfx)$

Example :

$\text{Inc Zero } \equiv \lambda nfx . f (nfx) [n := \text{Zero}]$

$\equiv \lambda fx . f (\text{Zero } f x)$

$\equiv \lambda fx . f ((\lambda fx . x) f x)$

$\equiv \lambda fx . f x$

$\equiv 1$

Decrement

$\text{Dec } \equiv \lambda nfx . n (\lambda gh . h (g f)) (\lambda u . x) (\lambda u . u)$

Example:

$\text{Dec } 1 \equiv \lambda nfx . n (\lambda gh . h (gf)) (\lambda u . x) (\lambda u . u) [n := \lambda fx . fx]$

$\equiv \lambda fx . (\lambda fx . fx) (\lambda gh . h (gf)) (\lambda u . x) (\lambda u . u)$

$\equiv \lambda fx . (\lambda x . (\lambda gh . h (gf)) x) (\lambda u . x) (\lambda u . u)$

$\equiv \lambda fx . (\lambda x . (\lambda gh . h (gf)) (\lambda u . x)) (\lambda u . u)$

Addition

$\text{Add } \equiv n + m \equiv \lambda mnfx . m f (n f x)$

Example:

$1 + 1 \equiv \lambda mnfx . m f (n f x)[m := 1][n := 1]$

$\equiv \lambda fx . (\lambda fx.fx) f ((\lambda fx.fx) f x)$

$\equiv \lambda fx . (\lambda fx.fx) f (fx)$

$\equiv \lambda fx . ffx$

We can show that $\text{Inc } \equiv \text{Add } 1$

$\text{Add } 1 \equiv \lambda mnfx . m f (n f x) [m := \lambda f . fx]$

$\equiv \lambda nfx . (\lambda f . fx) f (n f x)$

$\equiv \lambda nfx . f (n f x)$

$\equiv \text{Inc }$

Multiplication

$m * n \equiv \lambda mnf . n (m f)$

Example:

$2 * 3 \equiv \lambda mnf . n (m f)[m := 2][n := 3]$

$\equiv \lambda f . (\lambda fx. f^3x) ((\lambda fx . f^2x) f)$

$\equiv \lambda f . (\lambda fx . f^3x) (\lambda x. f^2x)$

$\equiv \lambda f . (\lambda x . f^6 x)$

$\equiv \lambda fx . f^6 x$

$\equiv 6$

Posted in functional programming, lambda calculus. Leave a Comment »

Quick and dirty intro to Lambda Calculus – Post #2

October 20, 2008 — bniemczyk

This is a continuatin of my previous post.

In this post and all the following posts I write, all $\lambda$ -calculus expressions are left-associative, ie..

$ABCD = ((AB)C)D$

In this post I will expound upon some of the things I glossed over in the last post.

Variable Bindings

The $\lambda$ operator binds a variable. If a variable occurs in the body of an abstraction but is not bound, then it is called free. In the case of name clashes, variable $x$ is bound to the inner most $\lambda x$ .

$\alpha$ -conversion

The easiest way to ensure that variable names don’t have scope issues is to simply rename all bound variables to a unique name:

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

$\beta$ -reduction

What I referred to as simplifying in the last post was actually a $\beta$ -reduction. $\beta$ -reduction is the act of making all the applications in an expression that do not use any bound variables. If all bound variables in expression have unique names, then a beta-reduction is very simple:

$(\lambda A . B) B$ reduces to $B[A := B]$

The $\alpha$ -conversion described above is very important because if variable names clash, then a $\beta$ -reduction is much more complicated. Take the following term:

$(\lambda ab . ab) (cb)$

Without first applying an $\alpha$ -conversion we might end up with something like this:

wrong:

$\lambda ab . ab [a := cb]$

$\equiv \lambda b . (cb) b$

Now our free variable $b$ in $(cb)$ is incorrectly bound. Instead we should get this:

correct:

$(\lambda ab . ab) (cb) \equiv (\lambda a_1 b_1 . a_1 b_1) (c_1 b_2)$

$\equiv \lambda a_1 b_1 . a_1 b_1 [ a_1 := c_1 b_2 ]$

$\equiv \lambda b_1 . (c_1 b_2) b_1$

Now our newly renamed $b_2$ is still a free variable.

That’s it for this post, in an upcoming post I will explain how to encode some basic datatypes using pure $\lambda$ -calculus.

Posted in functional programming, lambda calculus. 1 Comment »

Quick and dirty intro to Lambda Calculus – Post #1

October 17, 2008 — bniemczyk

This is the first of a multi-part post about $\lambda$ -Calculus. I’m going to start with a description of the Untyped $\lambda$ -Calculus. Future articles will include Church Numerals and Typed $\lambda$ -Calculus.

Why?

$\lambda$ -Calculus is important because it has a close tie with functional programming. In fact most functional languages compile to some form of $\lambda$ -Calculus. You could say that $\lambda$ -Calculus is to functional programming what the Turing machine is to imperative programming.

The very basics

Everything is a function in $\lambda$ -Calculus but for the purposes of this post we will extend the core calculus with integers and basic integer operations. In a future post we will go into how integers can be represented as functions (for those unwilling to wait, check out Church Numerals).

Lets start with a sample expression:

$\lambda x . x+y$

This is called an abstraction. In this expression we call the x variable bound and the y variable free. There is one other operation called application. Application takes the form of:

$\lambda x . x+y [x := 3]$

$\lambda$ -Calculus evaluates expressions by simple substitution so the above expression simplifies to $3+y$ . One thing to note about this is that in the term $\lambda x . M$ where $M$ is another term, only free occurences of $x$ get replaced.

$\lambda x . \lambda x . x+z [x := 3]$ therefore simplifies to $\lambda x . x+z$ .

All functions are functions of one variable

$\lambda$ -Calculus does not allow abstractions that take multiple arguments. Instead you write functions that return functions which take the next variable.

$\lambda x . \lambda y . x + y$

simplifying this with $x = 3, y = 4$ we get:

$\lambda x . \lambda y . x + y [x := 3][y := 4]$

$\lambda y . 3 + y [y := 4]$

$3 + 4$

$7$

For conciseness, $\lambda x . \lambda y . M$ can be written as $\lambda xy . M$ but it is important to remember that this is a function that takes the value for x and returns a new function.

The Y combinator

It may have occured to you that recursion cannot be implemented with a simple substitution model and there are no looping constructs. How can this be Turing Complete? Recursion can be simulated by using a function $Y$ such that $Yf \equiv f (Yf)$ (ie. a fixed-point function), assume for the moment that such a function $Y$ exists.

If you wanted to represent the factorial function with recursion you could do it as:

$\text{Factorial }x \equiv \text{ if } x == 0 \text{ then } 1 \text{ else } x * \text{ Factorial }(x-1)$

Since terms are not named, and recursion is impossible, we have to write a function that takes (Yf) as a parameter.

$\lambda f . \lambda x . \text{ if } x == 0 \text{ then } 1 \text{ else } x * f (x - 1)$

we’ll call this expression $\text{ Fact }$ for brevity.

Since: $Yf \equiv f (Yf)$

$Y \text{Fact} \equiv \lambda x . \text{ if } x == 0 \text{ then } 1 \text{ else } x * f (x - 1)$ and f is bound to $Y \text{Fact}$ giving us recursion!