lambda - lambda 演算的语法树

Question

我想弄清楚如何为下面的表达式绘制语法树。首先，这究竟是如何表现的？看样子是以1和2为参数，如果n是 0，它只会返回 m .



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

Answer 1

一旦定义了函数，您就可以在函数本身上应用参数，从而返回新函数，即应用参数的结果。

我不确定您使用哪种语言编写该代码，但该应用程序会导致类似以下内容:

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

自 \f是函数的定义，你可以把上面写成:

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

和应用程序:

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

用最里面的参数替换最外面的变量(在本例中， n 用 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

稍微解决一下:

(\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

应用第二个参数，并解决:

(**\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)

我们知道 (isZero 1) 是假的；所以，我们解决上面的表达式并得到结果:

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

这与将 0 应用于函数 f，然后将 3 应用于结果相同。
上面的表达式可以理解为:“f”是:0 应用于“f”，3 应用于前一个应用的结果。

但是 f 以前被定义为:

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

因此，在这种情况下，您将拥有:

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

在语法树中，您只需显示扩展，即可达到结果 3。

作为应用过程的一个更直接的例子，考虑函数“sum”，定义为 (\x.\y.x + y)，(sum 3 2) 的结果将是:

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

求解表达式的顺序没有限制； lambda 演算被证明具有相同的结果，无论使用的归约顺序如何。
See ref .

正如 Giorgio 所指出的， Y是一个定点组合器，它允许您在某个点停止迭代，如果您的应用程序返回到相同的表达式。

由于应用程序需要有限次数的迭代，因此解决方案是相同的，只需注意固定指针组合标记:

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

引用 fixed point combinator .