教会数字算术

Question

我正在通过 SICP 工作，problem 2.6 让我陷入了困境。在处理 Church 数字时，将零和 1 编码为满足某些公理的任意函数的概念似乎是有意义的。此外，使用零的定义和 add-1 函数推导出单个数字的直接公式是有意义的。我不明白加号运算符是如何形成的。

到目前为止，我有这个。

(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
  (lambda (f) (lambda (x) (f ((n f) x)))))

(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))

查看lambda calculus 的维基百科条目，我发现加号的定义是 PLUS := λmnfx.m f (n f x)。使用该定义，我能够制定以下程序。

(define (plus n m)
  (lambda (f) (lambda (x) ((m f) ((n f) x)))))

我不明白的是，如何仅使用先前派生过程提供的信息直接派生该过程。谁能以某种严格的类似证明的形式回答这个问题？直觉上，我想我明白发生了什么，但正如理查德·费曼曾经说过的，“如果我不能建造它，我就无法理解它......”

Answer 1

^{（确保您了解higher-order functions）。}在Alonzo Church 的untyped lambda calculus 中，函数是唯一的原始数据类型。没有数字、布尔值、列表或其他任何东西，只有函数。函数只能有 1 个参数，但函数可以接受和/或返回函数——不是这些函数的值，而是函数本身。因此，要表示数字、布尔值、列表和其他类型的数据，您必须想出一种巧妙的方法让匿名函数代表它们。 Church numerals 是表示natural numbers 的方式。无类型 lambda 演算中三个最原始的构造是：

1. λx.x，identity function，接受一些函数并立即返回。
2. λx.x x，自行申请。
3. λf.λx.f x，函数应用程序，接受函数和参数，并将函数应用于参数。

如何将 0、1、2 编码为函数？我们需要以某种方式将数量的概念构建到系统中。我们只有函数，每个函数只能应用于 1 个参数。我们在哪里可以看到类似数量的东西？嘿，我们可以多次将函数应用于参数！一个函数的 3 次重复调用显然有量感：f (f (f x))。所以让我们用 lambda 演算对其进行编码：

• 0 = λf.λx.x
• 1 = λf.λx.f x
• 2 = λf.λx.f (f x)
• 3 = λf.λx.f (f (f x))

等等。但是你如何从 0 到 1，或从 1 到 2？你将如何编写一个函数，给定一个数字，返回一个加 1 的数字？我们在 Church 数字中看到该术语始终以 λf.λx. 开头的模式，并且在您有限重复应用 f 之后，因此我们需要以某种方式进入 λf.λx. 的主体并将其包装起来进入另一个f。如何在不减少的情况下更改抽象体？好吧，您可以应用一个函数，将主体包装在一个函数中，然后将新主体包装到旧的 lambda 抽象中。但是您不希望参数改变，因此您将抽象应用于同名的值：((λf.λx.f x) f) x → f x，但 ((λf.λx.f x) a) b) → a b，这不是我们需要的。

这就是为什么add1 是λn.λf.λx.f ((n f) x)：你将n 应用于f，然后x 将表达式简化为主体，然后将f 应用于该主体，然后再次使用@ 抽象它987654347@。 练习：也知道这是真的，快速学习β-reduction 并减少(λn.λf.λx.f ((n f) x)) (λf.λx.f (f x)) 以使2 加1。

现在理解了将 body 包装到另一个函数调用背后的直觉，我们如何实现 2 个数字的加法？我们需要一个函数，给定 λf.λx.f (f x) (2) 和 λf.λx.f (f (f x)) (3)，将返回 λf.λx.f (f (f (f (f x)))) (5)。看看 2。如果您可以替换它的 x 为 3 的主体，即 f (f (f x))？要获得 3 的主体，很明显，只需将其应用于 f，然后将其应用于 x。现在将 2 应用于 f，然后将其应用于 3 的主体，而不是 x。然后再次将其包裹在λf.λx. 中：λa.λb.λf.λx.a f (b f x)。

结论：要将两个数字a 和b 加在一起，这两个数字都表示为教堂数字，你想替换 x in @ 987654363@ 和 b 的主体，所以 f (f x) + f (f (f x)) = f (f (f (f (f x))))。要做到这一点，请将a 应用到f，然后应用到b f x。

Answer 2

Eli 的回答在技术上是正确的，但由于在提出这个问题时尚未引入 #apply 程序，我认为作者并不打算让学生了解该问题或诸如柯里化之类的概念才能回答这个问题。

他们几乎通过建议一个人应用替换方法来引导一个人找到答案，然后从那里人们应该注意到加法的效果是一个数字与另一个数字的组合。组合是练习 1.42 中引入的一个概念；这就是了解附加程序如何在该系统中工作所需要的全部内容。

; The effect of procedure #add-1 on `one`, and `two` was the composition of `f` 
; onto `one` and `f` onto `two`.
;
; one   : (λ (f) (λ (x) (f x)))
; two   : (λ (f) (λ (x) (f (f x))))
; three : (λ (f) (λ (x) (f (f (f x)))))
;
; Thus one may surmise from this that an additive procedure in this system would
; work by composing one number onto the other.
;
; From exercise 1.42 you should already have a procedure called #compose.
;
; With a little trial and error (or just plain be able to see it) you get the
; following solution.

(define (adder n m)
  (λ (f)
    (let ((nf (n f))
          (mf (m f)))
      (compose nf mf))))

Answer 3

其实很简单。这可能会被视为火焰诱饵，但括号使其更难看到 - 了解发生了什么的更好方法是想象您使用的是咖喱语言，或者只是使用 Scheme 具有多参数功能和接受它...这是一个使用 lambdas 和多个参数的解释：

• 每个数字 N 都被编码为

  (lambda (f x) ...apply (f (f (f ... (f x)))) N times...)
  

• 这表示N的编码实际上是

  (lambda (f x) (f^N x))
  

  其中f^N 是函数求幂。

• 一个更简单的说法（假设柯里化）：数字 N 被编码为

  (lambda (f) f^N)
  

  所以N实际上是一个“N次幂”函数

• 现在表达你的看法（看看这里的lambdas）：

  ((m f) ((n f) x))
  

  因为n是一个数字的编码，它就是指数，所以这实际上是：

  ((m f) (f^n x))
  

  m 也一样：

  (f^m (f^n x))
  

  其余的应该很明显...您已将m 的f 应用应用于n 应用f 应用于x。

• 最后，让一些有趣——这是定义plus的另一种方式：

  (define plus (lambda (m) (lambda (n) ((m add1) n))))
  

  （好吧，不是很有趣，因为这个可能更明显。）