Lambda演算的前驱函数规约步骤

Question

Lambda演算的前驱函数规约步骤

21

我在lambda演算中的前导函数的维基百科描述上卡住了。

维基百科上的描述如下：

PRED := λn.λf.λx. n (λg.λh. h (g f)) (λu.x) (λu.u)

有人能够逐步解释一下缩减过程吗？

谢谢。

- user1004246

我发现 lambda 表示法很难理解，所以我使用 Clojure 对 (pred zero)、(pred one) 和 (pred two) 进行了逐步简化的 S-表达式，并在 Github 上发布了它。 - Agost Biro

6个回答

7

McCann的回答已经很好地解释了这个问题。我们来看一个具体的例子，令Pred 3 = 2:

考虑表达式：n (λgh.h (g f)) (λu.x)。令K = (λgh.h (g f))。

当n = 0时，我们将0编码成0 = λfx.x，因此当我们对(λfx.x)(λgh.h(gf))进行beta规约时，意味着(λgh.h(gf))不会被替换。进一步进行beta规约后，我们得到： λfx.(λu.x)(λu.u) 简化为 λfx.x 其中λfx.x = 0，这是预期的结果。

当n = 1时，我们将K应用于1次：

(λgh.h (g f)) (λu.x)
=> λh. h((λu.x) f)
=> λh. h x

当n = 2时，我们将K应用于2次：

(λgh.h (g f)) (λh. h x)
=> λh. h ((λh. h x) f)
=> λh. h (f x)

当n = 3时，我们将K应用于3次：

(λgh.h (g f)) (λh. h (f x))
=> λh.h ((λh. h (f x)) f)
=> λh.h (f (f x))

最后，我们将这个结果应用到一个id函数中，得到：

λh.h (f (f x)) (λu.u)
=> (λu.u)(f (f x))
=> f (f x)

这就是数字2的定义。

基于列表的实现可能更容易理解，但需要许多中间步骤。因此，在我看来，它不如Church的原始实现好。

- xin wang

我不明白如何从“对于n =某个值，我们将K应用某个次数”到每个推导的第一行。 - Zelphir Kaltstahl

是的，它并没有明确说明；但它来自于数字中的 f 项。例如，2 被定义为 λfx.f(fx)。这意味着当对 (λfx.f(fx))(λgh.h (g f)) 进行 beta 缩减时，(λgh.h (g f)) 函数被应用了两次。 - Greg

不可理解。 - Timur Fayzrakhmanov

1

在阅读之前的答案（不错的答案）后，我想分享一下自己的看法，希望能帮助到某些人（欢迎纠正）。我会用一个例子来说明。

首先，我想给定义加上一些括号，这让我更清楚地理解了。让我们重新定义给定的公式为：

PRED := λn λf λx.(n (λgλh.h (g f)) (λu.x)) (λu.u)

让我们还定义三个教堂数，以帮助这个例子：

Zero := λfλx.x
One := λfλx. f (Zero f x)
Two := λfλx. f (One f x)
Three := λfλx. f (Two f x)

为了理解这个过程的工作原理，让我们首先关注公式中的这一部分：

n (λgλh.h (g f)) (λu.x)

从这里，我们可以得出以下结论： n是一个Church数，要应用的函数是λgλh.h (g f)，起始数据是λu.x 有了这个理解，让我们试一个例子：

PRED Three := λf λx.(Three (λgλh.h (g f)) (λu.x)) (λu.u)

让我们先专注于数字的缩减（即我们之前解释过的部分）：

Three (λgλh.h (g f)) (λu.x)

转化为中文：

简化为：

(λgλh.h (g f)) (Two (λgλh.h (g f)) (λu.x))
(λgλh.h (g f)) ((λgλh.h (g f)) (One (λgλh.h (g f)) (λu.x)))
(λgλh.h (g f)) ((λgλh.h (g f)) ((λgλh.h (g f)) (Zero (λgλh.h (g f)) (λu.x))))
(λgλh.h (g f)) ((λgλh.h (g f)) ((λgλh.h (g f)) ((λfλx.x) (λgλh.h (g f)) (λu.x)))) -- Here we lose one application of f
(λgλh.h (g f)) ((λgλh.h (g f)) ((λgλh.h (g f)) (λu.x)))
(λgλh.h (g f)) ((λgλh.h (g f)) (λh.h ((λu.x) f)))
(λgλh.h (g f)) ((λgλh.h (g f)) (λh.h x))
(λgλh.h (g f)) (λh.h ((λh.h x) f))
(λgλh.h (g f)) (λh.h (f x))
(λh.h ((λh.h (f x) f)))

Ending up with:

λh.h f (f x)

所以，我们有:

PRED Three := λf λx.(λh.h (f (f x))) (λu.u)

再次简化：

PRED Three := λf λx.((λu.u) (f (f x)))
PRED Three := λf λx.f (f x)

如您所见，在这些缩减中，由于巧妙地使用函数，我们最终少应用了一次函数。

将add1用作“f”，将0用作“x”，我们得到：

PRED Three add1 0 := add1 (add1 0) = 2

希望这可以帮助到您。

- acontell

0

你可以尝试从continuations的角度理解前驱函数的定义（虽然这不是我最喜欢的定义方式）。

为了简化问题，让我们考虑以下变体。

    PRED := λn.n (λgh.h (g S)) (λu.0) (λu.u)

然后，您可以将S替换为f，将0替换为x。

函数的主体在参数N上迭代n次变换M。参数N是类型为（nat -> nat） -> nat的函数，它期望nat的继续并返回nat。最初，N = λu.0，即它忽略继续并只返回0。让我们称N为当前计算。

函数M：（nat -> nat） -> nat） ->（nat -> nat） -> nat将计算g：（nat -> nat） -> nat修改如下。它以输入继续h，并将其应用于使用S继续当前计算g的结果。

由于初始计算忽略了继续，因此经过一次M的应用，我们得到计算（λh.h 0），然后是（λh.h（S 0）），依此类推。

最后，我们将计算应用于身份继续以提取结果。

- Andrea Asperti

0

分割这个定义

PRED := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)

分为4个部分：

PRED := λn.λf.λx. | n | (λg.λh.h (g f)) | (λu.x) | (λu.u)
                    -   ---------------   ------   ------
                    A   B                 C        D

现在先忽略 D。根据 Church 数字的定义，A B C 是 B^n C：对 C 应用 n 次 B 的折叠。

现在将 B 视为将一个输入转换为一个输出的机器。它的输入 g 的形式为 λh.h *，当附加上 f 时，变成了 (λh.h *) f = f *。这增加了一个应用程序到 * 中的 f。结果 f * 然后被前置 λh.h 变成了 λh.h (f *)。

你看到了这个模式：每次应用 B 将 λh.h * 转换为 λh.h (f *)。如果我们以 λh.h x 作为起始项，那么在 n 次应用 B 后，我们将得到 λh.h (f^n x) 作为结束项。

然而，起始项是C = (λu.x)，当附加f时，变成(λu.x) f = x，然后在前面加上λh.h变成λh.h x。因此，在第一个B应用之后，我们得到了λh.h x，而不是之前。这就是为什么我们有λh.h (f^(n-1) x)作为结束项的原因：第一次应用f被忽略了。

最后，将λh.h (f^(n-1) x)应用于D = (λu.u)，即恒等式，得到f^(n-1) x。也就是说：

PRED := λn.λf.λx.f^(n-1) x

- Cyker

0

我会在上面的好回答中加入我的解释，主要是为了自己的理解。这里再次给出PRED的定义：

PRED := λnfx. (n (λg (λh.h (g f))) )  λu.x λu.u

第一个点号右边的东西应该是f对x做(n-1)次复合后的结果：f^(n-1)(x)。

我们逐步理解这个表达式，来看一下为什么会这样。

λu.x是以x为值的常函数。我们简称它为const_x。

λu.u是恒等函数。我们称之为id。

λg (λh.h (g f))是一个我们需要理解的奇怪函数。我们称之为F。

好的，所以PRED让我们对常函数做n次F的组合，然后对结果进行恒等函数的求值。

PRED := λnfx. F^n const_x id

让我们更仔细地看一下 F：

F:= λg (λh.h (g f))

在编程中，F将G发送到G（F）进行评估。我们用ev_y表示值y的评估。也就是说，ev_y：= λh.h y

因此，

F = λg. ev_{g(f)}

现在我们弄清楚了 F^n const_x 是什么。

F const_x = ev_{const_x(f)} = ev_x

并且

F^2 const_x = F ev_x = ev_{ev_x(f)} = ev_{f(x)}

同样地，

F^3 const_x = F ev_{f(x)} = ev_{f^2(x)}

等等：

F^n const_x = ev_{f^(n-1)(x)}

现在，

PRED = λnfx. F^n const_x id

     = λnfx. ev_{f^(n-1)(x)} id

     = λnfx. id(f^(n-1)(x))

     = λnfx. f^(n-1)(x)

这正是我们想要的。

非常滑稽。这个想法是将做某事n次变成做f (n-1)次。解决方案是对const_x应用F n次，以获得ev_{f^(n-1)(x)}，然后通过在单位函数上评估来提取f^(n-1)(x)。

- Dmitri Gekhtman

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- C. A. McCann · Accepted Answer

好的，Church数是使用函数对“数据”进行编码的想法，对吗？这种方法是通过用一些通用操作来表示值来实现的。因此，我们也可以反过来做，有时可能会使事情更清晰。

Church数是自然数的一元表示法。因此，让我们使用Z表示零，使用Sn表示n的后继。现在我们可以这样计数：Z、SZ、SSZ、SSSZ……等等。相应的Church数需要两个参数 - 第一个对应于S，第二个对应于Z - 然后使用它们来构建上述模式。因此，给定参数f和x，我们可以这样计数：x、f x、f (f x)、f (f (f x))……等等。

现在看看PRED函数的作用。

首先，它创建一个带有三个参数的lambda函数，其中n是我们想要前任的Church数，而f和x是生成的数字的参数，因此该lambda函数的主体将是f将会比n少应用一次的x。

接下来，它将n应用于三个参数。这是棘手的部分。

从之前的Z对应的第二个参数来看，它是一个常数函数λu.x，它会忽略一个参数并返回x。

第一个参数对应之前的 S，为 λgh.h (g f)。我们可以将其重写为 λg. (λh.h (g f))，以反映仅应用最外层的 lambda n 次。这个函数所做的是将到目前为止累积的结果作为 g 并返回一个新函数，该函数接受一个参数，将该参数应用于 f 应用于 g。当然，这有点令人困惑。

那么... 这里发生了什么？考虑使用 S 和 Z 进行直接替换。在非零数字 Sn 中，n 对应于绑定到 g 的参数。因此，记住 f 和 x 在外部作用域中绑定，我们可以这样计数：λu.x、λh. h ((λu.x) f)、λh'. h' ((λh. h ((λu.x) f)) f)... 执行明显的简化，我们得到：λu.x、λh. h x、λh'. h' (f x)... 这里的模式是将一个函数 "向内" 传递一层，此时一个 S 将应用它，而 Z 将忽略它。因此，对于每个 S，我们会得到一个 f 的应用，除了最外层。

第三个参数只是简单的恒等函数，由最外层的 S 忠实地应用，返回最终结果——f 的应用次数比 n 对应的 S 层数少一次。