如何使用 Clojure 语言的子集在 lambda 演算中实现递归函数？

我正在阅读 Greg Michaelson 所著的《通过 Lambda 演算进行函数式编程简介》一书来学习 lambda 演算。

我仅使用 Clojure 语言的一个子集来实​​现示例。我只允许：

• symbols
• 单参数 lambda 函数
• 功能应用
• var 定义是为了方便。

到目前为止，我已经使这些功能正常工作：

(def identity (fn [x] x))
(def self-application (fn [s] (s s)))

(def select-first (fn [first] (fn [second] first)))
(def select-second (fn [first] (fn [second] second)))
(def make-pair (fn [first] (fn [second] (fn [func] ((func first) second)))))    ;; def make-pair =  λfirst.λsecond.λfunc.((func first) second)

(def cond make-pair)
(def True select-first)
(def False select-second)

(def zero identity)
(def succ (fn [n-1] (fn [s] ((s False) n-1))))
(def one (succ zero))
(def zero? (fn [n] (n select-first)))
(def pred (fn [n] (((zero? n) zero) (n select-second))))

但现在我陷入了递归函数的困境。更准确地说是关于实施add。书中提到的第一个尝试是这样的：

(def add-1
  (fn [a]
    (fn [b]
      (((cond a) ((add-1 (succ a)) (pred b))) (zero? b)))))

((add zero) zero)

减少力的 Lambda 演算规则取代了内部调用add-1与包含定义本身的实际定义......无休止。

在 Clojure（一种应用程序订单语言）中，add-1在任何类型的执行之前也会急切地评估，我们得到了StackOverflowError.

经过一番摸索后，本书提出了一种巧妙的设计，用于避免前面示例的无限替换。

(def add2 (fn [f]
            (fn [a]
              (fn [b]
                (((zero? b) a) (((f f) (succ a)) (pred b)))))))
(def add (add2 add2))

的定义add扩展到

(def add (fn [a] 
           (fn [b]
             (((zero? b) a) (((add2 add2) (succ a)) (pred b)))))) 

在我们尝试之前这完全没问题！这就是 Clojure 要做的事情（引用透明度）：

((add zero) zero)
;; ~=>
(((zero? zero) zero) (((add2 add2) (succ zero)) (pred zero)))
;; ~=>
((select-first zero) (((add2 add2) (succ zero)) (pred zero)))
;; ~=>
((fn [second] zero) ((add (succ zero)) (pred zero)))

在最后一行(fn [second] zero)是一个 lambda，在应用时需要一个参数。这里的论据是((add (succ zero)) (pred zero))。 Clojure 是一种“应用顺序”语言，因此参数在函数应用之前进行评估，即使在这种情况下根本不会使用参数。在这里我们再次出现add会再次出现在add...直到堆栈爆炸。 在像 Haskell 这样的语言中，我认为这很好，因为它很懒（正常顺序），但我使用的是 Clojure。

之后，这本书详细介绍了避免样板文件的美味 Y 组合器，但我得出了同样可怕的结论。

EDIT

正如 @amalloy 所建议的，我定义了 Z 组合器：

(def YC (fn [f] ((fn [x] (f (fn [z] ((x x) z)))) (fn [x] (f (fn [z] ((x x) z)))))))

我定义了add2像这样：

(def add2 (fn [f]
            (fn [a]
              (fn [b]
                (((zero? b) a) ((f (succ a)) (pred b)))))))

我这样使用它：

(((YC add2) zero) zero)

但我仍然得到了 StackOverflow。

我尝试“手动”扩展该功能，但经过 5 轮 beta 缩减后，它看起来像是在括号森林中无限扩展。

那么有什么技巧可以让 Clojure 在没有宏的情况下成为“正常顺序”而不是“应用顺序”。有可能吗？这甚至可以解决我的问题吗？

这个问题与这个问题非常接近：如何使用scheme lisp实现lambda演算的迭代？ https://stackoverflow.com/questions/45931279/how-to-implement-iteration-of-lambda-calculus-using-scheme-lisp。只是我的内容是关于 Clojure 而不一定是关于 Y-Combinator。

对于严格的语言，您需要Z组合器 https://en.wikipedia.org/wiki/Fixed-point_combinator#Strict_fixed_point_combinator而不是 Y 组合器。基本思想相同，但替换为(x x) with (fn [v] (x x) v)这样自引用就被封装在 lambda 中，这意味着只有在需要时才会对其进行求值。

您还需要修复布尔值的定义，以便使它们以严格的语言工作：您不能只向其传递您关心的两个值并在它们之间进行选择。相反，您传递它 thunk 来计算您关心的两个值，并使用虚拟参数调用适当的函数。也就是说，就像您通过 eta 扩展递归调用来修复 Y 组合器一样，您也可以通过 eta 扩展 if 和 eta-reduce 布尔值本身的两个分支来修复布尔值（我不能 100% 确定 eta-reducing这里是正确的术语）。

(def add2 (fn [f]
            (fn [a]
              (fn [b]
                ((((zero? b) (fn [_] a)) (fn [_] ((f (succ a)) (pred b)))) b)))))

请注意，if 的两个分支现在都用(fn [_] ...)，并且 if 本身被包裹着(... b)，其中b是我任意选择传入的值；你可以通过zero相反，或者任何东西。