[tsimionescu]

I will note though that in the actual lambda calculus there is no "+", "2" or "1" - it's functions all the way.

1 is typically defined in the Church encoding as \f -> \x -> f x. Addition is \m -> \n -> \f -> \x -> m f (n f x). Finding the Church encoding of 2 is left as an exceecise.

We can then use beta reduction to compute 1 + 1 by replacing m and n with 1:

  1 = \f -> \x -> f x
  (\m -> \n -> \f -> \x -> m f (n f x)) 1 1 =>beta
  \f -> \x -> 1 f (1 f x)

  \f -> \x -> 1 f x = (\f -> \x -> f x) f x =>beta
  1 f x = f x

  \f -> \x -> 1 f (1 f x) <=> \f -> \x -> 1 f (f x)

  (\f -> \x -> f x) f (f x) =>beta
  \f -> \x -> f f x - the Church encoding of 2.

This is how computation using beta reduction only looks like.

[opnitro]

Yup, was just trying to give an example that utilized primitives to make it easier.

[tsimionescu]

Yes yes, I wanted to add to your example, not to say that you said anything wrong!