用于函数式编程的 lambda 演算

Question

在 lambda 演算中 (λ x. λ y. λ s. λ z. x s (y s z)) 用于两个 Church 数字的加法，我们如何解释这一点，有没有什么好的资源用于函数式编程的 lambda 演算？非常感谢您的帮助

Answer 1

实际上是λ f1。 λ f2。 λs。 λz。 (f1 s (f2 s z)) 计算加法，因为它实际上是将 f2 表示的数字 (f2 s z) 替换为 (f1 s z) 内部的“零”。

示例：让我们为 f2 取两个，s s z 的扩展形式。 f1 为一：s z。将最后一个 z 替换为 f2，您将得到 s s s z，这是三个的扩展形式。

用黑板和挥手会更容易，抱歉。

Answer 2

在 lambda 演算中，您根据数据类型引发的操作对数据类型进行编码。例如，布尔值只是一个选择函数，它接受输入两个值 a 和 b，并返回 a 或 b：

                      true = \a,b.a   false = \a,b.b

自然数有什么用？其主要计算目的是 提供迭代的界限。因此，我们将自然数编码为运算符 它接受输入一个函数 f、一个值 x，并迭代应用程序 f 超过 x 的 n 次：

                        n = \f,x.f(f(....(f x)...))

f 出现 n 次。

现在，如果你想从 x 开始迭代 n + m 次函数 f 您必须开始迭代 n 次，即 (n f x)，然后迭代 m 额外的时间，从之前的结果开始，也就是

                                m f (n f x)

同样，如果你想迭代 n*m 次，你需要迭代 m 次 迭代 n 次 f 的操作（就像在两个嵌套循环中一样），即

                                 m (n f) x  

前面的数据类型编码更正式地解释为 构造函数和相应的消除器（所谓的 Bohm-Berarducci 编码）。