了解教堂数字

Understanding church numerals

我正在研究 SICP,它为 教会数字 zero 给出了以下定义:

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

我有几个问题:

  1. 为什么语法这么复杂?仅使用以下内容似乎可读性很强:

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

    我们可以看到它是一个名为 zero 的函数,它接受一个(未使用的)参数 f 和 return 一个单参数函数 return 其参数。几乎看起来这个定义只是为了尽可能不直接。

  2. 那里的x是做什么用的?例如做这样的事情:

    ((zero square) 100)
    

    returns 100x 只是默认值 returned 吗?

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

(lambda (x) x)中的x绑定。它可以用任何名字命名。我们不能在 (lambda (x) x) 中谈论 x,就像我们不能在 (lambda (y) y) 中谈论 y

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

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

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

但这在这里并不重要。数字的 Church 编码实际上是一个二元函数,一个需要两个参数的函数——fz。 “后继步骤”一元函数 f 和“零”“值”z,无论是什么,只要两者结合在一起即可。一起讲道理。一起努力。

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

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

在 lambda 演算中,所有函数都是一元函数。为了表示二元函数,使用一元函数,这样当给定它的(第一个)参数时,它 returns 另一个一元函数,当给出 its (现在,第二个) 参数,执行我们预期的二元函数应该执行的任何事情,使用这两个参数,第一个和第二个。

如果我们只是用组合(等式)表示法而不是 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)

但这是一回事。符号上的差异并不重要。

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

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

意思是,(succ number) 就是这样一个 数字 ,它给定 fz,再对它们做一个 f 步与 number 相比。


因此,((zero square) 100)表示,使用数字zero后继步骤square100的零值,并有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很容易明白什么是。以及如何大声朗读 tf。 (可能最初的 f 更适合命名为 s,表示“继承者”或类似的名称)。