用于函数式编程的 lambda 演算
在 lambda 演算中 (λ x. λ y. λ s. λ z. xs (ysz)) 用于添加两个丘奇数字，我们如何解释这一点，是否有任何用于函数式编程的 lambda 演算的好资源？非常感谢你的帮助
in lambda calculus (λ x. λ y. λ s. λ z. x s (y s z)) is used for addition of two Church numerals how can we explain this, is there any good resource the lambda calculus for functional programming ? your help is much appreciated
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
实际上是λf1。 λf2。 λ s。 λz。 (f1 s (f2 sz)) 计算加法，因为它实际上是将 f2 表示的数字 (f2 sz) 替换为 (f1 sz) 内的“零”。
示例：让我们以扩展形式的 f2、
ss z取两个。 f1 是一：s z。将最后一个z替换为 f2，您将得到sss z，即 3 的扩展形式。抱歉，如果有黑板和挥手，这会更容易。
Actually λ f1. λ f2. λ s. λ z. (f1 s (f2 s z)) computes addition because it is in effect substituting (f2 s z), the number represented by f2, to the "zero" inside (f1 s z).
Example: Let's take two for f2,
s s zin expanded form. f1 is one:s z. Replace that lastzby f2 and you gets s s z, the expanded form for three.This would be easier with a blackboard and hand-waving, sorry.
在 lambda 演算中，您可以根据数据类型引发的操作来编写数据类型的代码。例如，布尔值只是一个选择函数，它接受输入两个值 a 和 b，然后返回 a 或 b：
自然数有什么用？其主要计算目的是
提供迭代的界限。因此，我们将自然数编码为运算符
接受输入函数 f、值 x，并迭代应用程序
f 超过 x n 次：
f 出现 n 次。
现在，如果您想从 x 开始迭代函数 f n + m 次
你必须开始迭代n次，即(nfx)，然后迭代m次
额外的次数，从之前的结果开始，也就是说
同样的，如果要迭代n*m次就需要迭代m次
迭代 n 次 f 的操作（就像在两个嵌套循环中一样），即
之前的数据类型编码更正式地解释为
构造函数和相应的消除器（所谓的
Bohm-Berarducci 编码）。
In lambda calculus, you code a datatype in terms of the operations it induces. For instance, a boolean is a just a choice function that takes in input two values a and b and either returns a or b:
What is the use of a natural number? Its main computational purpose is to
provide a bound to iteration. So, we code a natural number as an operator
that takes in input a function f, a value x, and iterate the application
of f over x for n times:
with n occurrences of f.
Now, if you want to iterate n + m times the function f starting from x
you must start iterating n times, that is (n f x), and then iterate for m
additional times, starting from the previous result, that is
Similarly, if you want to iterate n*m times you need to iterate m times
the operation of iterating n times f (like in two nested loops), that is
The previous encoding of datatypes is more formally explained in terms
of constructors and corresponding eliminators (the so called
Bohm-Berarducci encoding).