我对 Lambda 演算中前任函数的 Wikipedia 描述感到困惑。
维基百科是这样说的：
PRED := λn.λf.λx. n (λg.λh. h (g f)) (λu.x) (λu.u)
有人可以逐步解释还原过程吗？
谢谢。
【问题讨论】：
(pred zero)、(pred one) 和 (pred two) 和 published it on Github. 使用 S 表达式进行了逐步简化/跨度>
好的，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 应用于 x 比 n 少一倍。
接下来，它将n 应用于三个参数。这是棘手的部分。
第二个参数，对应于之前的Z，是λu.x——一个忽略一个参数并返回x的常量函数。
第一个参数，对应于之前的S，是λgh.h (g f)。我们可以将其重写为 λg. (λh.h (g f)) 以反映只有最外层的 lambda 被应用 n 次的事实。这个函数所做的是将累积的结果带到g，并返回一个带有一个参数的新函数，该函数将该参数应用于g，应用于f。当然，这绝对令人困惑。
那么...这里发生了什么？考虑用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应用的次数比S对应的层数少一倍n。
【讨论】：
f 应用于 x 比 n 少一倍。”但它是如何实现这个目标的，从你的描述中我仍然无法理解。它可能有助于向这个公式添加更多抽象，将这些想法抽象到更高的层次。例如，通过将 Lu.u 替换为 I，标识函数。也许还有其他一些人。我在这里看到了一个有趣的解释：mactech.com/articles/mactech/Vol.07/07.05/LambdaCalculus/… 将这些 lambda 表达式解读为列表操作（cons,car,cdr）。
McCann 的回答很好地解释了这一点。让我们以 Pred 3 = 2 为例：
考虑表达式：n (λgh.h (g f)) (λu.x)。设K = (λgh.h (g f))
对于 n = 0，我们编码 0 = λfx.x，因此当我们对 (λfx.x)(λgh.h(gf)) 应用 beta 缩减时，意味着 (λgh.h(gf)) 被替换了 0 次。在进一步降低 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 的定义。
基于列表的实现可能更容易理解，但它需要许多中间步骤。所以它不如教会最初的实施 IMO 好。
【讨论】：
f 术语。例如 2 定义为λfx.f(fx)。这意味着当对 (λfx.f(fx))(λgh.h (g f)) 进行 beta 缩减时，(λgh.h (g f)) 函数会应用两次。
在阅读了之前的答案（好的答案）之后，我想给出我自己对此事的看法，希望它对某人有所帮助（欢迎指正）。我会举个例子。
首先，我想在定义中添加一些括号，让我更清楚地了解一切。让我们将给定的公式重新定义为：
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是教会数字，要应用的函数是λ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 作为f 和 0 作为x，我们得到：
PRED Three add1 0 := add1 (add1 0) = 2
希望这会有所帮助。
【讨论】：
你可以试着从延续的角度来理解前置函数（不是我最喜欢的）的这个定义。
为了简化问题，让我们考虑以下变体
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))，依此类推。
最后，我们将计算应用于恒等式 提取结果。
【讨论】：
我会将我的解释添加到上述好的解释中，主要是为了我自己的理解。这是 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 告诉我们在常数函数上评估 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.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)。
【讨论】：