lambda - 在 Racket 中使用纯 lambda 演算和 Church 数字实现斐波那契数列

Question

一段时间以来，我一直在为 Lambda 微积分苦苦挣扎。有很多资源可以解释如何减少嵌套的 lambda 表达式，但很少能指导我编写自己的 lambda 表达式。

我正在尝试使用纯 lambda 演算(即单参数函数、教堂数字)在 Racket 中编写递归斐波那契解决方案。

这些是我一直在使用的教会数字的定义:

(define zero  (λ (f) (λ (x) x)))
(define one   (λ (f) (λ (x) (f x))))
(define two   (λ (f) (λ (x) (f (f x)))))
(define three (λ (f) (λ (x) (f (f (f x))))))
(define four  (λ (f) (λ (x) (f (f (f (f x)))))))
(define five  (λ (f) (λ (x) (f (f (f (f (f x))))))))
(define six   (λ (f) (λ (x) (f (f (f (f (f (f x)))))))))
(define seven (λ (f) (λ (x) (f (f (f (f (f (f (f x))))))))))
(define eight (λ (f) (λ (x) (f (f (f (f (f (f (f (f x)))))))))))
(define nine  (λ (f) (λ (x) (f (f (f (f (f (f (f (f (f x))))))))))))

这些是我一直试图合并的单参数函数:

(define succ   (λ (n) (λ (f) (λ (x) (f ((n f) x))))))
(define plus   (λ (n) (λ (m) ((m succ) n))))
(define mult   (λ (n) (λ (m) ((m (plus n)) zero))))
(define TRUE   (λ (t) (λ (f) t)))
(define FALSE  (λ (t) (λ (f) f)))
(define COND   (λ (c) (λ (x) (λ (y) ((c x) y)))))
(define iszero (λ (x) (x ((λ (y) FALSE) TRUE))))
(define pair   (λ (m) (λ (n) (λ (b) (((IF b) m) n)))))
(define fst    (λ (p) (p TRUE)))
(define snd    (λ (p) (p FALSE)))
(define pzero  ((pair zero) zero))
(define psucc  (λ (n) ((pair (snd n)) (succ (snd n)))))
(define pred   (λ (n) (λ (f) (λ (x) (((n (λ (g) (λ (h) (h (g f))))) (λ (u) x))(λ (u) u))))))
(define sub    (λ (m) (λ (n) ((n pred) m))))
(define leq    (λ (m) (λ (n) (iszero ((sub m) n))))) ;; less than or equal
(define Y      ((λ (f) (f f)) (λ (z) (λ (f) (f (λ (x) (((z z) f) x))))))) ;; Y combinator

我首先在 Racket 中编写递归斐波那契数列:

(define (fib depth)
  (if (> depth 1)
    (+ (fib (- depth 1)) (fib (- depth 2)))
  depth))

但是在我的多次尝试中，我一直没有成功使用纯 lambda 演算来编写它。即使是开始也是一场斗争。

(define fib
   (λ (x) ((leq x) one)))

我称之为(例如):

(((fib three) add1) 0)

这至少有效(正确返回教堂零或一)，但添加任何超出此范围的内容都会破坏一切。

我对 Racket 非常缺乏经验，而 Lambda 微积分对于直到最近才开始学习的人来说是一个令人头疼的问题。

我想了解如何构建这个函数，并将递归与 Y 组合器结合起来。我特别感谢任何代码旁边的解释。让它与 fib(zero) 一起工作高达 fib(six)就足够了，因为我可以担心以后会扩展教会的定义。

编辑:

我的 iszero函数在我的实现中是一个隐藏的破坏者。这是一个正确的版本，其中包含来自 Alex 答案的更新后的 bool 值:

(define iszero (λ (x) ((x (λ (y) FALSE)) TRUE)))
(define TRUE   (λ (t) (λ (f) (t))))
(define FALSE  (λ (t) (λ (f) (f))))

有了这些变化，并结合了 thunk，一切都正常了!

Answer 1

分支形式和短路

如果你使用像 Racket 这样急切(而不是懒惰)的语言，你需要小心你如何编码像 COND 这样的分支形式。功能。

您现有的 bool 值和条件定义是:

(define TRUE   (λ (t) (λ (f) t)))
(define FALSE  (λ (t) (λ (f) f)))
(define COND   (λ (c) (λ (x) (λ (y) ((c x) y)))))

它们适用于这样的简单情况:

> (((COND TRUE) "yes") "no")
"yes"
> (((COND FALSE) "yes") "no")
"no"

但是，如果“未采用分支”会产生错误或无限循环，那么好的分支形式会“短路”以避免触发它。一个好的分支形式应该只评估它需要采取的分支。

> (if #true "yes" (error "shouldn't get here"))
"yes"
> (if #false (error "shouldn't trigger this either") "no")
"no"

然而你的 COND评估两个分支，仅仅是因为 Racket 的函数应用程序评估所有参数:

> (((COND TRUE) "yes") (error "shouldn't get here"))
;shouldn't get here
> (((COND FALSE) (error "shouldn't trigger this either")) "no")
;shouldn't trigger this either

使用额外的 lambdas 来实现短路

我被教导用一种急切的语言来解决这个问题(例如，不切换到 #lang lazy)是将 thunk 传递给这样的分支形式:

(((COND TRUE) (λ () "yes")) (λ () (error "doesn't get here")))

但是，这需要对 bool 值的定义稍作调整。之前， bool 值需要两个值可供选择，然后返回一个。现在，一个 bool 值会从两个 thunk 中进行选择，它会调用一个。

(define TRUE (λ (t) (λ (f) (t))))   ; note the extra parens in the body
(define FALSE (λ (t) (λ (f) (f))))  ; same extra parens

COND form 可以像以前一样定义，但你必须以不同的方式使用它。翻译 (if c t e)在你写之前的地方:

(((COND c) t) e)

现在有了 bool 值的新定义，您将编写:

(((COND c) (λ () t)) (λ () e))

我要缩写(λ () expr)如 {expr}这样我就可以这样写:

(((COND c) {t}) {e})

现在，之前因错误而失败的操作返回了正确的结果:

> (((COND TRUE) {"yes"}) {(error "shouldn't get here")})
"yes"

这允许您编写条件，其中一个分支是停止的“基本情况”，而另一个分支是继续前进的“递归情况”。

(Y (λ (fib)
     (λ (x)
       (((COND ((leq x) one))
         {x})
        {... (fib (sub x two)) ...}))))

没有那些额外的 (λ () ....) 's 和 bool 值的新定义，这将永远循环，因为 Racket 的急切(而不是懒惰)参数评估。