了解教会数字

如何解决了解教会数字

我正在研究 SICP，它为 Church Numerals 给出了 zero 的以下定义：

(define zero (lambda (f) (lambda (x) x)))

我有几个问题：

1. 为什么要复杂的语法？只需使用以下内容，它似乎很容易阅读：

   (define (zero f) 
      (lambda (x) x))
   

   我们可以看到它是一个名为 zero 的函数，它接受一个（未使用的）参数 f 并返回一个函数的一个参数，该函数将返回其参数。该定义似乎只是为了尽可能不直截了当。

2. 那里的 x 有什么用？例如做这样的事情：

   ((zero square) 100)
   

   返回 100。 x 只是返回的默认值吗？

解决方法

x 中没有 (lambda (x) x)。没有。

x 中的 (lambda (x) x) 绑定。它可以以任何名称命名。我们不能在x中谈论(lambda (x) x)，就像在y中不能谈论(lambda (y) y)一样。

y 中没有 (lambda (y) y) 可言。它只是一个占位符，一个任意名称，其在正文中的唯一目的是与活页夹中的相同。相同，不考虑在那里使用哪个特定名称，只要它使用两次 - 第一次在活页夹中，另一次在正文中。

事实上，对于 lambda 项有一个完整的“另一种表示法”，称为 De Bruijn 表示法，其中 相同的全部内容 写成 (lambda 1)。 1 的意思是“我指的是我上面 1 步的活页夹收到的参数”。

所以 x 并不重要。重要的是 (lambda (x) x) 表示一个按原样返回其参数的函数。所谓的“身份”功能。

但即使这在这里也不重要。数字的 Church 编码实际上是一个二元函数，该函数需要两个参数——f 和 z。 “后续步骤”一元函数 f 和“零”“值”z，无论可能是什么，只要两者结合即可。一起讲道理。一起工作。

当它实际上是一个二元函数时，我们怎么会在那里看到两个一元函数？

那是重要的一点。它被称为currying。

在 lambda 演算中，所有函数都是一元的。并且为了表示一个二元函数，使用了一元函数，这样当给定它的（第一个）参数时它返回另一个一元函数，当给定它的（现在，第二个）参数时，它执行我们的任何事情预期的二元函数应该使用这两个参数执行，第一个和第二个。

如果我们只用组合（等式）表示法而不是 lambda 表示法来编写它，这一切都非常非常简单：

zero f z = z
one f z = f z
two f z = f (f z) = f (one f z) = succ one f z
succ one f z = f (one f z)

其中每个并列表示一个应用程序，所有应用程序都在左侧关联，因此我们认为上面是

的快捷表示法

zero f = lambda z. z
zero = lambda f. (lambda z. z)
......
......
succ = lambda one. (lambda f. (lambda z. f (one f z) ))
;; such that
succ one f z = (((succ one) f) z)
  = ((((lambda one. (lambda f. (lambda z. f (one f z) ))) one) f) z)
  = .... 
  = (f ((one f) z))
  =  f (one f z)

但它是一样的。符号上的差异并不重要。

当然，one 中没有 lambda one. (lambda f. (lambda z. f (one f z) ))。它是绑定的。它可以只是命名，我不知道，number:

succ number f z = f (number f z) = f ((number f) z)

意思是，(succ number) 是这样一个数字，给定 f 和 z，对它们再做一个 f 步与 number 的做法相比。

---

因此，((zero square) 100) 表示，将数字 zero 与后继步骤 square 和 100 的零值一起使用，并让 zero 执行其我们的后续步骤数——也就是说，0 步——从零值开始。因此返回它不变。

另一种可能的用途是((zero (lambda (x) 0)) 1)，或者一般来说

((lambda (n) ((n (lambda (x) 0)) 1)) zero)  

;; or even more generally,abstracting away the 0 and the 1,((((lambda (n) (lambda (t) (lambda (f) ((n (lambda (x) f)) t)))) zero) 1) 0)

这只是另一种写作方式

zero (lambda x. 0) 1  ;; or

foo n t f = n (lambda x. f) t   ;; and calling

foo zero 1 0

希望您能轻松看到foo是什么。以及如何朗读此 t 和此 f。 （可能原来的 f 更适合命名为 s，表示“继任者”或类似名称）。