函数式编程中的λ演算

Question

在λ演算中，(λ x. λ y. λ s. λ z. x s (y s z)) 用于将两个 Church 数加起来。如何解释这个过程？是否有关于函数式编程的λ演算的好资源？非常感谢您的帮助。

- dinsim

---

请查看页面右侧的“相关”部分：https://dev59.com/LHRB5IYBdhLWcg3wyqAd，https://dev59.com/aXNA5IYBdhLWcg3wNa-T等。 - vgru

Answer 1

实际上λ f1. λ f2. λ s. λ z. (f1 s (f2 s z)) 计算加法，因为它有效地将(f2 s z)即f2代表的数字替换到(f1 s z)中的“零”的位置。

例如：我们取f2为二进制的ssz。f1是一：s z。将最后一个z替换为f2，您会得到sss z，即三的扩展形式。

这需要黑板和手势讲解，抱歉。

- Pascal Cuoq

Answer 2

在λ演算中，您可以通过其引导的操作来编写数据类型。例如，布尔值只是一个选择函数，它接受两个值a和b作为输入，并返回a或b：

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

自然数有什么用？它主要的计算目的是提供迭代的界限。因此，我们将自然数编码为一个运算符，该运算符接受一个函数f和一个值x作为输入，并在x上迭代地应用f n次。

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

有 f 函数的 n 次出现。

现在，如果您想从 x 开始迭代函数 f n + m 次，则必须先迭代 n 次，即 (n f x)，然后从前一个结果开始迭代 m 次，即

                                m f (n f x)

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

                                 m (n f) x  

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

- Andrea Asperti