lambda calculus for functional programming

Question

in lambda calculus (λ x. λ y. λ s. λ z. x s (y s z)) is used for addition of two Church numerals how can we explain this, is there any good resource the lambda calculus for functional programming ? your help is much appreciated

Answer 1

Actually λ f1. λ f2. λ s. λ z. (f1 s (f2 s z)) computes addition because it is in effect substituting (f2 s z), the number represented by f2, to the "zero" inside (f1 s z).

Example: Let's take two for f2, s s z in expanded form. f1 is one: s z. Replace that last z by f2 and you get s s s z, the expanded form for three.

This would be easier with a blackboard and hand-waving, sorry.