eqv 的 R5RS 规范 letrec 示例？

Question

我正在阅读 R5RS 的规范，其中有 eqv?

的两个示例

(letrec ((f (lambda () (if (eqv? f g) 'both 'f)))
         (g (lambda () (if (eqv? f g) 'both 'g))))
  (eqv? f g))
                               ;; ===>  unspecified

(letrec ((f (lambda () (if (eqv? f g) 'f 'both)))
         (g (lambda () (if (eqv? f g) 'g 'both))))
  (eqv? f g))
                               ;; ===>  #f

我不明白这是不是代码错误，从我看来他们比较的是不同的函数对象，它们是两个 lambda 表达式，这是否意味着第一个示例如何 return如果由于优化而未指定，则为真？不应该反过来吗？未指定 (if (eqv? f g) 'f 'both) 这两个功能 return 相同的符号。

Spec link

Answer 1

这是一个非常微妙的例子。在第一个例子中：

(letrec ((f (lambda () (if (eqv? f g) 'both 'f)))
         (g (lambda () (if (eqv? f g) 'both 'g))))
  (eqv? f g))

嗯，f 和 g 在文字上是不同的，对吧？所以这应该是错误的。除此之外，好吧，如果我们假设 (eqv? f g) 是真的——我们假设 f 和 g 是实际上是一样的——然后我们可以优化掉条件，并将每个 f 和 g 重写为：

(letrec ((f (lambda () 'both))
         (g (lambda () 'both)))
  (eqv? f g))

现在，好吧，我们可以将它们优化为相同的功能，正如 eqv? 所考虑的那样。因此，假设函数与 eqv? 所考虑的相同，我们可以将它们优化为实际上 be 在 eqv? 下等效的状态。

在第二个例子中：

(letrec ((f (lambda () (if (eqv? f g) 'f 'both)))
         (g (lambda () (if (eqv? f g) 'g 'both))))
  (eqv? f g))

好吧，如果我们再次假设 f 和 g 相同，那么我们可以再次尝试优化条件：

(letrec ((f (lambda () 'f))
         (g (lambda () 'g)))
  (eqv? f g))

这显然是错误的。所以我们不能假设f和g是一样的。现在我们遇到了麻烦，因为如果我们假设它们不同那么我们也许可以再次优化它们......现在它们是相同的功能，也许可以优化为相同在 eqv? 下 ... 除了现在我们处于循环中。所以在 eqv? 下它们必须被认为是不同的，即使它们可能 return 相同的值。

第二个例子非常接近说谎者的悖论：它逃脱了，因为 eqv? 被允许不知道两件事是相同的（对于 'the same' 的定义，我有更努力地思考）即使他们实际上是。

个人注意：虽然我认为这些示例非常聪明和微妙，但我不会将它们放在规范中，或者至少在没有对系统允许或不允许的非常详细的解释的情况下不会这样做做，为什么。

eqv 的 R5RS 规范 letrec 示例？

R5RS Spec letrec example for eqv?

lisp

scheme