Church numeral for addition

Question

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?

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

My advice, from my own limited but recent experience:

1. Do one thing at a time: perform an alpha conversion, a beta reduction or an eta conversion. Note in the margin of the page you're working on what step you've taken to reach the next line. If those words aren't familiar to you, what they do will be - just take a look on Wikipedia.

A quick summary of these reduction steps:

Alpha just means change the names of variables in a context consistently:

λfx. f (f x) => λgx. g (g x)

Beta just means apply the lambda to one argument

(λf x. f x) b => λx. b x

Eta is simply 'unwrapping' an unnecessarily wrapped function that doesen't change its meaning.

λx.f x => f

Then

2. Use lots of alpha conversion to change the names of the variables to make things clearer. All those fs, it's always going to be confusing. You've done something similar with the " on your second row

3. Pretend you're a computer! Don't leap ahead or skip a step when you're evaluating an expression. Just do the next thing (and only one thing). Only move faster once you're confident moving slowly.

4. Consider naming some of the expressions and only substituting them for their lambda expressions when you need to evaluate them. I usually note the substitution in the margin of the page as by def as it's not really a reduction step. Something like:

   add two three 
   (λm n f x. m f (n f x)) two three | by def
   

So following the above rules, here's my worked example:

two   = λfx. f (f x)
three = λfx. f (f (f x))
add   = λmnfx. m f (n f x)

0  | add two three 
1  | (λm n f x. m f (n f x)) two three           | by def
2  | (λn f x. two f (n f x)) three               | beta
3  | (λf x. two f (three f x))                   | beta
4  | (λf x. two f ((λfx. f (f (f x))) f x))      | by def
5  | (λf x. two f ((λgy. g (g (g y))) f x))      | alpha
6  | (λf x. two f ((λy. f (f (f y))) x))         | beta
7  | (λf x. two f (f (f (f x))))                 | beta
8  | (λf x. (λfx. f (f x)) f (f (f (f x))))      | by def
9  | (λf x. (λgy. g (g y)) f (f (f (f x))))      | alpha
10 | (λf x. (λy. f (f y)) (f (f (f x))))         | beta
11 | (λf x. (λy. f (f (f (f (f x))))))           | beta

Answer 3

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.