21

我被 Wikipedia 对 lambda 演算中前任函数的描述所困扰。

维基百科说的是以下内容：

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

有人可以逐步解释减少过程吗？

谢谢。

4

5 回答 5

30

好的，所以 Church 数字的想法是使用函数对“数据”进行编码，对吧？工作方式是通过您将使用它执行的一些通用操作来表示一个值。因此，我们也可以朝另一个方向前进，这有时可以使事情变得更清楚。

教堂数字是自然数的一元表示。所以，让我们用Z表示零并Sn表示 的继任者n。现在我们可以这样计数：Z, SZ, SSZ, SSSZ... 等效的 Church 数字有两个参数——第一个对应于S，第二个对应于——Z然后使用它们来构造上述模式。所以给定参数f和x，我们可以这样计算：x, f x, f (f x), f (f (f x))...

让我们看看 PRED 做了什么。

首先，它创建一个带有三个参数n的 lambda——当然是我们想要其前身的 Church 数字，这意味着f和x是结果数字的参数，这意味着该 lambda 的主体将f应用于x一次比n会少。

接下来，它适用n于三个论点。这是棘手的部分。

第二个参数，对应Z于前面的，是λu.x一个常量函数，它忽略一个参数并返回x。

对应S于前面的第一个参数是λgh.h (g f)。我们可以重写它λg. (λh.h (g f))以反映只有最外层的 lambda 被应用的事实n。这个函数所做的是将累积的结果带到最远的地方，g并返回一个带有一个参数的新函数，该函数将该参数g应用于applyed to f。当然，这绝对令人困惑。

那么......这里发生了什么？S考虑用和直接替换Z。在非零数Sn中，n对应于绑定到 的参数g。因此，记住fand被x绑定在外部范围内，我们可以λu.x这样计数：一层，此时 an将应用它，而 a将忽略它。所以我们得到一个应用程序，除了最外层。λh. h ((λu.x) f)λh'. h' ((λh. h ((λu.x) f)) f)λu.xλh. h xλh'. h' (f x)SZfS

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

于 2012-01-10T01:32:00.120 回答
7

麦肯的回答很好地解释了这一点。让我们以 Pred 3 = 2 为例：

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

对于 n = 0，我们对 进行编码，因此当我们对均值0 = λfx.x应用 beta 缩减时，将被替换 0 次。在进一步减少 beta 后，我们得到：(λfx.x)(λgh.h(gf))(λgh.h(gf))

λ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 的定义。

基于列表的实现可能更容易理解，但它需要许多中间步骤。所以它不如教会最初的实施IMO好。

于 2016-05-13T02:47:09.823 回答
1

在阅读了以前的答案（好的答案）之后，我想给出我自己对此事的看法，希望它可以帮助某人（欢迎更正）。我将使用一个例子。

首先，我想在定义中添加一些括号，让我更清楚。让我们将给定的公式重新定义为：

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

让我们还定义三个有助于示例的 Church 数字：

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)))

结束于：

λ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 asf和 0 as x，我们得到：

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

希望这可以帮助。

于 2017-08-27T17:36:26.167 回答
0

我会将我的解释添加到上述好的解释中，主要是为了我自己的理解。这是 PRED 的定义：

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

第一个点右侧的内容应该是应用于 x 的 f 的 (n-1) 折叠组合：f^(n-1)(x)。

让我们通过逐步理解表达式来了解为什么会出现这种情况。

λu.x 是在 x 处取值的常数函数。让我们将其表示为 const_x。

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

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

好的，所以 PRED 告诉我们在常数函数上评估 F 的 n 倍组合，然后在恒等函数上评估结果。

PRED := λnfx. F^n const_x id

让我们仔细看看F：

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

F 将 g 发送到 g(f) 处的评估。让我们用 ev_y 表示值 y 的评估。即 ev_y := λh.hy

所以

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)。

于 2019-09-25T16:51:40.103 回答
0

您可以尝试从延续的角度来理解前置函数（不是我最喜欢的）的这个定义。

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

    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))，依此类推。

最后，我们将计算应用于恒等式以提取结果。

于 2017-01-21T21:50:15.887 回答