language-agnostic - 自然数的 Church 数字编码是否不必要地复杂？

Question

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

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 表示数字的一种更直接、更直观的方式。这种方法是否存在问题，因此有充分的理由说明教堂数字以它们的方式工作吗？这种方法是否已经得到证实？

Answer 1

您的编码(零:λx.x，一:λx.λx.x，二:λx.λx.λx.x 等)使定义增量和减量变得容易，但除此之外，为您的编码开发组合器变得非常棘手。例如，您如何定义 isZero ?

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

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

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