Jerzy Karczmarczuk wrote:
> 6. Subtraction. Largo.
> According to some folklore Church himself thought for some time
> that it is not possible to define the subtraction using pure
> lambdas.
> In fact it is possible to subtract Church numerals (but never
> getting negative numbers, of course) The following solution is
> silly, but please find a *really* better one...
>
> First the incrementation: inc n s z = n s (s z)
> (You may use it also to define the addition.)
>
> Then the iteration defining the decrement
> dec n = d zer where
> zer s z = z
> v = n s z -- global constants
> d m = let h = inc m
> in if h s z == v then m else d (inc m)
> and the subtraction is the iterated decrement. Its complexity
> is really bad (n^2).
Compared to using equality, I think the following is really better:
dec n = fst (n (\(_,b)->(b,inc b)) (zer,zer)) where zer s z = z
Of course, you wouldn't really use built-in pairing, would you?
Christian Sievers
