问题描述
我正在用格雷格·迈克尔森（Greg Michaelson）的《通过Lambda微积分进行函数式编程入门》一书来研究lambda微积分。
I'm studying lambda calculus with the book "An Introduction to Functional Programming Through Lambda Calculus" by Greg Michaelson.
我仅使用一个子集在Clojure中实现示例语言。我只允许：
I implement examples in Clojure using only a subset of the language. I only allow :
- 符号
- 一个arg lambda函数
- 功能应用程序
- 为方便起见定义的变量。
- symbols
- one-arg lambda functions
- function application
- var definition for convenience.
到目前为止，我有那些工作的功能：
So far I have those functions working :
(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 。本书中第一次提到的尝试是这样的：
But now I am stuck on recursive functions. More precisely on the implementation of add. The first attempt mentioned in the book is this one :
(def add-1
(fn [a]
(fn [b]
(((cond a) ((add-1 (succ a)) (pred b))) (zero? b)))))
((add zero) zero)
Lambda演算规约法则替换为 add-1 带有包含定义本身的实际定义...无休止。
Lambda calculus rules of reduction force to replace the inner call to add-1 with the actual definition that contains the definition itself... endlessly.
在Clojure中，这是一个应用程序订单语言 add-1 在进行任何形式的执行之前也会急切评估，我们得到了 StackOverflowError 。
In Clojure, wich is an application order language, add-1 is also elvaluated eagerly before any execution of any kind, and we got a StackOverflowError.
经过一番摸索，本书提出了一种用于避免对上一个示例进行无限替换的装置。
After some fumblings, the book propose a contraption that is used to avoid the infinite replacements of the previous example.
(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要做的（参考透明性）：
Which is totally fine until we try it! This is what Clojure will do (referential transparency) :
((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]零）是一个lambda，在应用时需要一个参数。这里的参数是（（add（succ零））（pred零））。
Clojure是一种应用顺序语言，因此即使在此情况下根本不会使用参数，也会在应用函数之前对参数进行评估。在这里，我们在 add 中重复出现，而在 add 中重复出现...直到堆栈崩溃。
在像Haskell这样的语言中，我认为这会很好，因为它很懒（正常顺序），但是我使用的是Clojure。
On the last line (fn [second] zero) is a lambda that expects one argument when applied. Here the argument is ((add (succ zero)) (pred zero)).Clojure is an "applicative order" language so the argument is evaluated before function application, even if in that case the argument won't be used at all. Here we recur in add that will recur in add... until the stack blows up.In a language like Haskell I think that would be fine because it's lazy (normal order), but I'm using Clojure.
在那之后，这本书详细介绍了可以避免样板的美味Y组合器，但得出了同样令人毛骨悚然的结论。
After that, the book go in length presenting the tasty Y-combinator that avoid the boilerplate but I came to the same gruesome conclusion.
编辑
如@amalloy所建议，我定义了Z组合器：
As @amalloy suggests, I defined the Z combinator :
(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。
But I still get a StackOverflow.
I尝试手动扩展功能，但经过5轮beta还原
I tried to expand the function "by hand" but after 5 rounds of beta reduction, it looks like it expands infinitely in a forest of parens.
那么，使Clojure成为正常顺序而不是没有宏的应用顺序的窍门是什么呢？可能吗？它甚至可以解决我的问题吗？
So what is the trick to make Clojure "normal order" and not "applicative order" without macros. Is it even possible ? Is it even the solution to my question ?
这个问题与这个问题非常接近：。
This question is very close to this one : How to implement iteration of lambda calculus using scheme lisp? . Except that mine is about Clojure and not necessarily about Y-Combinator.
推荐答案
对于严格的语言，您需要，而不是Y组合器。这是相同的基本思想，但用（fn [v]（xx）v）替换（xx）自我引用包装在lambda中，这意味着仅在需要时才对其进行评估。
For strict languages, you need the Z combinator instead of the Y combinator. It's the same basic idea but replacing (x x) with (fn [v] (x x) v) so that the self-reference is wrapped in a lambda, meaning it is only evaluated if needed.
您还需要修正布尔值的定义，以使其在严格的条件下工作语言：您不能只将您关心的两个值传递给它并在它们之间进行选择。取而代之的是，您将其传递给用于计算您关心的两个值的处理程序，然后使用哑元参数调用适当的函数。也就是说，就像您通过eta扩展递归调用来修复Y组合器一样，您也可以通过eta扩展if和eta减少布尔值本身的两个分支来修复布尔值（我不是100％确定eta减少
You also need to fix your definition of booleans in order to make them work in a strict language: you can't just pass it the two values you care about and select between them. Instead, you pass it thunks for computing the two values you care about, and call the appropriate function with a dummy argument. That is, just as you fix the Y combinator by eta-expanding the recursive call, you fix booleans by eta-expanding the two branches of the if and eta-reduce the boolean itself (I'm not 100% sure that eta-reducing is the right term here).
(def add2 (fn [f]
(fn [a]
(fn [b]
((((zero? b) (fn [_] a)) (fn [_] ((f (succ a)) (pred b)))) b)))))
请注意，if的两个分支现在都用（ fn [_] ...），如果if本身用（... b）包装，其中b是我选择的值任意通过您可以改为传递零或任何其他值。
Note that both branches of the if are now wrapped with (fn [_] ...), and the if itself is wrapped with (... b), where b is a value I chose arbitrarily to pass in; you could pass zero instead, or anything at all.
这篇关于如何使用Clojure语言的子集在lambda演算中实现递归函数？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！