We have a successor function, but we don't have a predecessor function. To define it we need a different abstraction though: the pair!
pair a b f = f a b
1st p = p true
2nd p = p false
[We're using Haskell-like syntax now. This means that (bla a = b) is the same as (bla = (\ a -> b)). Oh, and we're using \ at the beginning of lambda expressions, too.]
pair works because you usually only supply 2 arguments -- and when you want to use them, pass a function to them. You can also extract the 1st and 2nd elements using 1st and 2nd, which use true and false to select the correct element, respectively.A few examples of using pair (in our imaginary lambda calculus interpreter):
> 1st (pair 42 13)
42
> 2nd (pair 42 13)
13
> pair 42 13 add
55
> pair 10 (pair 20 30) (\a b -> pair (pair a (1st b)) (2nd b))
pair (pair 10 20) 30
We can now use pair to create our predecessor function:
pred n = 1st (n (\p -> pair (2nd p) (suc (2nd p))) (pair 0 0))
This is complicated, so I'll go through this with you. You start with
(pair 0 0), and apply (\p -> pair (2nd p) (suc (2nd p))), n times. What each of those applications does is, in effect, it transforms the pair (a, b) into the pair (b, b+1). So, by the time you've applied it n times to the pair (0, 0), you get the pair (n - 1, n). Then all you have to do is get the 1st element using 1st. That's it!If you do
(pred 0), it returns 0, but we can make an alternate version of pred that takes care of this:pred_ x n = 1st (n (\p -> pair (2nd p) (succ (2nd p))) (pair x 0))
Another way to define
pred now is:pred = pred_ 0
We can now do subtraction:
sub a b = a pred b
or
sub_ x a b = a (pred_ x) b
sub = sub_ 0
For division we need a predicate. Predicates are functions that return either true or false:
not b = b false true
is0? n = n (\x -> false) true
ge? a b = is0? (sub b a)
lt? a b = not (ge? a b)
not inverts a boolean, is0? asks whether or not a number is 0, ge? asks if one number is greater than or equal to the other, and le? asks if a number is less than another. We can now do division and modulo (remainder):div a b = lt? a b 0 (suc (div (sub a b) b))
mod a b = lt? a b a (mod (sub a b) b)
You learned about pairs, predecessors, predicates, and powerful arithmetic, today. Tomorrow: Lists! Can't wait! :)