Once the function is defined, you execute the application of the arguments of the function itself, thus returning new functions, resulting application arguments.
I'm not sure what language you used this code in, but the application will result in something like:
\f.\n.\m.if isZero n then m else f (pred n) (succ m)
Since \f is a function definition, you can write above:
add = (\n.\m.if (isZero n) then m else add (pred n) (succ m))
And applications:
add = (\n.\m.if (isZero n) then m else add (pred n) (succ m)) add 1 2 (\n.\m.if (isZero n) then m else add (pred n) (succ m)) 1 2
Replacing the outer variable with the innermost argument (in this case, n by 1):
((**\n**.\m.if (isZero n) then m else f (pred **n**) (succ m)) **1**) 2 (\m.if (isZero 1) then m else add (pred 1) (succ m)) 2
By resolving this a bit:
(\m.if (isZero 1) then m else add **(pred 1)** (succ m)) 2 (\m.if (isZero 1) then m else add 0 (succ m)) 2
Application of the second argument and resolution:
(**\m**.if (isZero 1) then **m** else add 0 (succ **m**)) **2** (if (isZero 1) then 2 else add 0 (succ 2)) (if (isZero 1) then 2 else add 0 **(succ 2)**) (if (isZero 1) then 2 else add 0 3)
We know (isZero 1) falsely; therefore, we solve the above expression and get the following:
(if **(isZero 1)** then 2 else add 0 3) (if False then 2 else add 0 3) add 0 3
Same as applying 0 to the function f, and then 3 to the result. The above expression can be read as: "f": 0 applies to "f" and 3 applies to the result of the previous application.
But f was previously defined as:
(\f.\n.\m.if (isZero n) then m else f (pred n) (succ m))
So in this case you will have:
add = (\f.\n.\m.if (isZero n) then m else f (pred n) (succ m)) add 0 3 = \n.\m.if (isZero n) then m else add (pred n) (succ m)) 0 3 = **\n**.\m.if (isZero **n**) then m else add (pred **n**) (succ m)) **0** 3 = \m.if (isZero 0) then m else add (pred 0) (succ m)) 3 = **\m**.if (isZero 0) then **m** else add (pred 0) (succ **m**)) **3** = if (isZero 0) then 3 else add (pred 0) (succ 3)) = if **(isZero 0)** then 3 else add (pred 0) (succ 3)) = if True then 3 else add (pred 0) (succ 3)) = 3
In the syntax tree, you just have to show the decompositions, reaching result 3.
As a simpler example of the application process, counting the "sum" function, defined as (\ x. \ Yx + y), the result (sum 3 2) will be:
(sum 3 2) ((sum 3) 2) (((sum) 3) 2) (((\x.\yx + y) 3) 2) ((\y.3 + y) 2) (3 + 2) 5
There are no restrictions on the order that solves expressions; it is proved that lambda calculus has the same result, whatever the order of abbreviations used. See link .
As Giorgio noted, Y is a fixed-point combinator that allows you to stop iterating at a specific point if you access the same expressions.
Since the application requires a finite number of iterations, the solution will be the same by simply noting the sign of a fixed combination of pointers:
Y = (\f.\n.\m.if (isZero n) then m else f (pred n) (succ m)) Y add = (\f.\n.\m.if (isZero n) then m else f (pred n) (succ m)) add Y add = (**\f**.\n.\m.if (isZero n) then m else **f** (pred n) (succ m)) **add** Y add = \n.\m.if (isZero n) then m else add (pred n) (succ m) Y add 0 3 = \n.\m.if (isZero n) then m else add (pred n) (succ m)) 0 3 = **\n**.\m.if (isZero **n**) then m else add (pred **n**) (succ m)) **0** 3 = \m.if (isZero 0) then m else add (pred 0) (succ m)) 3 = **\m**.if (isZero 0) then **m** else add (pred 0) (succ **m**)) **3** = if (isZero 0) then 3 else add (pred 0) (succ 3)) = if **(isZero 0)** then 3 else add (pred 0) (succ 3)) = if True then 3 else add (pred 0) (succ 3)) = 3
A reference to a fixed-point combinator .