# Lambda Calculus 3 - Arithmetic with Church Numbers

Previously I've posted about the lambda calculus and Church numbers. We'd shown how we can encode numbers as functions using the Church encoding, but we'd not really shown how we could do anything with those numbers.

But before we get into it, let's clear up some stuff about brackets...

## Left association and you

Just as it's easier to write $\lambda nfx.$ than $\lambda n.\lambda f.\lambdax.$ because we make the assumption that each application of the function returns a new function, so there is a way of writing out function application without having to use lots of parentheses.1

Where we would normally write

$$f(x)$$

with parentheses, we could instead write

$$f\ x$$

under the assumption that each argument associates to the one on the left. So if we had

$$((f(x)\ y)\ z)$$

we can write it as

$$f\ x\ y\ z$$

and something like

$$(g(x)\ f(x))$$

is

$$g\ x\ (f\ x)$$

As we still need the parentheses to make sure that the $f$ and $x$ get bundled together. We'll need this convention as we go on as things are going to get a little more parenthesis-heavy.

OK, let's get back to the arithmetic.

Say we have the number three:

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

(the function $f$ applied to $x$ three times)

And we wanted to get to the number four:

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

(the function $f$ applied to $x$ four times)

How do we get from $three$ to $four$? Well, the difference is that we just need to apply $f$ one more time.

$$four \ \equiv \ f\ three$$

We can encode the idea of applying $f$ one more time into a lambda function. We could call it $add-one$ or $increment$ but lets go with $succ$ for 'successor'.

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

The $n$ is the number we're adding one to - we need to bind in the values of $f$ and $x$ in to the function because they'll need to have $n$ applied to them before we can apply $f$ in the one extra time.

Another way to think of this is that the general signature for a number is $\lambda f. \lambda x.$, and that when we apply $succ$ to a number, we need to get back another number - something else with the signature of $\lambda f. \lambda\ x.$

So the signature of $succ$ - and consequently any unary operation on a number - is $\lambda n.\lambda f.\lambda x$, where $n$ is the number being changed.

In Clojure that looks like:

(fn [n] (fn [f] (fn [x] (f ((n f) x))))))


Yeah, it's a bit verbose in comparison to the lambda calculus version.2 All those parentheses, while great for being explicit about which functions get applied to what, makes it a bit tough on the eyes.

\n f x -> f (n f x)


Bit more like the original, eh? Haskell has currying and left-association baked in to its syntax so its lambda expressions look almost exactly the same as the lambda calculus ones. You can see why it's so popular.3

Let's see if we can define addition.

First off, $addition$ is an operation that takes two arguments, two numbers. So we know it needs to look something like:

$$\lambda m. \lambda n. \lambda f. \lambda x.$$

Where $m$ and $n$ are the numbers being added together. Now all we need to do is work out what comes after the dot.

We could define it in terms of $succ$ - all we need to do is apply $succ$ $m$ many times to $n$:

$$\lambda m.\lambda n.\lambda f.\lambda x.\ m\ succ\ n\ f\ x$$

And this works,4 but we could probably write something both more intuitive and simpler.

What do we want as the result of $add$? We want a function that applies $f$ to $x$ $n$ many times, and the applies $f$ to the result of that $m$ many times.

$$add\ (\lambda fx.\ f\ (f\ x))\ (\lambda fx.\ f\ (f\ (f\ x))) = \lambda fx.\ f\ (f\ (f\ (f\ (f\ x))))$$

We can just write that out with the variables we've been given - first apply $f$ to $x$, $n$ many times.

$$n\ f\ x$$

and then apply $f$ to that result $m$ many times

$$m\ f\ (n\ f\ x)$$

giving us

$$add\ \equiv\ \lambda n.\lambda m.\lambda f.\lambda x.\ m\ f\ (n\ f\ x)$$

The order of $n$ and $m$ doesn't matter as they're just the order in which the number of $f$s are applied.5

## Multiplication

We've used the word 'times' a lot here when talking about the application of $f$ onto $x$s in the above. But now we'll have to deal with real multiplication.

Before you try and reach at an answer, step back a little and ask yourself what the result ought to be, and what the Church arithmetic way of describing it would be.

Say we had the numbers two and three. If I was back in primary school I'd say that the reason that multiplying them together made six was because six was 'two lots of three' or 'three lots of two'.

So when I want to put this into Church arithmetic, I feel like saying 'six is the application of three lots of the application of two lots of the application of $f$ onto $x$'. Which is a mouthful, for sure, but looks like

$$six\ \equiv\ \lambda f.\lambda x.\ ((three\ (two\ f))\ x)$$

or, without the parentheses

$$six\ \equiv\ \lambda f.\lambda x.\ three\ (two\ f)\ x$$

$two\ f$ is a function that applies $f$ two times to whatever it's next argument is. $three\ (two\ f)$ will apply $two\ f$ to its next argument three times. So it will apply it $3\ \times\ 2$ times - 6 times.

And so now we can move from the particular case to the general case; multiplication is:

$$mult\ \equiv\ \lambda m.\lambda n.\lambda f.\lambda x.\ m\ (n\ f)\ x$$

"$m$ lots of ($n$ lots of $f$) applied to $x$", which is still a mouthful but

## Exponentiation

So what could exponentiation be? Well, the first thing we know is that this time, order is going to be important - $2^3$ is not the same as $3^2$.

Next, what does exponentiation mean? I mean, really mean? When we did multiplication we saw us doing 'two lots of (three lots of $f$)'. But now we need to do 'two lots of something' three times. The 'three' part has to apply, not to the number of times we do an $f$, nor the number of times we do '$n$ lots of $f$'. But rather it needs to be the number of times we do $n$ to itself.

Woah.

So if 'three' is the application of $f$ three times to $x$, we can say that $2^3$ is the application of $two$ three times to $f\ x$.

Even. Bigger. Woah.

Another way to look at it: a Church number is already encoding some of the behaviour of exponentiation. When we use inc and 0 as f and x we can think of the number n acting as $inc^n$ - inc done to itself n many times.

This is more explicit if we try it with something other than increment - say double, aka 'times two'. Let's do it in Haskell - but please feel free to pick any language you like.

let timesTwo = \x -> 2 * x
let four = \f x -> f(f(f(f x)))

four timesTwo 1 -- 16


Four lots of timesTwo is 16; all we need to do is to use the number two instead, and apply the result to an f and an x.

let two = \f x -> f(f x)
four two succ 0 -- 16


Sixteen again.

So function for exponentiation - m to the power of n - is:

$$exp\ \equiv\ \lambda m.\lambda n.\lambda f.\lambda x.\ n\ m\ f\ x$$

But remember $\eta$-reduction? We can just go directly to:

$$exp\ \equiv\ \lambda m.\lambda n.\ n\ m$$

This is because you know the function you're left with after you've applied $n$ to $m$ is a number - will take an $f$ and an $x$ - you don't need to explicitly bind them in the outer function just in order to pass them unchanged to the inner one.

But that's just a nicety. The important thing is... we've finished!

## Summary and Next!

This post looked at some simple arithmetic using Church numerals. We saw successor

$$succ\quad \equiv\quad \lambda n.\lambda f.\lambda x.\ f\ (n\ f\ x)$$

$$add\quad \equiv\quad \lambda m.\lambda n.\lambda f.\lambda x.\ m\ f\ (n\ f\ x)$$

multiplication:

$$mult\quad \equiv\quad \lambda m.\lambda n.\lambda f.\lambda x.\ m\ (n\ f)\ x$$

and exponentiation:

$$exp\quad \equiv\quad \lambda m.\lambda n.\ m\ n$$

An interesting relationship between the last three: the $f$ moves along to the right as the operation becomes 'bigger'.

Next post we'll be taking a short break from arithmetic to take a look at logic using the lambda calculus.

1. And I'm speaking as a mad Lisp fan, lover of parens where ever they are.

2. But still terse compared to the mess we'd get in Python. Or Ruby. Yeah, don't try it in Ruby. Oh, and I guess we could use the short hand anonymous function syntax, but I think that'd look even messier...

3. For functional programming that is.

4. Get your pencil and paper out if you want to prove it!

5. The same will go for multiplication. We know that this has to be the case if we're representing these numbers and operations correctly as they should display the commutative property

# Lambda Calculus 2 - Church Numbers

## Counting without numbers?

In the first post I wrote about the lambda calculus we looked at the basic syntax and a simple function that took two numbers and added them together:

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

This might all look OK until I tell you that, in the untyped lambda calculus, the only primitive data type is a function.

A function. Not a bit, a byte, a string; not a number - a function.

So we should be a little suspicious of $\,\lambda x.\lambda y.x + y$ as this $+$ symbol needs to be defined as a function. Fair enough - addition feels like a the sort of thing that could easily be a function.

But what would we apply to it? We need a number - like one or two. But we need to make them out of functions.

Wait, what? We need to make numbers out of functions?!

And this is where things start to get weird.

## So what's a number anyway?

You will now be inducted into a sacred mystery that will allow you to make and understand Lisp jokes on the Internet. Be brave.

In a universe which only has functions - how would we count? Well, we'd have to do it with functions, obviously.

OK, sure - but that's not really getting us anywhere - let's take $2$ as a concrete example. How do I write a function that represents $2$?

Simple - we could just give it a name - like it was JavaScript:

const two = () => {}


Now you're obviously shouting "But that's cheating! What are these 'names' of which you speak? Are they made of functions too?"

And you'd be right. The thing is, we don't just want a symbol for $2$ - the numeral. What we want is a function that represents, in some way, the very essence of two-ness.

What I'm trying to get across here (without jumping to the solution immediately) is that the representation of numbers in the lambda calculus are not mere symbols; they capture a key behaviour that we associate with the idea of 'number'.

And that behaviour is repetition. When we say 'look at those two apples', we're expecting there to be an apple, and then another apple. In Church arithmetic a number is represented by a function that takes two values, and then applies the first value to the second value $n$ times, where $n$ is the number being represented.

## Church numbers

So much for the theory, let's take a look at some real numbers.1 First up, the number one:

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

We accept a variable called $f$, we take another one called $x$, and we call $f$ with $x$ once. We're kinda hoping that $f$ turns out to be a function that takes a single argument, but as this is the lambda calculus and everything is a function that takes a single argument, we can be fairly absolutely certain it is.

In JavaScript:

f => x => f(x)


And Scheme:

(lambda (f) (lambda (x) (f x)))


So if that's one, we can probably work out what two is, right?

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

And three?

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

OK, so no peeking now. What's zero?

...

...

...

...

...

Did you work it out?

$$\lambda fx. x$$

It's just ignoring the original function and returning the value it would've been applied to. The function $f$ has been applied to $x$ zero times.

## Function composition and functional powers

There's a neater way of talking about this, with just a litte more notation. We can abstract the idea of "first apply $f$, then apply $f$ to that result, then apply $f$..." out to the idea of function composition, which you might have seen in some languages. This is just building a new function out of two functions. The new function does exactly the same thing as calling one function after the other (in right-to-left order). This is usually written using the $\circ$ symbol:

$$(f \circ f)\ x = f\ (f\ x)$$

And so three could become the (slightly) easier to read:

$$\lambda f.\lambda x.\ (f \circ f \circ f)\ x$$

But we can go further. The idea of composing a function with itself so-many times can be written as a functional power - a 'function to the $n$'. Just like we can say $2^3 = 8$, so we can say:

$$\lambda f.\lambda x.\ (f\ (f\ (f\ x)))\quad=\quad \lambda fx. (f\circ f\circ f)\ x\quad=\quad \lambda fx. f^3\ x$$

Implementing composition and powers of functions is left as an exercise for the reader in their favourite language.2

## Playing around with the computer

I find there to be two productive interesting ways to play around with the lambda calculus and Church numbers when I'm trying to understand what's going on.

Firstly, and probably more obviously, try plugging around with them in your favourite language (as long as it has some sort of anonymous function type). Say Python - if we were to write three as a Church numeral we'd have:

three = lambda f: lambda x: f(f(f(x)))


If we want to test this - to see if it does what we think it does - we just need a function to be $f$:

increment = lambda x: x + 1


and some value to play the role of $x$

zero = 0


So then we just plug in those values:

three(increment)(0) #=> 3


We used three variables to hold the values above, but we could just inline them to get to something that looks a little more lambda-y:

(lambda f: lambda x: f(f(f(x))))(lambda x: x + 1)(0) #=> 3


Which translates to:

$$(\lambda f.\lambda x.\ f\ (f\ (f\ x)))\ (\lambda x. x + 1)\ 0 = 3$$

Both zero and increment use Python's built in number system. But we don't have to use numbers to test Church numbers. All we need are values that behave in the required way.3 For instance:

(define inc (lambda (x) (cons '() x)))

(define zero '())

(((lambda (f) (lambda (x) (f x))) inc) zero) ;;=> (())
(((lambda (f) (lambda (x) (f (f x)))) inc) zero) ;;=> (() ())
(((lambda (f) (lambda (x) (f (f (f x))))) inc) zero) ;;=> (() () ())


Lots of things will work - experiment!

## Playing around with pen and paper

The second way I like to play with lambdas is with pen and paper. The simplicity of the syntax, and the very few transformations allowed on an expression,4 mean that it's possible to do the evaluation yourself. Let's try it with the above. I'm going to go through it step by step, and I'm going to note which of the reductions steps being performed at each line.

$$\begin{array}{ c | l | c} & Expression & Reduction \\ \hline 0 & (\lambda fx.\ f\ (f\ (f\ x)))\ (\lambda x. x + 1)\ 0 \\ 1 & (\lambda x.\ (\lambda x.\ x + 1)\ ((\lambda x.\ x + 1)\ ((\lambda x.\ x + 1)\ x)))\ 0 & \beta \\ 2 & (\lambda x. (\lambda a.\ a + 1)\ ((\lambda b.\ b + 1)\ ((\lambda c.\ c + 1)\ x)))\ 0 & \alpha \\ 3 & (\lambda a.\ a + 1)\ ((\lambda b.\ b + 1)\ ((\lambda c.\ c + 1)\ 0)) & \beta \\ 4 & (\lambda a.\ a + 1)\ ((\lambda b.\ b + 1)\ 1) & \beta \\ 5 & (\lambda a.\ a + 1)\ 2 & \beta \\ 6 & 3 & \beta \end{array}$$

This is fun to try out, and while it's not much help when the expression is relatively simple as the one above, it gets pretty vital for me when I want to discover how more complicated expressions work.

In summary, the computer is great for checking that a lambda expression works, but I prefer to do get the pen and paper out if I want to get a feel for what's going on - for what makes it work.

## But ...

But what about the $+$ and $1$ and $0$ above? I said that there were only functions in the lambda calculus, aren't we still cheating a little bit?

We are. So in the next post let's define increment, add, multiply and maybe even exponentiation in terms of lambdas. Things are certain to get weirder.

1. I mean, actually these are the natural numbers including zero, not actually the real numbers. Yay, maths joke!

2. I've always wanted to say that. But, seriously - implement them. It's fun!

3. I am thoroughly in debt to the amazing book The Little Schemer for the this example.

4. $\alpha$-conversion and $\alpha$-reduction - see the first post

# Lambda Calculus 1 - Syntax

The word 'lambda' comes up more and more the longer you work as a programmer. There it is as a keyword in Python for an anonymous function. Same again in Scheme. Oh look, there it is in Ruby. Look at the logos for Racket, Clojure, MIT. Lambdas everywhere. The interest/obsession goes back to the mathematical roots of Lisp, specifically Alonzo Church's lambda calculus.

## Why?

Church was researching the foundations of mathematics - particularly computation. The notation he came up with is a way of expressing any computation at all - if a computer can do it, it can be written in the syntax of the lambda calculus. But, interestingly for us, it is not concerned about how he computer does it; rather it just has some simple rules about what a computer can do. It is, if you like, a very simple declarative programming language.

## Syntax

The lambda calculus gets its name from its use of the Greek letter lambda - $\lambda$ to represent a function that takes a single argument.

After the $\lambda$ comes the name that that single argument is bound to - say $x$.

And after that we write a $.$ to say that we're inside the 'body' of the function.

The $x$ is a bound variable - it stands for some value that the function can be applied to.

And to apply a value to a function, you call it by putting them next to each other (maybe with some brackets to make it clearer what's the value and what's the body).

That's it. That's everything in the lambda calculus - it's a syntax for writing about functions of one argument.

So where in JavaScript we have:

x => x + 1


and in Scheme we have

(lambda (x) (+ x 1))


in the lambda calculus syntax we have:

$$\lambda x.x + 1$$

## Only one argument?

So you might see some limitations here.Only one argument, you may say, what if I need another one? Happily we can just return another function to bind a new argument. Hooray - everything is curryed.

So where in JavaScript:

x => y => x + y


and in Scheme:

(lambda (x) (lambda (y) (+ x y)))


so in the lambda calculus we have:

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

Although usually1 we'd just write:

$$\lambda xy.x + y$$

But we would of course remember that, if the function had only one argument applied to it, it would return a function that expected the next argument.

## $\alpha$-conversion, $\beta$-reduction

These terms do absolutely nothing to dispell the feeling that the lambda calculus is a bit elitist. Look, even more Greek letters - it must be complicated and clever because just writing about it requires me to know how to say $\alpha$!

Really though, these are just big words for 'substitution' and 'application', the basics of which you probably picked up in high school algebra.

'α-conversion' (alpha-conversion) just means that we can change the name of a bound variable in a Lambda expression. So if we've got:

$$\lambda xy.x + y$$

We can just change all the $x$s to $a$s

$$\lambda ay.a + y$$

And the expression hasn't changed its meaning one iota.2

'β-reduction' (beta-reduction) is a little more complicated - what it means is that, when a value is applied to a function, we can substitute all the variables that name that argument with the value the function is applied to. For instance, in JavaScript:

(x => y => x + y)(5)


under β-reduction becomes

y => 5 + y


We unwrap the outer function and replace occurances of its variable with the supplied value. In lambda land:

$$(\lambda xy. x + y)\ 5$$

Becomes

$$\lambda y. 5 + y$$

(I threw some parentheses around that other Lambda expression to make it clear that the $5$ was getting applied to the whole function and to separate it from the body $x + y$ - there's no hard and fast rules as far as that goes).

Next up - numbers made of functions. Wait, what?

1. To save on the world's dwindling supply of $\lambda$s

2. Greek alphabet pun. BOOM!

# async/await in JavaScript in Five Minutes

When I first heard about async/await in JavaScript I was quite excited. Now I know about it I'm not. Let me explain; instead of doing some Lisp this evening I decided to find out what async/await fuss was about, and I think I can put it in a single sentence.

async/await is syntactic sugar to make Promises look more sequential

That's it. If you have the most basic understanding of Promises in JavaScript then you should be able to use async/await in about thirty seconds. There is nothing surprising here, which is a relief.

### async

Think of this as an annotation to a function - a way of saying that, within this lexically scoped block, we'll be living in async/await world.

async function asyncAwaitLand () {
// blah blah fishcakes
}


### await

In async/await world, .then() is spelt await. And it's another annotation, this time to to an expression. What larks. Here it is in Promise-speak:

function normalPromiseLand () {
Promise.resolve('some value')
.then(theResultOfAPromise => console.log(theResultOfAPromise))
}


And here's the same thing in nuspeak async/await

async function asyncAwaitLand () {
const theResultOfAPromise = await Promise.resolve('some value')
console.log(theResultOfAPromise)
}


### Playing nicely with Promises

async functions return Promises, so if you want to start chaining them all together be my guest:

const arrowAsync = async () => {
return 'the async annotation works with anonymous arrow functions too'
}

arrowAsync()
.then(string => console.log(string))


### Errors and Rejects

But how do you .catch() those long-awaited Promises when they go horribly wrong? Would it surprise you at all if I told you that you just use the normal sequential JavaScript error handling construct of try/catch?

function rejectedPromise () {
return Promise.reject(new Error('boom'))
}

async function asyncAwaitLand () {
try {
const nope = await rejectedPromise()
console.log('will never happen', nope)
} catch (error) {
console.log('I caught a rejected Promise:', error.message)
}
}


So how do you reject() in an async function? You can guess right? You just throw like it's sequential code.

async function throwingAsync () {
throw new Error('boom')
}

function promiseLand () {
throwingAsync()
.then(nope => console.log('will never happen', nope))
.catch(error => console.log('I caught an async throw:', error.message))
}


### Are you still reading this?

async/await is boring - thank goodness. A pretty piece of syntactic sugaring that extends the language not one jot. If you understand Promises then you should already have some ideas for how you're going to use it - more of a way of tidying up some ugly looking bits of code than a complete rethink of your codebase.

# Book Review: Clojure for the Brave and True

One line review: Clojure for the Brave and True by Daniel Higginbotham is a pretty good intro to Clojure, if you can get past the undergraduate humour.

Clojure for the Brave and True could be thought of as a part of a loose trilogy of books, including Land of Lisp and Realm of Racket,1 that explore modern Lisps in a light hearted way with cartoons.

The first problem with this comparison is that Brave & True is nowhere near as good as Land of Lisp - Barski's jokes are funnier, his cartoons are better, the content is both deeper and broader. Land of Lisp has a chapter called "Let's build a Web Server from Scratch" and it's not lying. Whereas Brave & True won't even show you the ropes on something like Compojure.

The best chapters in Brave and True, which are also the most useful ones, are the ones where you're being walked through a piece of code line by line. The 'Peg thing' game is a great example of a interactive command-line game written using a series of pure functions. This chapter gives you a real idea of how to get some Clojure code doing stuff in the world - a practical toolkit to let you get writing something.

The other great thing about this book is its opinionated introduction to editors. I struggled mightily setting up something to do my Lisps in, having gone through a variety of Vim and Emacs setups with every damn plugin you can imagine. Brave and True has an entire chapter dedicated to getting a decent Emacs environment (you can download the configuration), complete with Cider and Paredit. It's not going to teach you everything you want to know, but once you're done you will be immediately productive and able to get along with the more serious task of actually writing some Clojure.

But I often found the sense of humour in this book grating. It is as if I was forced to hang around with my fourteen-year-old self.2 The one who'd memorized a lot of Monty Python and The Hitchhiker's Guide to the Galaxy and thought that quoting it back at my friends was the height of sophisticated humour. The examples feel contrived to fit the humour, often to the detriment of the point that is trying to be made.

The poorest chapters are the ones where an idea is introduced but not fully explored. When introduced to protocols and records it would be nice to understand how they are used to leverage polymorphism in something more practical than the contrived Richard-Simmons-as-Werewolf examples that felt even less useful than the usual Object Oriented Guide to Animal Taxonomy we're forced to endure.

Brave and True is a good book, and is worth buying and reading (and if you want to sample the content it's all available on the book's excellent website). It's filled me with confidence to write Clojure (probably before other languages) and to read more books on Clojure. I just wish that it had spent less time crapping around with spurious examples and more time showing me how and why Clojure is the best.

Now I'm going to read my favourite introduction to Lisp again (keep scrolling) and maybe finish Land of Lisp.

1. Guess they couldn't find an appropriate name for an area starting with 'C'. Castle of Clojure? Continent? Cave

2. Bah, OK. My 20 year old self too. I can still sing all of The Philosophers' Song, I just know I shouldn't.