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

Question

我正在用Greg Michaelson的"通过Lambda微积分进行功能编程简介"一书中学习lambda演算.

我仅使用该语言的一个子集在Clojure中实现示例.我只允许:

• 符号
• one-arg 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组合子,避免了样板,但我得出了同样可怕的结论.

编辑

正如@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减少后,看起来它在parens森林中无限扩展.

那么在没有宏的情况下,使Clojure成为"正常顺序"而非"应用顺序"的诀窍是什么呢？它甚至可能吗？它甚至是我的问题的解决方案吗？

这个问题非常接近这个问题:如何使用方案lisp实现lambda演算的迭代？.除了我的是关于Clojure而不一定是关于Y-Combinator.

Answer 1

对于严格的语言,您需要Z组合器而不是Y组合器.它是相同的基本思想,但替换(x x)为(fn [v] (x x) v)使自引用包含在lambda中,这意味着只在需要时才进行评估.

您还需要修复布尔值的定义,以使它们以严格的语言运行:您不能只传递它关注的两个值并在它们之间进行选择.相反,你传递thunks来计算你关心的两个值,并使用伪参数调用适当的函数.也就是说,就像你通过eta扩展递归调用来修复Y组合子一样,你通过eta扩展if和eta的两个分支来修复布尔值 - 减少布尔本身(我不是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微积分程序之间的耦合太强了

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机器都遇到同样的问题; 如果您有兴趣查看自制的变通方法,请查看:如何在没有尾调用优化的情况下使用函数式编程替换while循环？

3. 写一个实际的评估者 - 这意味着你可以将你的Lambda微积分程序的表示与Clojure和Clojure的编译器/评估器的数据类型和行为分离 - 你可以选择这些东西是如何工作的,因为你是编写评估者的人

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

   如上所述,在JavaScript中使递归堆栈安全非常困难,并且(有时)需要在代码中进行大量转换才能使其成为堆栈安全的.我花了两个月的许多不眠之夜来将它调整为一个堆栈安全的,正常的,按需调用的评估器:https://repl.it/DIfs/2 - 这就像Haskell或Racket的#lang lazy

   至于在Clojure中这样做,JavaScript代码可以很容易地适应,但我不知道足够的Clojure向你展示一个合理的评估程序可能是什么样子 - 在书中,计算机程序的结构和解释,(第4章) ,作者向您展示了如何使用Scheme本身为Scheme(一个Lisp)编写一个求值程序.当然,这比原始的Lambda微积分复杂10倍,所以如果你能编写一个Scheme评估器,你也可以写一个LC.这可能对您更有帮助,因为代码示例看起来更像Clojure

一个起点

我为你研究了一点Clojure并提出了这个问题 - 它只是一个严格的评估者的开始,但它应该让你知道如何很少地工作以获得非常接近的工作解决方案.

请注意,我们fn在评估a 时会使用,'lambda但此详细信息不会透露给程序的用户.对于env- 也就是说,env只是一个实现细节而不应该是用户关注的问题.

为了击败死马,您可以看到替代评估者和基于环境的评估者都得到了相同输入程序的等效答案 - 我无法强调这些选择是由您决定的 - 在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引发错误; 你的选择}