Church numeral for addition

Question

Hi All,

I am stuck up at the following step. It will be great if someone can help me out:

2 = λfx.f(f x)
3 = λfx.f(f(f x))
ADD = λm n f x. m f (n f x)

My steps are:

   (λm n f x. m f (n f x)) (λf x.f(f(f x))) (λf x.f(f x))
-> ((λn f x. (λf x.f(f(f x))) f (n f x))) (λf x.f(f x))
-> ((λf x. (λf' x'.f'(f'(f' x'))) f ((λf" x".f"(f" x")) f x)

Is the parenthesis fine? I really confuse myself on the substitutions and parenthesis. Is there a formal, easier technique to address such problems?

regards, darkie

Answer 1

Try Alligator Eggs!

Here are my steps, which I derived with the help of Alligator Eggs:

ADD 2 3
-> (λm n f x. m f (n f x)) (λf x.f(f(f x))) (λf x.f(f x))
->   (λn f x. (λf x.f(f(f x))) f (n f x))   (λf x.f(f x))
->     (λf x. (λf x.f(f(f x))) f ((λf x.f(f x)) f x)) 
->     (λf x.   (λx.f(f(f x)))   ((λf x.f(f x)) f x)) 
->     (λf x.       f(f(f(λf x.f(f x)) f x)))))
->     (λf x.       f(f(f  (λx.f(f x)) x)))))
->     (λf x.       f(f(f     (f(f x))  )))))

Answer 2

Is there a formal, easier technique to address such problems?

It is much easier to write a reducer and prettyprinter for lambda terms than it is to do reductions by hand. But PLT Redex can give you a leg up on the reductions; try defining rules for normal-order reduction, and then all you have to do is worry about prettyprinting the results with no redundant parentheses.

You will probably learn a lot more, too.