Purely Functional Numbers

When I guessed that Friedman would give us something harder to do to make up for the amazingly easy assignment, I was half right. (By the way, there was a message on the class message board saying that the assignment had been edited, so I guess some of the others actually did have trouble with it. Giancarlo agreed with my assessment that it was a cakewalk, though, so I'm not the only one who nailed on the first try.) He did give us an extra brain teaser, but he didn't make it mandatory.

The brain teaser is quite difficult, and I haven't finished it yet - but it's also extremely interesting. Waaaaaay back on a post I have yet to finish I wrote, in part, about modeling addition as a series of add-one operations. So rather than thinking of 3 + 4 as such, you can think of it as 1 + 1 + 1 + 4. And indeed, four could also just be 1 + 1 + 1 + 1. In fact, this is the way that Turing Machines would represent numbers - just a series of ones. Addition becomes a simple operation of writing whatever number of ones on the end of the string.

Well, around the same time that it was proved that Turing Machines were complete (that is, covered all possible computations) - it was also discovered that the Lambda Calculus was computationally equivalent to Turing Machines (i.e. also complete). My beloved Scheme was originally styled as an Interpreter for Extended Lambda Calculus - and it is indeed based on the Lambda Calculus. So performing primitive operations in LC is a pretty good way to get a look at the engine that makes Scheme what it is.

Numbers can, of course, be modeled in the Lambda Calculus just as they can in Turing Machines. The principle is similar. Since everything in the Lambda Calculus is a function, we just need to think of numbers as functions rather than a series of symbols. The equivalent LC definition of 4 would be:

(lambda (z)
 (lambda (s)
  (s (s (s (s z))))))

Where z is a variable that we'll replace with 0, and s is a variable that we'll replace with the successor function. You would call it like
this:

(((lambda (z)
 (lambda (s)
  (s (s (s (s z)))))) 0) add1)

Where add1 is obviously shorthand for a function that takes a number and adds one to it.

So we can watch this in action:

 (lambda (s)
  (s (s (s (s 0)))) add1)

So z is replaced with 0.

(add1 (add1 (add1 (add1 0))))

And then all instances of* s are bound to add1.

(add1 (add1 (add1 1)))

And so it procedes.

(add1 (add1 2))

And so on eventually returning 4.

The brain teaser was to figure out how to do addition and multiplication with this.

Now, notice that numbers are represented as functions that take two arguments - a base and a successor function. So in a sense, the idea of addition
is already built into numbers. z can really be whatever we want - it doesn't have to be 0. It could, for example, be another number. And so
numbers, when you think about it that way, in the Lambda Calculus are really just a series of applied successor operations. (This representation for a number, by the way, is called a Church number, after Alonzo Church who developed the Lambda Calculus.)

So figuring out addition was fairly easy. I just reasoned that we would need to pass as the z argument to one Church number another Church number that
has already been resolved. Of course, this whole operation needs to return a Church number itself (for consistency) - so I started with this definition:

(define addition
 (lambda (rator rand)
  (lambda (z)
   (lambda (s)
    (...)))))

So the idea is that this should be a function that takes two Church numbers - (ope)rator and (ope)rand - and returns a Church number - i.e. a function that takes a base argument (z) and a successor function argument (s), just like all Church numbers.

Now, we know that the resolved rand is going to be passed to rator as its base argument, and that this will then need to take an s argument of its own, so:

(define addition
 (lambda (rator rand)
  (lambda (z)
   (lambda (s)
    ((rator (rand ....)) s)))))

And of course the next step is just making sure that rand gets everything it needs to be resolved - which, being a Church number itself, is a z and an s argument:

(define addition
 (lambda (rator rand)
  (lambda (z)
   (lambda (s)
    ((rator ((rand z) s)) s)))))

And in fact, this works in Scheme. I defined numbers for four, three, two and one, just like above, and it gets the right answers when you pass
it first, say, four and three, and then pass the resulting function 0 and add1.

Multiplication was also easy, given that multiplication is just repeated application of addition.

The trick here, of course, is that each s argument to rand should simply "insert" all the operations that rator performs. This is a little tricky, because we need s to have already been passed to rator before it gets passed to rand - but of course s is the second argument to a Church number! But this is just a simple matter of wrapping. If I want to exchange the order of arguments in the lambda calculus, I can simply do this:

(lambda (x) ((rator x) s))

provided we're already inside another function where s is in scope. And of course, we are because we know (from having already done addition) that our operation will return a Church number - which is a function that takes two arguments - 'a z' and 'an s.' This whole thing gets passed to rand - but this time as the s argument, not the z argument. So when we pass it, the z argument to rand should have already been passed. And we end up with:

(define multiplication
  (lambda (rand rator)
    (lambda (z)
      (lambda (s)
        ((rand z) (lambda (x) ((rator x) s)))))))

And again, if you test this in Scheme, you'll find that it works.

So that's multiplication and addition in the Lambda Calculus!!!

Subtraction is quite a bit harder, though, and I haven't figured it yet. One idea that I'm chewing on but can quite get to work is the idea that we
would want to pass the identity function as the s argument to rator a number of times equal to the number of s-es in rand. The identity function being - of course - just this:

(lambda (x) x)

All it does is take an argument and return the same argument. If I could manage to do that in place of a number of the existing s-es in rator, then it would effectively be subtraction, because it would eliminate a number of s-es equal to the number of s-es in rand (rather than adding one it would just return whatever the number was at those points, and since we're representing numbers as a series of additions, NOT adding 1 when you should is the same as subtracting 1).

But there are two problems with this.

First of all, it doesn't capture negative numbers at all - and that's something we would like to do. Now, granted, I'm not sure how Turing machines capture negative numbers either - but I can at least imagine that they might count any 1s that are written to the right of the starting position as negative or someting like that. I don't really have an idea how to represent this in Lambda Calculus, though.

Another problem is that doing it this way would seem to involve decomposing both numbers into a series of applications of potentially different successor functions - and that's something I simply don't know how to do and can't figure out. The idea would be to transform three, which is currently defined this way:

(define three
 (lambda (z)
  (lambda (s)
   (s (s (s z))))))

into something like this:

(define three
 (lambda (z)
  (lambda (a)
   (lambda (b)
    (lambda (c)
     (a (b (c z))))))))

That way it would at least be possible to pass ident instead of add1 at some stages. But there would also be the problem of how to know how many times to pass id and when to stop and start passing add1. So rand will have to be transformed even more cleverly into something that takes this kind of thing and applies the right arguments to it. And I really just have no clue how to do that.

Somehow my intuition tells me this is the approach Friedman is looking for, though.

Now, some readers will probably want to know why it isn't possible to simple pass in the sub1 function for s in some cases. Well, in the first place I'm not sure we're allowed to have a sub1 (though of course it exists in Scheme). I kinda get the impression we're not (because Friedman keeps hinting that the solution is very very clever - and simply passing sub1 doesn't seem all that clever). For another thing, it's still not clear how to know when to pass sub1 and when not. Remember, we're returning functions that take one base and one s. Doing this by making use of sub1 would seem to involve a three-argument definition for subtraction, and that would break our consistency (because numbers that came about as the result of subtraction would be different in kind from those that came about because of addition). So I really don't think that's what Friedman is looking for - though I could be wrong.

In any case, it's pretty clear to me that I'm not going to solve it - but I thought it might help to type all this out and get my thoughts straight on it.

Historically, incidentally, this is how Kleene (of Kleene star fame) made his name. As a graduate student, he supposedly ran in huffing and puffing to Church's office and said "I've figured out subtraction!" Meaning that how to do subtraction wasn't obvious even to the experts for some time. I don't feel so bad not being able to get it. Though I would add that there's some truth to the "ambient knowledge" idea - and that solving this problem was MUCH harder when Kleene did it because there weren't things like Scheme to get us used to the Lambda Calculus - which had, after all, just been invented. I have a bit more training in Lambda Calculus than Kleene arguably did when he and Church were inventing this stuff. So in that sense it's a much easier problem for me than it was for him. Which means, on the one hand, that I should be optimistic that I might actually solve it before Tuesday. On the other hand, I don't have the "Kleene had trouble with it too!" thing to fall back on as much.

If I get frustrated, though, I took the liberty of checking this book out of the library. I intend to read it in any case, but I promised myself I would have an honest go at this problem before I opened it (because I suspect the answer is probably found early in the book).

I will definitely be blogging about this book soon. I'm really excited about it. Friedman says the man who wrote it discovered something very cool indeed about the Lambda Calculus. I know what it is (he reduced the system so that it only needs a single operator), but I don't want to go into any detail about it until I've understood it better.

(A pdf version of an early version of the book seems to be available here.)