Lambda Subtraction Update

I flipped though Okasaki's book this morning in frustration with not being able to solve subtraction in the Lambda Calculus, and it turns out it's not going to be helpful. By which of course I mean "helpful for the problem at hand." It really is only about traditional data structures - there's no sort of introduction section to the Lambda Calculus. Technically, the numbers I'm building are data structures, I suppose. But Okasaki's book is nothing if not seeped in functional language culture - which is to say it's concise and minimalist.

I'm dying to read it - and I think that's what I'll spend a lot of my time doing today. (It's only about 200pages. I might even finish it. Except that the examples are in ML - the granddaddy functional language - and not Scheme, so there's a bit of a curve for me getting used to the new notation.)

I'm ashamed to admit I took a peek at the first part of the Wiki page on Church numbers to make sure my addition function was right - and I stumbled across an interesting and obvious suggestion. On the Wiki page, addition is defined exactly as I defined it, only the order of arguments is reversed. So, translating from their functional notation back to Scheme:

(lambda (rator)
  (lambda (rand)
    (lambda (s)
      (lambda (z)
        (((rator s) ((rand s) z))))))

So I think I can maybe get my identity function idea to work after all. Here's why: now I can define the successor function (add1 in previous examples) actually defined as well - and that, effectively, makes my number a chain of explicit functions, as I wanted. I just have to define "successor" in such a way that it takes a function as an argument and does the right thing with it. It will be up to the number being subtracted to "exhaust" itself after so many such passes, leaving just a number, or something.

This is still a fuzzy idea, but it seems like another piece of the puzzle added.

I will have to take a solemn vow not to peek at Wikipedia from here out, though, because too many such hints and it's cheating.