算术与教会数字

Question

我正在通过SICP工作,问题2.6让我陷入了困境.在处理教会数字时,将零和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)))))

通过wikipedia条目查看lambda演算,我发现plus的定义是PLUS:=λmnfx.mf(nfx).使用该定义,我能够制定以下程序.

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

我不明白的是,如何仅使用先前派生的程序给出的信息直接导出该过程.任何人都可以用某种严格的证明形式回答这个问题吗？直觉上,我想我明白发生了什么,但正如Richard Feynman曾经说过的那样,"如果我不能建造它,我就无法理解......"

Answer 1

它实际上非常简单.这可能会被视为flamebait,但括号使其难以看到的 - 更好的方式来看看会发生什么或者是想象一下你在一个令行禁止的语言的时候,或者只使用该方案具有多参数的函数的事实,拥抱那......这是一个使用lambdas和多个参数的解释:

• 每个数字N编码为

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

• 这意味着N的编码实际上是

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

  f^N功能取幂在哪里.

• 一种更简单的说法(假设是currying):数字N被编码为

  (lambda (f) f^N)
  

  所以N实际上是"提升N的力量"功能

• 现在接受你的表达(在lambda这里查看s):

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

  既然nis是一个数字的编码,那就是取幂,所以这实际上是:

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

  (好吧,不是太有趣,因为这个可能更明显.)