lambda-calculus - Lambda 演算前导函数约简步骤

Question

我被 Wikipedia 对 lambda 演算中前任函数的描述所困扰。
维基百科说的是以下内容:

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

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

Answer 1

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

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

让我们看看 PRED 做了什么。

首先，它创建一个带有三个参数的 lambda -- n当然，是我们想要其前身的教堂数字，这意味着 f和 x是结果数字的参数，因此这意味着该 lambda 的主体将是 f申请x比 n 少一次将。

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

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

第一个参数，对应于 S从之前，是 λgh.h (g f) .我们可以将其重写为 λg. (λh.h (g f))以反射(reflect)仅应用最外层 lambda 的事实 n次。这个函数所做的是将累积的结果带到g。并返回一个带有一个参数的新函数，该函数将该参数应用于 g申请f .当然，这绝对令人困惑。

那么......这里发生了什么？考虑用 S 直接替换和 Z .在非零数中 Sn , n对应于绑定(bind)到 g 的参数.所以，记住 f和 x绑定(bind)在外部范围内，我们可以这样计算:λ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会忽略它。所以我们得到了一份 f 的申请。对于每个 S除了最外面的。

第三个参数是简单的恒等函数，由最外层的 S 尽职尽责地应用。 ，返回最终结果-- f应用次数比 S 的数量少一次层 n对应。