Quick and dirty intro to Lambda Calculus – Post #3 « 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 »

Leave a Reply

« Quick and dirty intro to Lambda Calculus – Post #2

New life in bnIRC »