Lambda calculus for functional programming

Question

in the lambda calculus (λ x. λ y. λ s. λ z. xs (ysz)) is used to add two digits in the Church, how can we explain this, is there a good resource for lambda calculus for functional programming? your help is much appreciated

Answer 1

In fact, λ f1. λ f2. λ s. λ z. (f1 s (f2 sz)) computes the addition because it actually replaces (f2 sz), the number represented by f2 with a "zero" inside (f1 sz).

Example: take two for f2, ssz in extended form. f1 - one: sz . Replace the last z with f2 and you get sssz , an extended form for three.

It would be easier with a board and a manual swing, sorry.

Answer 2

In lambda calculus, you encode a data type in terms of the operations it invokes. For example, a boolean is simply a selection function that takes two input values ​​a and b and returns a or b:

  true = \a,ba false = \a,bb 

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

  n = \f,xf(f(....(fx)...)) 

with n occurrences f.

Now, if you want to iterate n + m times, the function f starting with x you should start iterating n times, that is (nfx), and then iterating for m extra times, starting from the previous result, i.e.

  mf (nfx) 

Similarly, if you want to iterate n * m times, you need to repeat the iteration operation m times n times f (as in two nested loops), i.e.

  m (nf) x 

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