scheme - eqv 的 R5RS Spec 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 表达式，这是否意味着第一个示例如果由于优化而未指定，如何返回 true？不应该反过来吗？未指定(if (eqv? f g) 'f 'both)两个函数返回相同的符号。

规格链接

标签： schemelisp

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?我们会进入一种可以优化它们以在 下实际等效的状态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?，即使它们可能返回相同的值。

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

---

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