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.

Answer 2

In lambda calculus, you code a datatype in terms of the operations it induces. For instance, a boolean is a just a choice function that takes in input two values a and b and either returns a or b:

                      true = \a,b.a   false = \a,b.b

What is the use of a natural number? Its main computational purpose is to provide a bound to iteration. So, we code a natural number as an operator that takes in input a function f, a value x, and iterate the application of f over x for n times:

                        n = \f,x.f(f(....(f x)...))

with n occurrences of f.

Now, if you want to iterate n + m times the function f starting from x you must start iterating n times, that is (n f x), and then iterate for m additional times, starting from the previous result, that is

                                m f (n f x)

Similarly, if you want to iterate n*m times you need to iterate m times the operation of iterating n times f (like in two nested loops), that is

                                 m (n f) x  

The previous encoding of datatypes is more formally explained in terms of constructors and corresponding eliminators (the so called Bohm-Berarducci encoding).