Previous: Part 4: Reductions, Up: Contents

Part 5: Church Numerals

Goals

Representing data in the Lambda Calculus

As we have seen before, the lambda calculus can be used to define anonymous functions. Since the only operations that can be performed in the lambda calculus are definition of functions (lambda abstractions) and application of functions (lambda applications), you might wonder how the lambda calculus could be used to represent data values. Doing so is simple but requires a somewhat different mode of thinking.

Boolean values

One of the simplest types of data to represent are boolean values, true and false. However, since all we can effectively do with the lambda calculus is define functions, which are active constructs rather than the passive constructs we usually use to hold data, it is helpful to think about what we want to do with the boolean values rather than what we want them to represent. One of the most basic uses for boolean values is in computing conditionals such as if statements.

First let's construct a simple if function that only acts as a wrapper to facilitate argument passing and makes the expressions look a little more human-readable:

	if := \c.\i.\e.c i e

Think of the argument c as standing for "condition", i standing for "if", and e standing for "else". If the condition c is true, we want to return the expression i, otherwise we want to return the expression e. Because we can't really store data, only define functions, we need a novel approach. Why not let the condition do all the work instead of the actual if function itself? What the if statement returns is totally dependent on the condition passed to it – we just want to return either the second argument to the if function or the third argument, depending on the condition.

We previously saw the selectFirst function that returns the first argument passed to it:

	selectFirst := \x.\y.x
	selectFirst u v ->β* u

Similarly, we can define the selectSecond function:

	selectSecond := \x.\y.y
	selectSecond u v ->β* v

Now if we think of selectFirst as being true, and selectSecond as being false, we can pass the corresponding function to if and have it return the proper value:

	true := selectFirst := \x.\y.x
	false := selectSecond := \x.\y.y
	if true u v ->β* u
	if false u v ->β* v

The condition is not what we normally think of as the condition in an if statement, but rather the operation we want to perform. You can see that although we haven't defined the actual values "true" and "false", their intrinsic functionality are modeled by the functions selectFirst and selectSecond.

Exercise

Using the functions defined above, apply successive beta-reductions to show that:

	if true 1 2 ->β* 1
	if false 1 2 ->β* 2

Answers

The intermediate beta-reductions for the first expression are:

	if true 1 2 = (\c.\i.\e.c i e) true 1 2 ->β (\i.\e.cie)[true\c] = (\i.\e.true i e) 1 2
	(\i.\e.true i e) 1 2 ->β (\e.true i e)[1\i] = (\e.true 1 e) 2
	(\e.true 1 e) 2 ->β (true 1 e)[2\e] = true 1 2
	true 1 2 = (\x.\y.x) 1 2 ->β (\y.x)[1\x] = (\y.1) 2
	(\y.1) 2 ->β (1)[2\y] = 1

The intermediate beta-reductions for the second expression are:

	if false 1 2 = (\c.\i.\e.c i e) false 1 2 ->β (\i.\e.cie)[false\c] = (\i.\e.false i e) 1 2
	(\i.\e.false i e) 1 2 ->β (\e.false i e)[1\i] = (\e.false 1 e) 2
	(\e.false 1 e) 2 ->β (false 1 e)[2\e] = false 1 2
	false 1 2 = (\x.\y.y) 1 2 ->β (\y.y)[1\x] = (\y.y) 2
	(\y.y) 2 ->β (y)[2\y] = 2

Representing integers as lambda abstractions

Now that you have seen how simple boolean values can be modeled, we can show how integers can be represented. Just like before, because we can't necessarily store data, only define functions, it is helpful to think about what actionable quality integers represent: they represent a count, a number of things. Rather than trying to store a data representation of a count, we can define a set of functions that actually call another function a specified number of times. For example, we could represent zero as follows:

	zero := \f.\x.x

In this case, an application of the abstraction will take two arguments, f and x. The idea is to apply f the correct number of times to x. However, since this abstraction represents zero, it applies f zero times. Take a look at the functions to represent one and two:

	one := \f.\x.f x
	two := \f.\x.f (f x)

As you can see, the function for one will apply f to x just once. The function for two applies f to x once, and then applies f to the result, for a total of two times. Usually, x will be 0, so that the function can be applied a certain number of times starting at zero. We can continue to define these functions indefinitely:

	three := \f.\x.f (f (f x))
	four := \f.\x.f (f (f (f x)))
	...

Exercises

Assuming we have a function u, perform the intermediate beta-reductions to show the following:

	zero u zero ->β* zero
	three u zero ->β* u (u (u (\f.\x.x))))

Answers

The intermediate beta-reductions for the first expression are:

	zero u zero = (\f.\x.x) u zero ->β (\x.x)[u\f] = (\x.x) zero
	(\x.x) zero ->β (x)[zero\x] = zero
	zero = \f.\x.x

The intermediate beta-reductions for the second expression are:

	three u zero = (\f.\x.f (f (f x))) u zero ->β (\x.f (f (f x)))[u\f] = (\x.u (u (u x))) zero
	(\x.u (u (u x))) zero ->β (u (u (u x)))[zero\x] = u (u (u zero)))
	u (u (u zero))) = u (u (u (\f.\x.x))))

The successor function

Now that we have defined individual functions that can be used to represent integers, we can find a successor function that allows us to pass an abstraction for an integer that we've defined above, and get the function for the next successive integer as a result. What we basically want to do is add another f application on before all the rest of the f applications that take place inside the definition of the integer function. So, we can define a function successor that takes three arguments:

	successor := \n.\f.\x.f (n f x)

You can think of n as representing the number we want to find the successor of, and then f and x are the same arguments that usually get passed to our integer functions above. As you can see, it simply calls the integer function that is passed to it, and then applies f one more time to the result.

Exercises

Perform the intermediate beta-reductions to show the following:

	successor zero ->β* one
	successor two ->β* three

Answers

The intermediate beta-reductions for the first expression are:

	successor zero = (\n.\f.\x.f (n f x)) zero ->β (\f.\x.f (n f x))[zero\n] = \f.\x.f (zero f x)
	\f.\x.f (zero f x) = \f.\x.f ((\f.\x.x) f x) ->β (\x.x)[f\f] = \f.\x.f ((\x.x) x)
	\f.\x.f ((\x.x) x) ->β (x)[x\x] = \f.\x.f x
	\f.\x.f x = one

The intermediate beta-reductions for the second expression are:

	successor two = (\n.\f.\x.f (n f x)) two ->β (\f.\x.f (n f x))[two\n] = \f.\x.f (two f x)
	\f.\x.f (two f x) = \f.\x.f ((\f.\x.f (f x)) f x) ->β (\x.f (f x))[f\f] = \f.\x.f ((\x.f (f x)) x)
	\f.\x.f ((\x.f (f x)) x) ->β (f (f x))[x\x] = \f.\x.f (f (f x))
	\f.\x.f (f (f x)) = three

References

http://www.cs.brown.edu/courses/cs173/2001/Lectures/2001-10-25.pdf
http://www.cs.rpi.edu/~schupp/entries/COURSES/pl/notes/theory1.html
http://www.itlabs.umn.edu/HyperNews/get/gopalan/courses/CSCI8980-fall-2001/classwork/1.html
http://www.mactech.com/articles/mactech/Vol.07/07.06/ChurchNumerals

Previous: Part 4: Reductions, Up: Contents