教堂数字算术

发布于 2024-09-27 16:52:04 字数 912 浏览 5 评论 0原文

我正在通过 SICP 进行工作，并且问题 2.6 让我陷入了进退两难的境地。在处理丘奇数字时，将 0 和 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 的定义是 PLUS := λmnfx.mf (nfx)。使用该定义，我能够制定以下过程。

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

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

原文

I am working through SICP, and the problem 2.6 has put me in something of a quandary. In dealing with Church numerals, the concept of encoding zero and 1 to be arbitrary functions that satisfy certain axioms seems to make sense. Additionally, deriving the direct formulation of individual numbers using the definition of zero, and an add-1 function makes sense. I do not understand how a plus operator can be formed.

Thus far I have this.

(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)))))

Looking through the wikipedia entry for lambda calculus, I found that the definition of plus was PLUS := λmnfx.m f (n f x). Using that definition I was able to formulate the following procedure.

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

What I don't understand, is how that procedure can be derived directly using only the information given by the previously derived procedures. Can anyone answer this in some kind of rigorous proof-like form? Intuitively, I think I understand what's going on, but as Richard Feynman once said, "If I can't build it, I can't understand it..."

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

隔岸观火 2024-10-04 16:52:04

其实很简单。这可能会被视为诱饵，但括号使其更难看到——查看发生情况的更好方法是想象您使用的是柯里化语言，或者只是使用 Scheme 具有多参数函数的事实，并且拥抱这一点...下面是一个在方便的情况下使用 lambda 和多个参数的解释：

每个数字 N 都编码为

(lambda (fx) ...应用 (f (f (f ... (fx)))) N 次...)

这意味着N的编码实际上是
<前><代码>(lambda (fx) (f^N x))
其中f^N是函数求幂。
更简单的说法（假设柯里化）：数字 N 被编码为
<前><代码>(lambda (f) f^N)
so N 实际上是一个“提高 N 的幂” 函数
现在获取您的表达式（查看此处的 lambda 内部）：
<前><代码>((mf) ((nf) x))
由于 n 是数字的编码，它就是求幂，所以这实际上是：
<前><代码>((mf) (f^nx))
与m相同：
<前><代码>(f^m (f^nx))
其余的应该是显而易见的...您有 m 个 f 应用程序应用于 n 个 f 应用程序code> 应用于 x。
最后，为了留下一些乐趣——这是定义plus的另一种方法：
```
(定义 plus (lambda (m) (lambda (n) ((m add1) n))))
```
（嗯，不是太有趣，因为这个可能更明显。）

It's actually pretty simple. This will probably be viewed as flamebait, but the parens make it harder to see -- a better way to see what happens is either imagine that you're in a curried language, or just use the fact that Scheme has multi-argument functions and embrace that... Here's an explanation that uses lambdas and multiple argument where convenient:

Every number N is encoded as

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

This means that the encoding of N is actually
```
(lambda (f x) (f^N x))
```
where f^N is functional exponentiation.
A simpler way to say this (assuming currying): the number N is encoded as
```
(lambda (f) f^N)
```
so N is actually a "raise to the power of N" function
Now take your expression (looking inside the lambdas here):
```
((m f) ((n f) x))
```
since n is is an encoding of a number, it's that exponentiation, so this is actually:
```
((m f) (f^n x))
```
and the same for m:
```
(f^m (f^n x))
```
and the rest should be obvious... You have m applications of f applied on n applications of f applied on x.
Finally, to leave some fun -- here's another way to define plus:
```
(define plus (lambda (m) (lambda (n) ((m add1) n))))
```
(Well, not too much fun, since this one is probably more obvious.)

回复收藏 0 原文

廻憶裏菂餘溫 2024-10-04 16:52:04

^{（确保您了解高阶函数）。} 阿隆佐教堂的非类型化 lambda 演算函数是唯一的原始数据类型。没有数字、布尔值、列表或其他任何东西，只有函数。函数只能有 1 个参数，但函数可以接受和/或返回函数——不是这些函数的值，而是函数本身。因此，要表示数字、布尔值、列表和其他类型的数据，您必须想出一种巧妙的方法让匿名函数来代表它们。教堂数字是表示自然数。无类型 lambda 演算中三个最原始的构造是：

λx.x，一个恒等函数< /a>，接受某个函数并立即返回它。
λx.x x，自行申请。
λf.λx.f x，函数应用，接受一个函数和一个参数，并将函数应用于参数。

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

0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (fx)< /code>
3 = λf.λx.f (f (fx))

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

这就是为什么 add1 是 λn.λf.λx.f ((nf) x)：您将 n 应用于 f 然后使用 x 将表达式简化为主体，然后将 f 应用于该主体，然后使用 λf.λx. 再次对其进行抽象。 练习：也看到这是真的，快速学习β-reduction 并减少 (λn.λf.λx.f ((nf) x)) (λf.λx.f (fx)) 以将 2 增加 1。

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

结论：要将 2 个数字 a 和 b 加在一起，这两个数字都表示为教堂数字，您需要替换 x 位于 a 中，主体为 b，因此 f (fx) + f (f (fx)) = f (f (f (f (fx))))。要实现这一点，请将 a 应用于 f，然后应用于 bf x。

^{(Make sure you understand higher-order functions).} In Alonzo Church's untyped lambda calculus a function is the only primitive data type. There are no numbers, booleans, lists or anything else, only functions. Functions can have only 1 argument, but functions can accept and/or return functions—not values of these functions, but functions themselves. Therefore to represent numbers, booleans, lists and other types of data, you must come up with a clever way for anonymous functions to stand for them. Church numerals is the way to represent natural numbers. Three most primitive constructs in untyped lambda calculus are:

λx.x, an identity function, accepts some function and immediately returns it.
λx.x x, self-application.
λf.λx.f x, function application, takes a function and an argument, and applies a function to an argument.

How do you encode 0, 1, 2 as nothing else but functions? We somehow need to build the notion of quantity into the system. We have only functions, every function can be applied only to 1 argument. Where can we see anything resembling quantity? Hey, we can apply a function to a parameter multiple times! There's obviously a sense of quantity in 3 repeated invocations of a function: f (f (f x)). So let's encode it in lambda calculus:

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

And so on. But how do you go from 0 to 1, or from 1 to 2? How would you write a function that, given a number, would return a number incremented by 1? We see the pattern in Church numerals that the term always starts with λf.λx. and after you have a finite repeated application of f, so we need to somehow get into the body of λf.λx. and wrap it into another f. How do you change a body of an abstraction without reduction? Well, you can apply a function, wrap the body in a function, then wrap the new body into the old lambda abstraction. But you don't want arguments to change, therefore you apply abstractions to the values of the same name: ((λf.λx.f x) f) x → f x, but ((λf.λx.f x) a) b) → a b, which is not what we need.

That's why add1 is λn.λf.λx.f ((n f) x): you apply n to f and then x to reduce the expression to the body, then apply f to that body, then abstract it again with λf.λx.. Exercise: too see that it's true, quickly learn β-reduction and reduce (λn.λf.λx.f ((n f) x)) (λf.λx.f (f x)) to increment 2 by 1.

Now understanding the intuition behind wrapping the body into another function invocation, how do we implement addition of 2 numbers? We need a function that, given λf.λx.f (f x) (2) and λf.λx.f (f (f x)) (3), would return λf.λx.f (f (f (f (f x)))) (5). Look at 2. What if you could replace its x with the body of 3, that is f (f (f x))? To get body of 3, it's obvious, just apply it to f and then x. Now apply 2 to f, but then apply it to body of 3, not to x. Then wrap it in λf.λx. again: λa.λb.λf.λx.a f (b f x).

Conclusion: To add 2 numbers a and b together, both of which are represented as Church numerals, you want to replace x in a with the body of b, so that f (f x) + f (f (f x)) = f (f (f (f (f x)))). To make this happen, apply a to f, then to b f x.

回复收藏 0 原文

故事灯 2024-10-04 16:52:04

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))))

Eli's answer is technically correct but since at the point that this question is asked the #apply procedure has not been introduced, I don't think that the authors intended the student to have knowledge of that or of concepts such as currying to be able to answer this question.

They pretty much guide one to the answer by suggesting that one apply the substitution method, and then from there one should notice that the effect of the addition is a composition of one number onto the other. Composition is a concept was introduced in exercise 1.42; and that's all that is required to understand how an additive procedure can work in this system.

; 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))))

回复收藏 0 原文

~没有更多了~