自然数的 Church 数字编码是否不必要地复杂？答案

【问题标题】：Is the Church numeral encoding of natural numbers unnecessarily complicated?自然数的 Church 数字编码是否不必要地复杂？
【发布时间】：2012-02-11 01:52:54
【问题描述】：

我一直在阅读的计算机程序的结构和解释一书通过定义零和增量函数来介绍教堂数字

zero: λf. λx. x
increment: λf. λx. f ((n f) x)

这对我来说似乎很复杂，我花了很长时间才弄清楚并推导出一个 (λf.λx. f x) 和两个 (λf.λx. f (f x))。

用这种方式编码数字不是更简单吗，零是空的 lambda？

zero: λ
increment: λf. λ. f

现在很容易推导出一个 (λ. λ) 和两个 (λ. λ. λ)，以此类推。

这似乎是一种用 lambda 表示数字的更直接、更直观的方式。这种方法是否存在一些问题，因此有充分的理由说明教堂数字以它们的方式工作吗？这种方法是否已经得到证实？

【问题讨论】：

我不确定我看到这个问题有什么问题。谁能解释一下？
我没有投过票，但可能人们觉得它更适合 ctheory 什么的？
CSTheory 用于研究级别的问题。这个可能太初级了。
我认为可以对标题进行清理，使其听起来更客观，并与帖子的其余部分保持一致，这将使它成为一个整体上更好的问题。
我同意这不属于 CS Theory SE，但它也不完全是代码的特定编程问题。即便如此，对于我的 +1 来说已经足够了。

标签： language-agnostic sicp lambda-calculus church-encoding

【解决方案1】：

您的编码（零：λx.x，一：λx.λx.x，二：λx.λx.λx.x 等）可以轻松定义增量和减量，但除此之外，为您的编码开发组合器变得非常棘手。例如，您如何定义isZero？

考虑 Church 编码的一种直观方式是，数字 n 由迭代 n 次的动作表示。这使得开发像plus 这样的组合子很容易，只需使用数字中编码的迭代即可。递归不需要花哨的组合器。

在 Church 编码中，每个数字都有相同的接口：它需要两个参数。在您的编码中，每个数字都由它所接受的参数数量定义，这使得统一操作非常棘手。

另一种编码数字的方法是将数字视为 n = 0 | S n，并为 unions 使用 vanilla 编码。

【讨论】：

【解决方案2】：

建议的数字语法在 lambda 演算中无效，而 Church 数字在 lambda 演算中确实是有效的结构。因此，这可能是 Church 数字如此的一个原因 - 数字编码必须遵守 lambda 演算的definition，其方式也允许在 lambda 演算中定义的进一步操作（例如，增量）在编码数字。

【讨论】：

我好像没看懂，在 lambda 演算中无效怎么办？出于某种原因，是否不允许使用空 lambda？如果这是问题所在，那么给它一个它基本上忽略并使其非空的虚拟参数将是微不足道的。
看看grammar（不是扩展的，只有基本的）。无论您为数字选择什么编码，它都必须尊重该语法——这是您提议的编码所不具备的
这真的不解释。我在问你哪部分我的编码违反了语法？似乎我的唯一形式与其他形式不同的是空 lambda，可以用λx.x 轻松替换。
它确实，例如根据语法，这不是有效的 lambda 函数λ.λ（根据您的编码，这是数字 1）。另一方面，λf.λx. f x 是完全有效的，这就是数字 1 的表示 chosen。理解这一点：你不能选择任意的符号串，它们必须在微积分的语法下是有效的，而你的不是
我了解语法：我什至写过代码解析器。我有点恼火，你一直在强调我使用的符号，经过一些简单的替换，根据你链接到的语法是有效的。如果您愿意，我可以将我的符号更改为更传统，并使用它来解释我的方法，但是您的回答，就目前而言，并没有真正解决我的问题。