racket - 为什么我需要 Redex 中的评估上下文？

Question

完全可以在不使用求值上下文的情况下为我的语言编写求值规则。我的语义完全是按值调用的，不允许在 lambda 内部向前推进该术语。尽管如此，我看到的所有资源都以某种方式使用了归约上下文。使用我缺少的上下文是否有充分的理由？

Answer 1

简短的回答:你不需要，但有了它们就容易多了。

长答案:几乎所有你会使用评估上下文的东西，你都可以在你的归约关系中使用不同的归约规则，它只会变得更加令人讨厌，特别是当你建模除了最小的语言之外的任何东西时。

假设您要通过值 lambda 演算对调用进行建模。它的语言(没有评估上下文)将是:

(define-language Lv
  (v (λ (x) e))
  (e v
     (e e))
  (x variable-not-otherwise-mentioned)
  #:binding-forms
  (λ (x) e #:refers-to x))

(此处，最后两行用于利用 Redex 的 capture avoiding substitution。

现在，让我们尝试在不使用求值上下文的情况下为该语言创建语义。有两个地方我们可以扩展子表达式，运算符和函数应用的操作数。因此，将其包含在正常的 beta 还原中可以得到:

(define red
  (reduction-relation
   Lv
   (--> (e_1 e_2)
        (v_1 e_2)
        (where v_1 ,(first (apply-reduction-relation red (term e_1)))))
   (--> (v_1 e_2)
        (v_1 v_2)
        (where v_2 ,(first (apply-reduction-relation red (term e_2)))))
   (--> ((λ (x) e) e_2)
        (substitute e x e_2))))

这还不算太糟糕，但请记住，我们必须为每个可以计算子表达式的地方添加一个额外的规则。所以 let 需要自己的规则，if 需要自己的规则，等等。请记住，这是在每种形式的规则之上。

一个更简单的方法是使用评估上下文，它允许我们指定哪些表达式具有可以采取步骤的子表达式，以及它们应该以什么顺序发生。所以让我们尝试重写我们的 Lv 具有评估上下文的语言:

(define-language Lv2
  (v (λ (x) e))
  (e v
     (e e))
  (x variable-not-otherwise-mentioned)
  (E hole
     (E e)
     (v E))
  #:binding-forms
  (λ (x) e #:refers-to x))

它现在长了三行，但这告诉 redex 我们将在求值上下文 E 中求值我们的表达式，当它完成表达式求值时，将它放入上下文(在哪里hole 可以说是顶级上下文)。因此，我们可以将归约关系简化为一个规则，即 beta 归约:

(define red2
  (reduction-relation
   Lv2
   (--> (in-hole E ((λ (x) e) e_2))
        (in-hole E (substitute e x e_2)))))

这里我们使用 in-hole 表示我们在 E 之后的洞中，如上所示。这遵循按值语义调用，因为孔只能在应用程序中从左到右出现。

您可以想象，如果您有一个包含许多子表达式的更大的演算，这将使您不必编写大量归约规则。

因此，回顾一下，您不需要这样做，它只会让您的模型短得多。