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?

Selfannihilation

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))  )))))

Rianna

thank you so very much. Frankly, I did not understand how to go about with the Alligator eggs! – Selfannihilation

I once stumbled upon these alligators, but it seemed to me as freakings of some madman. Though I know Lambda Calculus quite well, I couldn't figure out what those alligators have to do with it and how could it help with interpreting it :-P So my personal opinion is that it doesnt' help much with understanding LC, but introduces additional confusion. – Bee

I understand designing Turing machine to compute "adding two numbers". In fact there are many good you tube short videos explaining this - however Lambda calculus model I am finding hard to understand. Any good pointers, please ? – Cotoneaster

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

Tman

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.

Boathouse

10 years later with the same problem. Looks like PLT Redex was moved (redex.racket-lang.org). – Arthritis