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

Question

我正在阅读 Greg Michaelson "An Introduction to Functional Programming Through Lambda Calculus" 的书学习 lambda 演算。

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

符号
单参数 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 也在任何类型的任何执行之前急切地求值，我们得到了 WhosebugError.

经过一番摸索，本书提出了一个新奇的设计，用于避免对前面示例的无限替换。

(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 是一种 "applicative order" 语言，因此参数在函数应用之前被评估，即使在那种情况下参数根本不会被使用。在这里，我们在 add 中重复出现，它将在 add 中重复出现...直到堆栈爆炸。在像 Haskell 这样的语言中，我认为这很好，因为它是惰性的（正常顺序），但我使用的是 Clojure。

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

编辑

正如@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)

但我仍然得到了 Whosebug。

我试图扩展函数"by hand"，但经过5轮beta缩减后，它看起来像在parens森林中无限扩展。

那么在没有宏的情况下使 Clojure "normal order" 而不是 "applicative order" 的技巧是什么。有可能吗？它甚至可以解决我的问题吗？

这个问题与这个问题非常接近：How to implement iteration of lambda calculus using scheme lisp?。除了我的是关于 Clojure 而不一定是关于 Y-Combinator。

Answer 1

对于严格的语言，您需要 Z combinator 而不是 Y 组合子。这是相同的基本思想，但将 (x x) 替换为 (fn [v] (x x) v) 以便将自引用包装在 lambda 中，这意味着仅在需要时对其进行评估。

您还需要修改布尔值的定义，以便使它们在严格的语言中工作：您不能只将您关心的两个值传递给它，并在它们之间传递 select。相反，您将 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 代替，或者任何东西。

Answer 2

我看到的问题是您的 Clojure 程序和 Lambda 微积分程序之间的耦合太强

您正在使用 Clojure lambda 来表示 LC lambda
您正在使用 Clojure variables/definitions 来表示 LC variables/definitions
你正在使用 Clojure 的应用机制（Clojure 的求值器）作为 LC 的应用机制

所以你 实际上 正在编写一个受 clojure compiler/evaluator 影响的 clojure 程序（不是 LC 程序）——这意味着 严格求值和非-常量-space方向递归。让我们看看：

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

作为 Clojure 程序，在严格求值的环境中，每次我们调用 add2 次，我们求值

(zero? b) 作为 value1
(value1 a) 作为 value2
(succ a) 作为 value3
(f value2) 作为 value4
(pred b) 作为 value5
(value2 value4) 作为 value6
(value6 value5)

我们现在可以看到调用 add2 always 会导致调用递归机制 f – 当然程序永远不会终止，我们得到堆栈溢出！

你有几个选择

根据@amalloy 的建议，使用 thunk 来延迟某些表达式的计算，然后在您准备好时强制 (运行) 它们继续计算——虽然我认为这不会教给你很多东西
您可以使用 Clojure 的 loop/recur 或 trampoline 常量-space 递归来实现您的 Y 或 Z 组合器——这里有一个小问题，因为你只希望支持单参数 lambda，而且在不优化的严格评估器中这样做会很棘手（也许不可能）尾调用

我在 JS 中做了很多这样的工作，因为大多数 JS 机器都会遇到同样的问题；如果您有兴趣查看自制解决方法，请查看：
编写一个实际的求值器——这意味着您可以将 Lambda 微积分程序的表示与 Clojure 和 Clojure 的数据类型和行为分离 compiler/evaluator – 您可以选择这些东西是如何工作的，因为你是编写评估程序的人

我从未在 Clojure 中做过这个练习，但我在 JavaScript 中做过几次 – 学习体验是变革性的。就在上周，我写了https://repl.it/Kluo which is uses a normal order substitution model of evaluation. The evaluator here is not stack-safe for large LC programs, but you can see that recursion is supported via Curry's Y on line 113 - it supports the same recursion depth in the LC program as the underlying JS machine supports. Here's another evaluator using memoisation and the more familiar environment model: https://repl.it/DHAT/2——也继承了底层JS机器的递归限制

在 JavaScript 中使递归堆栈安全确实很困难，正如我在上面链接的那样，并且（有时）需要在您的代码中进行大量转换才能使其堆栈安全。我花了 两个月 的许多不眠之夜才将其调整为堆栈安全、正常顺序、按需调用的评估器：https://repl.it/DIfs/2 – 这就像 Haskell 或球拍的 #lang lazy

至于在 Clojure 中执行此操作，JavaScript 代码可以轻松调整，但我对 Clojure 的了解还不够多，无法向您展示一个 合理的 评估程序可能看起来像——在书中，Structure and Interpretation of Computer Programs，（第 4 章），作者向您展示了如何使用 Scheme 本身为 Scheme（一种 Lisp）编写求值器。当然，这比原始的 Lambda 微积分复杂 10 倍，所以按理说，如果你能写一个 Scheme 求值器，你也可以写一个 LC。这可能对您更有帮助，因为代码示例看起来更像 Clojure

一个起点

我为您研究了一些 Clojure 并想出了这个 – 这只是严格评估器的开始，但它应该让您了解只需很少的工作就可以非常接近可行的解决方案。

请注意，我们在评估 'lambda 时使用 fn，但不会向程序用户透露此详细信息。 env 也是如此——也就是说，env 只是一个实现细节，不应该是用户关心的问题。

为了打败死马，你可以看到替代评估器和基于环境的评估器都得出了相同输入程序的等效答案——我不能太强调这些选择是如何达到的 you – 在 SICP 中，作者甚至继续更改求值器以使用简单的基于寄存器的模型来绑定变量和调用过程。可能性是无限的因为我们选择控制评估；用 Clojure 编写所有内容（就像您最初所做的那样）并没有给我们那种灵活性

;; lambda calculus expression constructors
(defn variable [identifier]
  (list 'variable identifier))

(defn lambda [parameter body]
  (list 'lambda parameter body))

(defn application [proc argument]
  (list 'application proc argument))

;; environment abstraction
(defn empty-env []
  (hash-map))

(defn env-get [env key]
  ;; implement
)

(defn env-set [env key value]
  ;; implement
)

;; meat & potatoes
(defn evaluate [env expr]
  (case (first expr)
    ;; evaluate a variable
    variable (let [[_ identifier] expr]
               (env-get env identifier))

    ;; evaluate a lambda
    lambda (let [[_ parameter body] expr]
             (fn [argument] (evaluate (env-set env parameter argument) body)))

    ;; evaluate an application
    ;; this is strict because the argument is evaluated first before being given to the evaluated proc
    application (let [[_ proc argument] expr]
                  ((evaluate env proc) (evaluate env argument)))

    ;; bad expression given
    (throw (ex-info "invalid expression" {:expr expr}))))


(evaluate (empty-env)
          ;; ((λx.x) y)
          (application (lambda 'x (variable 'x)) (variable 'y))) ;; should be 'y

_{* 或者它可能会针对未绑定的标识符 'y; 抛出错误；你的选择}

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

How to implement a recursive function in lambda calculus using a subset of Clojure language?

recursion

clojure

lambda-calculus