lambda - lambda 演算的语法树

Question

我试图弄清楚如何为下面的表达式绘制语法树。首先，这究竟是如何表现的？看起来它需要 1 和 2 作为参数，如果n是 0，它只会返回m。

另外，有人可以指出解析树的起点，还是一个例子？我一直找不到。

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.