Session 24: Lambda calculus

Pragmatic considerations

Consider the following function to add up the numbers up to some parameter n.

addTo 0 = 0
addTo n = n + addTo (n - 1)

This works well, except there's an important limitation: Suppose we want to use it to add the numbers up to 1,000,000. This function will end up making 1,000,000 recursive calls, which is far more than the stack can handle.

We can address this through rewriting the function to take advantage of tail recursion.

addTo 0 sum = sum
addTo n sum = addTo (n - 1) (sum + n)

A reasonable Haskell system (including Hugs) will identify that this function makes its recursive call as the very last thing it does. Because of this, it can be optimized to iterate through the function again, rather than make a recursive call. That is, the compiler will translate it into assembly code corresponding to the following pseudocode:

addTo(n, sum):
begin: if n = 0: return sum
       sum := sum + n
       n := n - 1
       goto begin

This optimization couldn't be perfomed easily in the original code, because the function wants to add something to whatever the recursive call returns - there is something still to do with the recursive call. Thus, the original code would have used recursion, while this code would not.

And, indeed, if we used the modified code to add the numbers from 0 to 1,000,000, we would find that the computer does not complain about the stack overflowing. It still doesn't compute the value, however, because of another problem: It runs out of memory. This problem arises due to lazy evaluation: The program will continue tacking additions onto the sum parameter, but it wil never have any reason to perform the evaluation. The parameter accumulates the need to add many numbers together, and eventually the structure indicating this need eats up the memory allocated by the interpreter to this purpose.

Fixing this problem is a matter of forcing the evaluation of the parameter. The following accomplishes this purpose.

addTo _ -1  = 0
addTo 0 sum = sum
addTo n sum = addTo (n - 1) (sum + n)

Although the first line will never hold, it forces the thunk representing the sum parameter to be thawed after each recursive call. Once the thunk is thawed, the memory allocated to the accumulated expression is no longer needed, and the garbage collector can pick it up. This program can successfully add the numbers up to 1,000,000.

Lambda calculus

In the 1930's, Church developed the concept of representing a mathematical function without assigning it a name. Lambda notation is just a particular way of describing functions without including a name. It's called lambda notation, because the notation happens to use the Greek letter lambda in it. (I don't know why they chose a lambda; since lambda isn't in the HTML alphabet, I'll use a backslash in my notes.) Here's an example describing a squaring function.

\x. x * x

This describes a function that takes a parameter (named x) and returns x*x as its return value. It's the same thing as f above, except we don't have to think of a name for it.

I can apply such an anonymous function by writing the parameter value following the function.

(\x. x * x) 2

This would evaluate to 4, since plugging 2 in for x in the lambda notation gives 2 * 2 = 4. This process of plugging in something for a parameter is called a reduction.

Naturally, a function's parameter might be a function itself. The following function takes two single-parameter functions as parameters and returns the composition of the two functions.

\f. \g. \z. f (g z)

So say I do the following.

Define sq as \x. x * x
Define comp as \f. \g. \z. f (g (z))
Define qu as comp sq sq

The last translates to the following, to which we can apply a sequence of reductions.

qu = (comp sq) sq
   = ((\f. \g. \z. f (g z)) (\x. x * x)) (\x. x * x)
   = (\g. \z. (\x. x * x) (g z)) (\x. x * x)
   = \z. (\x. x * x) ((\x. x * x) z)
   = \z. (\x. x * x) ((\x. x * x) z)
   = \z. ((\x. x * x) z) * ((\x. x * x) z)
   = \z. (z * z) * ((\x. x * x) z)
   = \z. (z * z) * (z * z)

Each reduction here is just a textual substitution. For example, for the third equals sign, I textually substituted (\x. x * x) in for f. (Notice how this simplication process is very much like compiling an expression into a more efficient form.)

Now if we try to evaluate qu 2, we would find the following.

qu 2 = (\z. (z * z) * (z * z))
     = (2 * 2) * (2 * 2)
     = 4 * (2 * 2)
     = 4 * 4
     = 16

These sort of calculations - reductions in lambda notation -, by the way, are called lambda calculus. The term sounds daunting, but the concept is really extremely simple: You calculate (hence the term calculus) through repeated reductions.

Evaluation order

Notice that process of reducing qu eventually stopped to where we could no longer apply reductions. Such an expression, that cannot be simplified further through reductions, is said to be in normal form.

A natural question to ask is, ``Is this inevitable?'' Can we take any expression and reduce it into normal form? The answer is no. Consider the following lambda expression.

(\x. x x) (\x. x x)

If we try to simplify it, we would go through the following process.

(\x. x x) (\x. x x) = (\x. x x) (\x. x x)
                    = (\x. x x) (\x. x x)
                    = (\x. x x) (\x. x x)
                       :

This will never terminate. And it's not alone - there are many expressions that are not reducible to normal form.

There are also many expressions that can be reduced to normal form, but some orders of reductions will not get you there. Consider the following.

(\y. 2) ((\x. x x) (\x. x x))

If we approach this through eager evaluation technique, where the argument is reduced before substituting it into the function, we will end up in a loop.

(\y. 2) ((\x. x x) (\x. x x)) = (\y. 2) ((\x. x x) (\x. x x))
                              = (\y. 2) ((\x. x x) (\x. x x))
                              = (\y. 2) ((\x. x x) (\x. x x))
							     :

Here, we become stuck trying to simplify the argument. However, it can be reduced to normal form, which we'll immediately find if we simply substitute the unsimplified argument into the function.

(\y. 2) ((\x. x x) (\x. x x)) = 2

Is there any way we can guarantee that we'll be able to reduce an expression to normal form if it exists? Note how this sounds suspiciously like the Halting Problem. But in this case, there is a way to guarantee such a reduction - the Halting Problem would kick in when we ask whether we can determine whether a particular expression can be reduced to normal form in finite time, and this cannot be done.

It turns out, however, that lazy evaluation will always reduce any reducible expression to normal form eventually. This is a surprising but true fact, for which logicians have developed proofs. We won't go through the proof, but simply state it. It's a good additional reason for preferring lazy evaluation.

Because of this property, lazy evaluation is called by logicians normal evaluation order. (By contrast, a logician calls eager evaluation applicative evaluation order, in reference to evaluating an argument before applying it into a function.) Computer scientists more familiar with procedural languages call it call by name, since the ``name'' of the expression is being passed into a function, rather than its value as in call by value, also known as eager evaluation.