Syntax tree for lambda calculus

Question

I'm trying to figure out how I would draw a syntax tree for the expression below. First, how exactly is this behaving? It looks like it takes 1 and 2 as parameters, and if n is 0, it will just return m.

Also, could someone point a start off to parse tree, or an example? I haven't been able to find one.

Answer 1

Once the function is defined, you do applications of the arguments on the function itself, returning, thus, new functions, resultants of the applied args.

I'm not sure which language you used to wirte that code, but the application would result in something like:

\f.\n.\m.if isZero n then m else f (pred n) (succ m)

Since \f is the definition of the function, you can write the above as:

add = (\n.\m.if (isZero n) then m else add (pred n) (succ m))

And the 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 outermost 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

Resolving it 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

Applying the second argument, and resolving:

(**\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) is false; so, we solve the above expression and have the resulting:

(if **(isZero 1)** then 2 else add 0 3)
(if False then 2 else add 0 3)
add 0 3

Which is the same as of applying 0 to function f, and then, 3 to the result. The above expression may be read as: "f" is: 0 applied to "f", and 3 applied to the result of the former application.

But f's been defined formerly as:

(\f.\n.\m.if (isZero n) then m else f (pred n) (succ m))

So, in this case, you'd 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 would simply show the expansions, reaching the result 3.

As a more straightforward example of the application process, considering the function "sum", defined as (\x.\y.x + y), the result of (sum 3 2) would be:

(sum 3 2)
((sum 3) 2)
(((sum) 3) 2)
(((\x.\y.x + y) 3) 2)
((\y.3 + y) 2)
(3 + 2)
5

There's no restraint on the order one solves the expressions; lambda calculus is proved to have the same result what ever may be the order of the reductions used. See ref.

As pointed out by Giorgio, Y is a fixed point combinator, that allows you to stop iterating at a certain point, if you're applications return to the same expression.

Since the application requires a finite number of iterations, the solution would be the same, simply noting the fixed pointer combination mark:

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

Reference to fixed point combinator.