Day λ

For today, we are going back to foundations -- some of the oldest, and most fundamental and fascinating ideas in the entire field of computer science.

To get there, we have to talk about a few people.

The first, you may have heard of, Alan Turing. Turing was a mathematician and logician by training, and like many logicians around that time -- in the 1930s -- he was fascinated by the problem of how you expressed reasoning in mechanical ways. Now, remember -- there were no computers, so this was entirely on paper, on chalkboards, or described from person to person, but it was these people that enabled the breakthroughs that allowed computers to be built.

Turing did many things -- he's famous for at least three that are worth mentioning --

1. From the very beginning, he was fascinated by the idea of thinking machines. He devised a test for whether a machine was intelligent.
2. During WWII, he helped figure out how to leverage machines (essentially, pre-computers) to crack what was previously unbreakable Nazi encryption.
3. Relevant to today, he established fundamental results related to what can be expressed by a computer program.

A fascinating example of the last, Turing proved what is now known as the Halting Problem, which was one of the first impossibility results. What it says, essentially, is that it is impossible to construct a program that, given another program as input, can determine whether it will run forever. What was so interested about that (and it parallels work by logician Kurt Godel with other impossibility results) is that even while he and others were establishing the immense generality of this new idea of computation, they already were figuring out that there were fundamental limits. There were programs that were impossible to write. Not, difficult, or, they didn't know how to write, but mathematically impossible, with proof.

Computation is, indeed, deep. From the same era -- 1937, mathematician Lothar Collatz presented this seemingly simple problem:

Does the following program run forever on ay integer, or does it terminate for all?

fun collatz(n :: Number) -> Number:
  if n <= 1:
    n
  else if num-modulo(n,2) == 0:
    collatz(n / 2)
  else:
    collatz((n * 3) + 1)
  end
end

It's a simple program. You could have written it by the first week of class. And yet, we are 88 years later and we still don't know.

Part of what Turing did was create a universal model of computation, which is now called the Turing machine, which is a idealized model of a machine (it cannot be constructed in reality) that is capable of expressing any program that can be expressed on any machine.

But, perhaps even more fascinating, that era involved many different universal models of computation, and one of Turings other results was showing that his Turing machine was equivalent to another -- the Lambda Calculus of his PhD advisor, Alonzo Church.

The lambda calculus, unlike a Turing machine, can and has been used in computation -- indeed, most languages can express it. It involves three things, all of which you have used in Pyret:

• lambda (anonymous functions)
• variables (necessary for lambda, really)
• function application (to use the lambdas)

And that's it. What Church and Turing showed was that with these three things, and nothing else, any program could be expressed.

Now, if you pause and reflect a little, this probably seems impossible. Don't we need numbers, and strings, and booleans, and conditions, and adding, and for loops, and recursion, and any number of other things that you've learned this semester?

The goal of today, and next class, is to show you that you don't. This is a fascinating and fundamental result, and demonstrates the power and flexibility of computation.

Let's begin.

Booleans

While we started class with numbers, booleans are simpler data, so we begin our exploration of the lambda calculus with booleans.

We want to be able to write programs like:

true

true and false

if true:
  true
else:
  false
end

if true or false:
  false
else: 
  true
end

In order to do that, we need a way of expressing, using just our three tools, true, false, and, or, not, and if.

If we focus on true and false, these are values. i.e., they don't evaluate. Our only value in the lambda calculus is... lambda. So it must be that:

true = lam(...): ... end
false = lam(...): ... end

Clearly, these should be different (true is not false).

If we pause on that or a second, and think about if, or specifically, that we want to be able to express:

if COND:
  THEN
else:
  ELSE
end

Where COND, THEN, and ELSE are expressions -- COND should be a boolean, THEN and ELSE don't need to be. What if is doing, fundamentally, is using COND to decide whether to evaluate to THEN or to ELSE. How can we possibly express this decision when all we have are lambdas, variables, and function application?

The answer to both of these questions ends up being the same. If a boolean is a function of two arguments that returns only one of them, depending on whether it is true or false, then if can work by applying the boolean it gets.

Let's make this concrete:

true = lam(x y): x end
false = lam(x y): y end

if COND: THEN else: ELSE end = COND(THEN, ELSE)

If we apply this to a concrete example, like one of the ones we wanted to be able to express:

if true:
  true
else:
  false
end

We can translate that to our lambda calculus representation as:

(lam(x, y): x end)(lam(x, y): x end, lam(x, y): y end)

And if we run this, then we apply the first lam, substituting the two arguments for x and y. The latter isn't used at all in the body, and so the program evaluates to:

lam(x,y): x end

Which is our representation of true -- exactly as desired.

One issue with testing this -- while we can, on paper, evaluate function application, if we use Pyret to do it, we run into an issue -- functions are not printed out in the interactions window, so we can't see what the end result is.

One way around this is to add a little bit of code to convert back to ordinary Pyret booleans from what we can now call Church Booleans.

fun tobool(cb):
  cb(true, false)
end

If we call tobool(...) on one of our lambda calculus booleans, we will get back a normal Pyret boolean. This means we can, for example, take our previous example and wrap it appropriately:

tobool((lam(x, y): x end)(lam(x, y): x end, lam(x, y): y end))

And get back true as expected. The other thing we can do to make it easier for us to work with our lambda calculus definitions is define constants. Since these can always be substituted, using them isn't changing the fact that we are only using lambda, variable, and applications, but they can make reading the code a lot easier.

So we can define:

TRUE = lam(x,y): x end
FALSE = lam(x,y): y end

This allows us to rewrite our previous example as:

tobool(TRUE(TRUE, FALSE))

So how do we do and, or, and not?

Well, each should be a function, and and or both take two booleans and return one boolean. not takes a boolean and returns a boolean.

So,

AND = lam(b1, b2): ... end

What should it do? Well, if b1 is true, then it should return whatever b2 is. If b1 is false, it should return false.

If b1 is true, we know it is a function that returns its first argument, so in that case, we'd want it to be:

AND = lam(b1, b2): b1(b2, ...) end

What should the second argument be? Well, if b1 is true, it doesn't matter. But if b1 is false, then it will ignore its first argument (so its fine if its b2), but it will return whatever its second argument is. What do we want it to return? false! So let's make it:

AND = lam(b1, b2): b1(b2, FALSE) end

or is similar -- except now if b1 is true, we want to return true, and if it is false want to return whatever b2 is:

OR = lam(b1, b2): b1(TRUE, b2) end

For not, we have a single boolean argument, and if we get true as input, want to return false, and if we get false, want to return true.

How can we do that? Well, we know that true will return its first argument, so:

NOT = lam(b): b(FALSE, ...) end

And if we get false, then we know it will return its second argument, so we can complete as:

NOT = lam(b): b(FALSE, TRUE) end

So, we can express booleans. Let's move on to numbers -- specifically, we'll stick to natural numbers (0,1,2,...).

Numbers

Again we have task of representing values, this time things like:

0
1
2
3
...
1 + 2
3 * 4
...

Let's focus on the numbers. Again, they are values, so we need to figure out a way to represent them with lambda, i.e.:

ZERO = lam(...): ... end
ONE = lam(...): ... end
TWO = lam(...): ... end
...

And it should work for any natural number! How can we do that? One idea would be to have the number correspond to the number of arguments, i.e., 1 would be a one argument function 2 would be a two argument function (and whose body did...)... but since we can't create functions of dynamic number of arguments, it would seem to be impossible to implement something like +.

A better idea is to have each be a function with two arguments: a function and a value and have the function be applied a certain number of times to the value. Not in a row (since, until we implement mutation, running a function once and then running it again will produce the same result), but nested. i.e.,

ZERO = lam(f, x): x end
ONE = lam(f, x): f(x) end
TWO = lam(f, x): f(f(x)) end
...

Now, clearly we can construct any natural number this way -- pick a number and nest the calls the right number of times.

We can even create a helper ofnum(..) that takes a Pyret natural number and produces one of these (essentially -- it's not technically the exact same code, but it behaves the same way, and is extremely convenient for our understanding), and a corresponding tonum(..) that goes the other way:

fun ofnum(n :: Number):
  lam(f, x):
    fun r(m):
      if m == 0:
        x
      else:
        f(r(m - 1))
      end
    end
    r(n)
  end
end

fun tonum(cn) -> Number:
  cn(lam(y): y + 1 end, 0)
end

Now, of course, in order for these to be useful, we need to be able to express + and * (and others!), so lets do that, starting with +.

Addition takes two numbers and returns one, so we can start with:

ADD = lam(n1, n2): ... end

Now, what should the result be? Well, we want a function lam(f,x): f(f(...f(x))) end where there are n1 + n2 copies of f. Now, we know that n1 and n2 have this form already, but if we are going to be able to do anything with them, we have to apply them, so somehow it seems like we will need a new f and x to work with. So lets expand our solution to:

ADD = lam(n1, n2): lam(f, x): ... end end

So how can we get the inner applications? Well, if we apply n1(f,x), this should give us back f(f(...f(x))) where there are n1 copies (where we interpret n1 as a number). If we want another n2 applications of f, we can pass this as the starting value (the x) to n2, and we get:

ADD = lam(n1, n2): lam(f, x): n2(f, n1(f, x)) end end

How do we do multiplication? There are multiple ways of doing it, but one is noticing that n1 * n2 is the same as adding n2, n1 times, starting at 0.

i.e.,:

MUL = lam(n1, n2): n1(lam(y): ADD(n2, y) end, ZERO) end

This would mean if we had 4 multiplied by 3, this is the same as:

ADD(THREE, ADD(THREE, ADD(THREE, ADD(THREE, ZERO))))

To confirm, we can use our conversions:

check:
  tonum(MUL(ofnum(5), ofnum(6))) is 30
end

What about subtraction? Before we try to do n - m, let's do a simpler thing -- implement n - 1.

MINUS1 = lam(n): ... end

Somehow, this has to take a function lam(f, x): f(f(...f(x))) end and return lam(f,x): f(...f(x)) end -- i.e., apply the function one fewer time.

How can we do that? Well, the easiest way to do it is actually to take a slight detour, to define our first structured data (which we can do, of course!) -- a pair of two values.

Essentially, we want to define three things:

PAIR = lam(a,b): ... end
FIRST = lam(p): ... end
SECOND = lam(p): ... end

Where the ideas is that pairs are created with PAIR, and then one of the two values that was stored in the pair can be gotten out with FIRST or SECOND respectively.

How do we do that? Well, the idea is similar to how booleans work -- PAIR will create a lambda function, and then FIRST and SECOND will apply it in the right way (in this case by passing in functions that cause the right value to be passed back). Let's see:

PAIR = lam(a,b): lam(z): z(a,b) end end
FIRST = lam(p): p(lam(a,b): a end) end
SECOND = lam(p): p(lam(a,b): b end) end

We can confirm this is working using some of our other helpers, i.e.,:

check:
  tonum(FIRST(PAIR(ofnum(10), ofnum(5)))) is 10
end

Why do we want pairs anyway? Well, the trouble with trying to subtract one is that, with church numerals, that amounts to applying a function one fewer time.

i.e., if the input is lam(f,x): f(f(f(x)) end, we want the output to be lam(f,x): f(f(x)) end.

A very clever idea (due to another logician working around the same time, Stephen Kleene) was to construct, at each step, a pair of the current step and the next step. Then getting the previous step amounts to extracting the first part of the pair.

Let's see:

MINUS1 = lam(n): lam(f,x): FIRST(n(lam(y): PAIR(SECOND(y), f(SECOND(y))) end, PAIR(x,x))) end end

check:
  tonum(MINUS1(tonum(10))) is 9
end

Now we could implement general substraction using the same strategy as we did for multiplication -- by repeatedly subtracting 1, but let's move on, to one last task we'd like to be able to do: check for equality.

As before, we'll start with a small problem -- just checking if a number is equal to 0.

EQUAL0 = lam(n): ... end

How can we do that? Well, we want to return a boolean -- true if it is 0 and false in all other cases. In this case, we can use the fact that numbers are composed of f(f(...f(x))), i.e., if it is 0, then it is just whatever x is, and if it is non-zero, it is some number of applications of f:

EQUAL0 = lam(n): n(lam(y): FALSE end, TRUE) end

check:
  tobool(EQUAL0(ZERO)) is true
  tobool(EQUAL0(ofnum(10))) is false
end