3

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

4

1 回答 1

2

简短的回答：你没有，但有了它们会容易得多。

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

假设您想通过值 lambda 演算对调用进行建模。它的语言（没有评估上下文）将是：

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

（这里，最后两行用于利用 Redex 的捕获避免替换。

现在，让我们尝试在不使用评估上下文的情况下为这种语言制作语义。有两个地方可以展开子表达式，运算符和函数应用的操作数。因此，包括正常的 beta-reduction 给我们：

(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如上图所示。这遵循按值调用语义，因为孔在应用程序中只能从左到右出现。

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

所以，回顾一下，你不需要，它只会让你的模型更短。

于 2017-02-02T19:41:45.130 回答