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

Question

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

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

• 符号
• 单参数 lambda 函数
• 功能应用
• 为方便起见定义变量。

到目前为止，我的这些功能都在工作：

(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 组合器，但我得出了同样可怕的结论。

编辑

正如@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 成为“正常顺序”而不是“应用顺序”的诀窍是什么。甚至可能吗？它甚至可以解决我的问题吗？

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

Answer 1

我看到的问题是你的 Clojure 程序和你的 Lambda Calculus 程序之间的耦合太强了

1. 您正在使用 Clojure lambdas 来表示 LC lambdas
2. 您正在使用 Clojure 变量/定义来表示 LC 变量/定义
3. 您正在使用 Clojure 的应用机制（Clojure 的评估器）作为 LC 的应用机制

所以您实际上正在编写一个受 clojure 编译器/评估器影响的 clojure 程序（不是 LC 程序）——这意味着 严格评估和非-恒定空间方向递归。我们来看看：

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

作为 Clojure 程序，在严格评估的环境中，每次我们调用add2，我们都会评估

1. (zero? b) 为 value1
2. (value1 a) 为 value2
3. (succ a) 为 value3
4. (f value2) 为 value4
5. (pred b) 为 value5
6. (value2 value4) 为 value6
7. (value6 value5)

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

---

你有几个选择

1. 根据@amalloy 的建议，使用 thunk 来延迟某些表达式的计算，然后在您准备好继续计算时强制（运行）它们——虽然我不认为这会教你很多东西

2. 您可以使用 Clojure 的 loop/recur 或 trampoline 进行常量空间递归来实现您的 Y 或 Z 组合器 - 这里有一点挂断，因为您只希望支持单参数 lambda，在不优化尾调用的严格评估器中这样做会很棘手（可能是不可能的）

   我在 JS 中做了很多这样的工作，因为大多数 JS 机器都会遇到同样的问题；如果您有兴趣查看自制解决方法，请查看：How do I replace while loops with a functional programming alternative without tail call optimization?

3. 编写一个实际的评估器 - 这意味着您可以将 Lambda 演算程序的表示与 Clojure 和 Clojure 的编译器/评估器的数据类型和行为分离 - 您可以选择这些事情如何工作，因为您'是写评估员的人

   我从来没有在 Clojure 中做过这个练习，但我在 JavaScript 中做过几次——学习体验是变革性的。就在上周，我写了https://repl.it/Kluo，它使用了一个正常的顺序替换评估模型。这里的求值器对于大型 LC 程序来说不是堆栈安全的，但您可以看到 Curry 在第 113 行的 Y 支持递归 - 它在 LC 程序中支持与底层 JS 机器支持的相同递归深度。这是另一个使用 memoisation 和更熟悉的环境模型的评估器：https://repl.it/DHAT/2 - 也继承了底层 JS 机器的递归限制

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

   至于在 Clojure 中执行此操作，JavaScript 代码可以很容易地适应，但我对 Clojure 的了解还不够多，无法向您展示一个明智的评估程序可能是什么样子——在书中，@ 987654325@, （第 4 章），作者向您展示了如何使用 Scheme 本身为 Scheme（一个 Lisp）编写一个评估器。当然，这比原始的 Lambda 演算复杂 10 倍，所以按理说，如果你能写一个 Scheme 求值器，你也可以写一个 LC 求值器。这可能对您更有帮助，因为代码示例看起来更像 Clojure

---

起点

我为你研究了一点 Clojure 并想出了这个 - 这只是一个严格的评估器的开始，但它应该让你知道需要多少工作才能非常接近一个可行的解决方案。

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

为了打败一匹死马，您可以看到替代评估器和基于环境的评估器都针对相同的输入程序得出了相同的答案 - 我不能强调这些选择是如何由您决定的 /em> – 在 SICP 中，作者甚至继续更改评估器以使用简单的基于寄存器的模型来绑定变量和调用 procs。可能性是无穷无尽的因为我们选择控制评估；用 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; 抛出错误；你的选择}

Answer 2

对于严格的语言，您需要 Z combinator 而不是 Y 组合符。这是相同的基本思想，但将 (x x) 替换为 (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 代替，或者任何东西。