在 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) 一起工作就足够了，因为我可以担心以后扩展 Church 的定义。

---

编辑：

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

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

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

Answer 1

分支形式和短路

如果您使用像 Racket 这样的热切（而不是懒惰）语言，则需要注意如何编码分支形式，例如 COND 函数。

您对布尔值和条件的现有定义是：

(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

使用额外的 lambda 实现短路

我被教导用一种热切的语言解决这个问题（例如，不切换到 #lang lazy）是像这样将 thunk 传递给分支形式：

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

但是，这需要对布尔值的定义进行一些细微的调整。以前，布尔值有两个值可供选择，并返回一个。现在，一个布尔值会接受两个 thunk 以供选择，它会调用一个。

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

COND 表单的定义方式与以前相同，但您必须以不同的方式使用它。翻译(if c t e)之前你写的地方：

(((COND c) t) e)

现在有了布尔值的新定义，您将编写：

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

如果没有那些额外的 (λ () ....) 和布尔值的新定义，由于 Racket 急切（而不是懒惰）的参数评估，这将永远循环。